Twenty-Five Centuries of Logic

✱1Aristotle and the syllogism

Greece · Aristotle 384–322 BCE · Prior Analytics ⁹

Context

Aristotle was born in Stagira, studied in Plato’s Academy until 347 BCE and founded his own school, the Lyceum, in 335 ⁹. He inherited a culture of competitive argument. Zeno of Elea had refuted opponents by deriving absurdities from their assumptions; Plato split statements into noun and verb and catalogued sophistic tricks ¹⁰. Aristotle’s Topics is a manual for debate. In the Prior Analytics he asked a more general question: which arguments are conclusive purely because of their form? His logical works were later collected as the Organon (“instrument”), a title he never used ⁵.

The idea

Aristotle’s statements link two general terms in one of four ways, later labelled with vowels: A every S is P; E no S is P; I some S is P; O some S is not P. A syllogism has two premises that share a middle term M, and a conclusion that links the other two terms. Where the middle term sits gives three figures. Aristotle went through every pairing of premises, found the valid ones (14 in his three figures) and showed the rest invalid by giving counterexample terms. He treated four first-figure forms as perfect, evident on their face, and proved the others from them by converting premises (“no S is P” to “no P is S”) or by reductio ^5,1.

He wrote letters in place of terms; they work much like the variables of modern logic ¹⁰. In modern notation, with a caveat about empty terms explained below:

Worked example

What it changed

For two thousand years, “logic” meant mainly Aristotle’s syllogistic, studied through commentaries in Greek, Arabic and Latin (✱5–✱7). Kant still called it complete in 1787 (✱8). Its limit is that it handles one-place properties (“is mortal”) but not relations: it cannot show that if every horse is an animal, every head of a horse is the head of an animal. Frege removed that limit (✱10). Aristotle’s modal syllogistic (Prior Analytics I.8–22) and his “sea battle” passage on future contingents (On Interpretation 9) seeded modal and many-valued logic (✱18, ✱19) ¹².

Misconceptions

• Aristotle drew the square of opposition.The relations are his (On Interpretation 6–7); the diagram first survives in a text attributed to Apuleius (2nd century CE, attribution disputed) and was passed on by Boethius ¹¹.
• Aristotle named the moods Barbara, Celarent and so on.The names come from a medieval memory verse, first found in William of Sherwood in the 1230s ².

Further reading: Kneale & Kneale, ch. II ¹⁵; Handbook vol. 1 (Woods & Irvine; Boger; Johnson) ¹⁶.

Sources for ✱1: 1–2, 5, 9–19.

✱2Dialecticians and Stoics

Athens · Diodorus Cronus (taught c. 315–284 BCE) · Philo · Chrysippus c. 280–207 BCE ^20,21

Context

In the generation after Aristotle, Diodorus Cronus and his pupil Philo argued about what makes an “if … then” statement true. David Sedley groups them in a “Dialectical school” distinct from the Megarians; whether that school existed is debated ²⁰. Chrysippus of Soli, head of the Stoa from about 230 BCE, turned these debates into a system. He reportedly wrote over 700 books, none of which survives whole ²¹. We know Stoic logic from later reports, especially Diogenes Laertius and Sextus Empiricus ¹⁰.

The idea

The Stoic unit is a whole assertible (axioma), something said that is true or false at a given time. Assertibles combine with connectives: if, and, or, not. Where Aristotle’s letters stand for terms, Stoic variables (“the first”, “the second”) stand for whole propositions. Five basic argument forms, the indemonstrables, need no proof; four rules (themata) reduce other arguments to them, and only two of those rules survive ^10,22.

From the sourcesWording of the examples after Diogenes Laertius VII.80–81 ²²; the symbols are modern.

What makes “if p then q” true? Philo: it is false only when it begins with a truth and ends with a falsehood. Diodorus: it is true when it neither was nor is possible for p to be true and q false, in effect Philo’s test holding at all times ²⁰. A third view required a real connection: the denial of q must conflict with p ²².

Worked example

What it changed

The Stoics had a logic of propositions about two thousand years before Boole and Frege. It faded between the 3rd and 6th centuries CE ¹⁰, and pieces reached the Latin Middle Ages through Boethius (✱5). Its nature was recognized only once modern propositional logic existed: Łukasiewicz argued in 1934–35 that the Stoics had a propositional logic ²³, and Benson Mates reconstructed it in Stoic Logic (1953) ²⁴. Philo’s conditional anticipates the material conditional (✱9, ✱10); Diodorus’s resembles C. I. Lewis’s strict implication (✱19).

Misconceptions

• Philo invented the material conditional.He came close, but his statements are true or false at a time, so a conditional can change its truth value ²⁰.
• Stoic logic is a variant of Aristotle’s syllogistic.It is a different kind of logic, built on connectives between whole propositions rather than on relations between terms ¹⁰.

Further reading: Kneale & Kneale, ch. III ¹⁵; Handbook vol. 1 (O’Toole & Jennings) ¹⁶.

Sources for ✱2: 10, 15–16, 20–24.

✱3India: Nyāya, Dignāga, Dharmakīrti

South Asia · Nyāya-sūtra (dating disputed) · Dignāga c. 480–540 · Dharmakīrti 6th–7th c. · Gaṅgeśa c. 1300–1350 ^{25,26,27,28,29}

Context

Indian logic grew from public debate about doctrine and from the theory of pramāṇas, the reliable sources of knowledge: perception, inference (anumāna), comparison and testimony ³⁰. The founding text of the Nyāya school is the Nyāya-sūtra, attributed to Gautama (Akṣapāda). Its date is uncertain: estimates run from the 2nd century BCE to a redaction in the 2nd or 3rd century CE ^25,26,30. Buddhist logicians reshaped the field: Dignāga (c. 480–540) ²⁷ and Dharmakīrti, placed by different scholars between the mid-6th and the 7th century ²⁸. In the 14th century Gaṅgeśa of Mithilā founded “new Nyāya” (Navya-Nyāya) with his Tattvacintāmaṇi ²⁹.

The idea

Inference here is about evidence. Seeing smoke on a hill, we infer fire, because smoke is pervaded by fire (vyāpti): wherever there is smoke, there is fire. The Nyāya-sūtra (1.1.32) sets out an argument for others in five members ²⁵. Dignāga asked what makes a reason (hetu) good and gave three conditions, the trairūpya ²⁶. With H the reason, S the property to be proved and p the subject:

IllustrationDignāga’s three conditions ²⁶ applied to the Nyāya smoke example ³⁰; the formulas are a modern rendering.

Condition 3 is equivalent to ∀x(Hx → Sx), the pervasion. Together with condition 1 it yields S(p) by a valid step, provided condition 3 really covers every case. Dharmakīrti held that a pervasion must rest on a real relation, of identity of nature or of cause and effect, and recognized three kinds of good reason: nature, effect and non-perception ³¹. Navya-Nyāya built a precise technical language for stating pervasions and the extra conditions (upādhi) that defeat them ²⁹.

Worked example

What it changed

Indian logicians built detailed theories of faulty reasons (hetvābhāsa) and of how general connections are known. Navya-Nyāya’s technical idiom spread through Indian scholarship in many fields after the 14th century ²⁹. How far it resembles Aristotle’s syllogistic is itself a research question ^32,33.

Misconceptions

• The five-membered argument is Aristotle’s syllogism with extra steps.The example step supplies evidence for the general rule, and whether the scheme is deductive at all is the open question above ^33,34.
• The tetralemma proves that Buddhists rejected the law of non-contradiction.That is one contested reading among several ³⁸.

Further reading: Handbook vol. 1 (Ganeri, “Indian Logic”) ¹⁶.

Sources for ✱3: 16, 25–39.

✱4China: the Mohist canons

Warring States China · Mohist “Dialectics” late 4th – mid 3rd c. BCE · Gongsun Long c. 320–250 BCE ^40,41,42

Context

Mozi (fl. c. 430 BCE) founded a movement that taught impartial concern for everyone ⁴⁰. Later Mohists, who are anonymous, wrote the “Dialectics”: the Canons, their Explanations and two essays, the Greater and Lesser Selections (Daqu, Xiaoqu), now books 40–45 of the Mozi, probably from the late 4th to the mid 3rd century BCE ⁴¹. Their setting was biàn 辯, disputation: arguing over whether a term applies to a thing. Thinkers such as Hui Shi and Gongsun Long were later filed under a “School of Names”, a Han-dynasty catalogue label rather than a real school ⁴².

The idea

For the Mohists, reasoning works by kinds (lèi 類): things alike in the relevant way can be called by the same word. A gù 故 is a reason or cause; a fǎ 法 is a model or standard to compare against. Arguments proceed by analogy, by setting sentences in parallel and by extending what an opponent already accepts ⁴¹. The Xiaoqu examines when a parallel inference works:

Worked example

What it changed

The Mohists produced a careful theory of terms, kinds and reasons. After the Han dynasty the tradition was largely neglected and the texts survived in damaged form; modern study owes much to A. C. Graham’s reconstruction (1978) ⁴⁵.

Misconceptions

• Mozi wrote the canons.They are anonymous works of later Mohists ⁴¹.
• “A white horse is not a horse” is about Platonic universals.Most scholars now reject that reading ⁴².

Sources for ✱4: 40–48.

✱5Transmission and Arabic logic

Rome · Baghdad · Bukhara · Córdoba · al-Fārābī c. 870–950 · Avicenna 980–1037 · Averroes 1126–1198 ^49,50,51

Context

Late antique teachers read Aristotle through Porphyry’s Isagoge, an introduction to the Categories ⁵². In the Latin West, Boethius (c. 475/7–526) translated and commented on the Categories and On Interpretation and wrote textbooks, including one on hypothetical (conditional) syllogisms; his works were the main logic texts of the Latin West from the 9th to the 12th century ⁵³. In Baghdad, between the 8th and 10th centuries, Greek logic was translated into Arabic, often through Syriac, by scholars such as Ḥunayn ibn Isḥāq (d. 873) and Abū Bishr Mattā (d. 940) ⁵⁴. In a famous debate of 932, the grammarian al-Sīrāfī attacked logic as Greek grammar in disguise, against Abū Bishr ⁵⁵.

Al-Fārābī, called the “second master” after Aristotle, wrote commentaries and summaries on Aristotle’s logic, of which only the long commentary on On Interpretation survives complete ⁵⁶. He argued that logic stands to thought as grammar stands to a particular language ⁵⁷. Avicenna (Ibn Sīnā) wrote the logic of al-Shifāʾ in the 1020s and al-Ishārāt in the 1030s. He reorganized the subject instead of commenting on it, and Arabic logic divides into the periods before and after him ⁵⁰. Averroes (Ibn Rushd) of Córdoba returned to close commentary on Aristotle ⁵¹.

The idea

Avicenna made time and modality part of every categorical statement. “Every J is B” can be read in two main ways ⁵⁸. With E(x,t) for “x exists at time t”:

He also built a logic of conditionals quantified over times, such as “whenever the sun is up, it is day”, with its own syllogisms ⁵⁰.

Worked example

What it changed

Avicenna was the main Arabic influence on Latin logic; Averroes’s commentaries began to reach Latin readers in the 1220s–30s, though his middle commentaries on logic probably arrived later, in William of Luna’s translations ^17,59. In the Islamic world logic continued after the 12th century: the Shamsiyya of al-Kātibī (13th century) became a madrasa textbook that is still studied ⁵⁸.

Misconceptions

• Arabic scholars merely preserved Greek logic for Europe.They translated it, then built new temporal, modal and conditional logics on it ⁵⁰.
• Arabic logic ended with Averroes.Averroes was among the last of one line; the Avicennan tradition went on for centuries ⁵⁸.

Further reading: Handbook vol. 1 (Street, “Arabic Logic”; Burnett) ¹⁶.

Sources for ✱5: 16–17, 49–60.

✱6Abelard and the terminists

Paris · Oxford · Abelard 1079–1142 · William of Sherwood (1230s) · Peter of Spain (between the 1220s and 1250s) ^61,2,62

Context

Until about 1120, Latin logic rested on the “old logic”: Porphyry, the Categories, On Interpretation and Boethius ⁵³. Peter Abelard was the most famous teacher in Paris. The dates of his writings are largely uncertain ⁶¹; one estimate puts the Dialectica before 1117 or around 1118–19 ⁶³. From about 1120 Boethius’s translations of the rest of Aristotle’s logic began to circulate ⁶⁴, and the Prior Analytics came back into use in the mid-12th century, forming the “new logic” ¹⁷. In the 13th-century universities, textbooks by William of Sherwood and Peter of Spain set out a new topic: the properties of terms in sentences. Their authors are called terminists ^2,62.

The idea

Abelard held that an entailment must be necessary, and that a perfect entailment holds by its form alone, so that it survives any uniform substitution of terms: a formal account of validity ⁶¹. He also insisted on negating a whole proposition by putting “not” in front of it ⁶⁵. The terminists studied supposition, what a term stands for in a particular sentence ⁶⁶:

From the sourcesStandard examples of the period, as used by Peter of Spain, William of Sherwood and Ockham ^62,66,67.

Worked example

What it changed

Supposition theory is a medieval semantics of reference. Material supposition is what quotation marks do today, and the descent to singulars anticipates quantifier semantics (✱10, ✱14). Sherwood’s textbook contains the earliest surviving memory verse “Barbara, Celarent, Darii…” ², and Peter of Spain’s was taught in universities into the 17th century ⁶².

Misconceptions

• Medieval Europe always had Aristotle’s whole logic.Before the 12th century it had only Porphyry’s Isagoge, the Categories, On Interpretation and Boethius’s works ⁵³.

Further reading: Kneale & Kneale, ch. IV ¹⁵; Handbook vol. 2 (Marenbon; Wilks; Parsons) ⁶⁸.

Sources for ✱6: 2, 15, 17, 53, 61–68.

✱7Ockham, Buridan and paradox

Oxford · Paris · Ockham c. 1287–1347 · Summa Logicae c. 1323–25 · Buridan c. 1300–after 1358 · Treatise on Consequences 1335 ^69,70,71

Context

William of Ockham, an English Franciscan, wrote his Summa Logicae around 1323–25 ⁶⁹. He was a nominalist: only individual things exist, and general terms signify through concepts. In Paris, John Buridan spent his career teaching logic and natural philosophy. His Summulae de dialectica began as a commentary on Peter of Spain and grew more than ten times longer ⁷⁰, and his Treatise on Consequences is dated to 1335 ⁷¹. At Oxford, Thomas Bradwardine wrote on the “insolubles”, paradoxes such as the Liar, in 1321–24 ⁷².

The idea

A consequence is a valid inference between propositions, and 14th-century logicians built a general theory of them. A consequence is formal if it holds for all terms as long as its form, given by words like “every”, “not”, “and”, “if”, is kept; it is material if it holds because of what particular terms mean ⁶. Ockham states the laws now named after De Morgan: the contradictory of a conjunction is the disjunction of the contradictories of its parts, and the converse for disjunctions ⁷³.

Worked example

What it changed

Fourteenth-century logic had formal validity defined by substitution, propositional laws, quantifier semantics, the semantic paradoxes and even a relative of Curry’s paradox: the anonymous “Pseudo-Scotus” discussed the argument “God exists, therefore this argument is invalid” ⁶. Obligationes were formal disputation games with rules for what a respondent must grant ⁷⁴.

Misconceptions

• Ockham wrote “entities are not to be multiplied beyond necessity”.That wording appears nowhere in his works, though he did say that plurality should not be posited without necessity ⁶⁹.
• Scholastic logic was sterile hair-splitting.It contains real results on validity, reference and paradox, including a forerunner of Curry’s paradox ^6,72.

Further reading: Handbook vol. 2 (Klima; Dutilh Novaes; Yrjönsuuri) ⁶⁸.

Sources for ✱7: 6, 68–74.

✱8Leibniz’s dream

Europe · Port-Royal Logic 1662 · Leibniz 1646–1716 (papers of April 1679) · Euler 1768 · Kant 1787 ^76,77,78,79

Context

Seventeenth-century logic books turned toward method. The Port-Royal Logic of Antoine Arnauld and Pierre Nicole (1662) had four parts, on conceiving, judging, reasoning and ordering, and it distinguished the comprehension of an idea (its features) from its extension (what it applies to) ⁷⁶. Gottfried Wilhelm Leibniz, co-inventor of the calculus, wanted more: a universal symbolic language, the characteristica universalis, in which reasoning would be calculation, so that a dispute could be settled by saying “let us calculate” ⁷⁷.

The idea

In papers of April 1679, Leibniz gave each simple concept a prime number and each compound concept the product of its parts. Then “every S is P” is true when the number for P divides the number for S ⁷⁷. To handle particular and negative statements he gave each term a pair of coprime numbers; Łukasiewicz later showed that this arithmetic captures the traditional valid syllogisms, though Leibniz never treated negative concepts. Later papers (1686, 1690) developed an algebra of concepts that Wolfgang Lenzen shows to be equivalent to Boolean algebra ⁷⁷.

Worked example

What it changed

Leonhard Euler drew the four kinds of categorical statement as circles in his Letters to a German Princess, written in 1760–61 and published from 1768 ^78,19. In 1787 Kant wrote that logic had not taken a step forward or backward since Aristotle and seemed complete ⁷⁹. Leibniz had already gone further, but few could know it: Raspe (1765) and Erdmann (1839–40) printed only fragments, the bulk of the logical papers appeared in Couturat’s edition of 1903, and Boole learned of Leibniz’s ideas only after writing The Laws of Thought ⁷⁵. Frege later presented his concept-script as a step toward Leibniz’s universal characteristic (✱10) ⁸⁰.

Misconceptions

• Leibniz’s logic led to Boole’s.Boole worked without knowing it, and most of the papers were printed only in 1903 ⁷⁵.

Further reading: Kneale & Kneale, ch. V ¹⁵; Handbook vol. 3 (Lenzen, “Leibniz’s Logic”) ⁸².

Sources for ✱8: 15, 19, 75–82.

✱9The algebra of logic

Britain · USA · Germany · De Morgan and Boole 1847 · Boole 1854 · Jevons 1864 · Venn 1880 · Peirce 1870–1885 · Schröder 1890–1905 ^83,3,18,84

Context

In 1847 two books appeared: Augustus De Morgan’s Formal Logic and George Boole’s The Mathematical Analysis of Logic ⁸³. Boole, a largely self-taught mathematician from Lincoln who became professor at Queen’s College Cork in 1849, followed with An Investigation of the Laws of Thought in 1854 ^3,85. The program continued with W. S. Jevons, John Venn, C. S. Peirce in the United States, and Ernst Schröder, whose German lectures (1890–1905) summed up the field ⁸³.

The idea

Let letters stand for classes. xy is the class of things that are both x and y; 1 is the universe and 0 the empty class; 1 − x is everything that is not x. Selecting the x’s twice gives the x’s again, so x² = x. Among numbers only 0 and 1 obey this law, and rearranged it reads x(1 − x) = 0: nothing is both x and not-x ^3,85. “All X are Y” becomes x(1 − y) = 0.

Boole’s x + y was defined only for classes with no common members. Jevons made addition inclusive, so that x + x = x, in 1864; Boole rejected the change, and Peirce adopted it independently ⁸³. De Morgan and then Peirce (1870) extended the algebra to relations, and Peirce with his student O. H. Mitchell introduced symbols for “some” and “all” (Σ and Π, 1883–85) ^84,86.

Worked example

What it changed

Logic became a branch of algebra, with laws that could be proved like algebraic identities. Venn’s 1880 paper systematized the diagrams that bear his name ¹⁸. In his 1937 master’s thesis, published in 1938, Claude Shannon used Boolean algebra to design relay switching circuits, the start of its life in digital electronics ⁸⁸.

Misconceptions

• Boole invented the Boolean algebra of today.His addition was partial and he used ordinary subtraction and division; the modern system came from Jevons, Peirce and Schröder, and the name later ³.
• Venn invented logic diagrams.Euler’s circles came earlier (✱8). Venn’s change was to draw every possible region and shade the empty ones ¹⁹.

Further reading: Handbook vol. 3 (Hailperin; Hilpinen, “Peirce’s Logic”) ⁸²; vol. 4 (Jacquette, “Boole’s Logic”; Van Evra, “Venn’s Logic”) ⁹⁰.

Sources for ✱9: 3, 18–19, 82–91.

✱10Frege’s Begriffsschrift

Jena · Frege 1848–1925 · Begriffsschrift 1879 · Grundlagen 1884 · Grundgesetze 1893, 1903 ⁹²

Context

Gottlob Frege, a mathematician at Jena, wanted to show that arithmetic follows from logic alone, a view later called logicism. For that he needed a language in which every step of a proof is explicit, with no gaps for intuition to fill ⁹². His Begriffsschrift (“concept-script”, 1879) was that language ⁸⁰.

The idea

Three innovations. First, sentences are analysed as function and argument instead of subject and predicate: “Brutus killed Caesar” is K(b, c), so relations are as easy as properties. Second, a quantifier binds a variable and has a definite scope. Third, a system of axioms with modus ponens and substitution as rules, the first axiomatic presentation of quantificational logic ⁸⁹. Frege’s notation was two-dimensional:

Worked example

What it changed

Modern logic starts here, though in a notation nobody adopted: the symbols used today descend from Peano and Russell. Frege’s 1892 paper on sense and reference explained why substituting co-referring names can change what a sentence says, the phenomenon met in ✱4. His Grundgesetze derived arithmetic from axioms including Basic Law V, and that law is what Russell’s paradox broke (✱11) ⁹².

Misconceptions

• Frege was ignored in his lifetime.Partly true: the Begriffsschrift was reviewed, among others by Venn and Schröder, and Peano reviewed the Grundgesetze, but wide recognition came only after Russell’s discussion in 1903 ⁹⁶.
• Russell’s paradox refuted logic.It refuted Basic Law V, one axiom of Frege’s system ⁹².

Further reading: Handbook vol. 3 (Sullivan, “Frege’s Logic”) ⁸². English translation of the Begriffsschrift in van Heijenoort ⁹⁷.

Sources for ✱10: 80, 82, 89, 92–97.

✱11Paradox and Principia

Cambridge · Göttingen · Burali-Forti 1897 · Russell’s letter 16 June 1902 · Zermelo 1908 · Principia Mathematica 1910–13 ^{98,99,100,101}

Context

Georg Cantor’s set theory, from the 1870s, treated infinite collections as objects in their own right ¹⁰². Then paradoxes appeared. Cesare Burali-Forti published one about the collection of all ordinals in 1897 ⁹⁸. Bertrand Russell found a simpler one in spring 1901 and wrote to Frege on 16 June 1902; Frege replied on 22 June, acknowledging that it undermined his system ^92,99. Ernst Zermelo had found the same contradiction independently, around 1900–02 ¹⁰³.

The idea

Naive set theory, and Frege’s Basic Law V, allow every condition to define a set: {x | φ(x)}. Choose the condition “x is not a member of itself”. Two repairs followed. Zermelo’s axioms (1908) let a condition carve out a set only inside an existing set: {x ∈ A | φ(x)} ¹⁰⁰. Russell’s theory of types sorts objects into levels (individuals, classes of individuals, classes of those…) and allows x ∈ y only when y is one level above x, so x ∈ x cannot even be written ⁹⁸. Principia Mathematica, by Whitehead and Russell (1910–13), rebuilt mathematics on a refined, “ramified” version of types, needing an extra axiom of reducibility that critics found ad hoc ¹⁰¹.

Worked example

What it changed

Zermelo’s system, with the axiom of Replacement later proposed by Fraenkel and Skolem, is the root of the modern axiomatizations of set theory ¹⁰⁴. Types became central to computing (✱20). Principia is the system named in the title of Gödel’s 1931 paper (✱13) ¹⁰⁵, and in 1956 a computer program proved theorems from its second chapter (✱21) ¹⁰⁶.

Misconceptions

• Principia needs hundreds of pages to prove 1 + 1 = 2.✱54.43 in volume I is a lemma about classes with two members. The arithmetical 1 + 1 = 2 is ✱110.643 in volume II, where the authors remark that it is “occasionally useful” ¹⁰⁷.
• Russell’s paradox is the barber puzzle.The barber who shaves exactly those who do not shave themselves simply cannot exist. Russell’s paradox matters because naive set theory and Frege’s axioms say that his set does exist.

Further reading: Handbook vol. 5 (Irvine, “Russell’s Logic”) ¹⁰⁸. The Russell–Frege letters and Zermelo 1908 are translated in van Heijenoort ⁹⁷.

Sources for ✱11: 92, 97–108.

✱12Hilbert’s program

Göttingen · Hilbert 1862–1943 · lectures from 1921 · “On the Infinite” 1925 · Hilbert & Ackermann 1928 ^109,110,111

Context

After the paradoxes, and under attack from Brouwer’s intuitionism (✱17), David Hilbert proposed in lectures from 1921–22 to secure classical mathematics once and for all ¹¹². His lecture “On the Infinite” (Münster, 4 June 1925; published 1926) is the best-known statement ¹¹⁰. The 1928 textbook by Hilbert and Ackermann posed two open questions: is first-order logic complete, and is there a mechanical procedure to decide whether any given formula is valid, the Entscheidungsproblem ^95,111. The dispute with Brouwer turned personal: in 1928 Hilbert had him removed from the editorial board of the Mathematische Annalen ¹¹³.

The idea

Write mathematics as a formal system: a list of symbols, rules for building formulas, axioms and rules of inference. A proof is then a finite sequence of formulas, each an axiom or obtained from earlier ones by a rule, and checking a proof is mechanical. Consistency becomes a statement about finite strings of symbols: no proof ends in 0 = 1. Hilbert wanted to prove that statement by finitary reasoning about concrete symbols, which even sceptics of the infinite accept ¹¹².

Worked example

What it changed

Proofs became mathematical objects, and their study, metamathematics or proof theory, became a field. Hilbert’s two 1928 questions were answered within eight years: completeness yes (Gödel, ✱13), decidability no (Church and Turing, ✱15) ^114,111. The consistency goal ran into Gödel’s second theorem (✱13) and was transformed by Gentzen (✱16).

Misconceptions

• Hilbert thought mathematics was a meaningless game with symbols.He separated “real” statements with concrete finitary content from “ideal” ones, and the consistency proof was to justify using the ideal ones ¹¹².

Further reading: Handbook vol. 5 (Sieg, “Hilbert’s Proof Theory”) ¹⁰⁸. “On the Infinite” is translated in van Heijenoort ⁹⁷.

Sources for ✱12: 95, 97, 108–114.

✱13Gödel

Vienna · Gödel 1906–1978 · completeness 1929 (publ. 1930) · incompleteness 1931 ^115,114,105

Context

Kurt Gödel, a student of Hans Hahn in Vienna, proved in his 1929 dissertation that first-order logic is complete, answering one of Hilbert and Ackermann’s questions ¹¹⁴. At a conference in Königsberg on 7 September 1930 he mentioned, almost in passing, a far more surprising result; John von Neumann saw its importance at once ^116,112. The paper appeared in 1931 ¹⁰⁵.

The idea

Completeness: if a sentence is true in every structure where the premises are true, it can be derived from them: Γ ⊨ φ ⇒ Γ ⊢ φ. First incompleteness theorem: if a theory F is consistent, its axioms can be listed by a mechanical procedure, and it contains a modest amount of arithmetic, then some sentence G can be neither proved nor refuted in F. Gödel’s version needed a slightly stronger assumption (ω-consistency), which Rosser removed in 1936. Second theorem: such an F cannot prove its own consistency statement Con(F) ¹¹⁶.

Worked example

What it changed

Hilbert’s hope of proving the consistency of mathematics by finitary means, inside mathematics, could not succeed in its original form. Turing’s analysis (✱15) made “listed by a mechanical procedure” precise, so the theorems apply to every such system. Proof theory continued in relativized forms, beginning with Gentzen (✱16) ¹¹².

Misconceptions

• Gödel proved that mathematics is inconsistent, or that truth is unknowable.The theorems concern provability in one formal system at a time. A sentence unprovable in F can be proved in a stronger system ¹¹⁶.
• G is simply “true but unprovable”.G is true if F is consistent, and its self-reference is only a provable equivalence ¹¹⁶.
• Completeness and incompleteness contradict each other.“Complete” means different things in the two theorems: first-order logic proves every valid formula, while particular theories of arithmetic leave some sentences undecided ¹¹⁶.

Further reading: Handbook vol. 5 (van Atten & Kennedy, “Gödel’s Logic”) ¹⁰⁸. Both 1930 and 1931 papers are translated in van Heijenoort ⁹⁷.

Sources for ✱13: 97, 105, 108, 112, 114–116.

✱14Tarski and truth

Warsaw → Berkeley · Tarski 1901–1983 · truth monograph 1933 (Polish), 1935 (German) · logical consequence 1936 ^117,118,7

Context

Alfred Tarski, of the Lvov–Warsaw school of logic, moved to Berkeley in 1942 ¹¹⁷. The Liar paradox had made “truth” look suspect to scientifically minded philosophers. Tarski’s monograph, published in Polish in 1933 and in German in 1935, showed how to define truth exactly for a formalized language ¹¹⁸.

The idea

Any adequate definition of “true sentence of language L” must imply every instance of the T-schema: “s” is true ↔ p, where p translates s (Convention T). Tarski met this test by defining satisfaction clause by clause, one clause per logical symbol, in a metalanguage stronger than the language being described. He also proved that a sufficiently rich language cannot define its own truth predicate ^118,7.

Worked example

What it changed

Tarski’s definitions are the basis of semantics and model theory. In 1936 he defined logical consequence: a sentence follows from premises when every model of the premises is a model of the sentence ⁷. That is the ⊨ in Gödel’s completeness theorem. The split between object language and metalanguage echoes the medieval material supposition of ✱6.

Misconceptions

• The T-schema is Tarski’s definition of truth.It is the adequacy test a definition must pass; the definition itself goes through satisfaction ¹¹⁸.

Further reading: Handbook vol. 5 (Simmons, “Tarski’s Logic”; Cantini, “Paradoxes, Self-reference and Truth”) ¹⁰⁸.

Sources for ✱14: 7, 108, 117–118.

✱15Church and Turing

Princeton · Cambridge · Church 1903–1995 · Turing 1912–1954 · both 1936 · Post 1936 ^{119,120,121,122,123}

Context

To show that Hilbert’s decision problem has no solution, one needs a precise definition of “mechanical procedure”. Alonzo Church in Princeton identified effective calculability with definability in his λ-calculus and, in a note received in April 1936, proved the decision problem unsolvable ^121,111. Alan Turing in Cambridge reached the same result independently: his paper was received on 28 May 1936 and published in 1936–37 ¹²². Emil Post published a similar model later in 1936 ¹²³. Church named “Turing machines” in his 1937 review ¹²⁴.

The idea

Turing analysed what a human computer does with pencil and squared paper. His machine has a tape of squares, a head that reads and writes one symbol at a time, and finitely many states. Each rule says: in state q, reading symbol s, write s′, move left or right, go to state q′. A universal machine reads the description of any other machine and imitates it, the idea behind stored-program computers. Turing showed his machines compute exactly the λ-definable functions ¹²². The Church–Turing thesis says these models capture every function a human could compute by following rules ¹¹¹.

Worked example

What it changed

Computability became a precise subject. The universal machine keeps a program as data on its tape; the stored-program idea of von Neumann’s EDVAC design can be traced to it, though historians reject the claim that Turing alone invented the modern computer ¹²⁴. The λ-calculus became the core of functional programming and of the proof assistants of ✱20 and ✱22 ¹²⁶.

Misconceptions

• The Church–Turing thesis is a theorem, or says that minds and physical devices are Turing machines.It is a thesis about rule-following human calculation, which cannot be proved. Claims about physics or minds are separate and much more contested ¹¹¹.

Further reading: Handbook vol. 5 (Cardone & Hindley, “Lambda-calculus and Combinators”; Urquhart, “Emil Post”) ¹⁰⁸; vol. 9 (Davis, “Logic and the Development of the Computer”) ¹²⁷.

Sources for ✱15: 108, 111, 119–127.

✱16Gentzen

Göttingen · Gentzen 1909–1945 · natural deduction and sequent calculus 1934–35 · consistency of arithmetic 1936 ^128,129,130

Context

Axiom systems in the style of Frege and Hilbert do not resemble how mathematicians argue. Gerhard Gentzen, in Göttingen, designed proof systems that do, in “Investigations into Logical Deduction” (1934–35) ¹²⁹. Stanisław Jaśkowski developed natural deduction independently, from a problem Łukasiewicz posed in 1926 ¹³¹. In 1936 Gentzen proved the consistency of arithmetic ¹³⁰. Interned in Prague at the end of the war, he died of malnutrition on 4 August 1945 ¹²⁸.

The idea

In natural deduction, each connective has an introduction rule (how to prove it) and an elimination rule (how to use it), and you may assume something temporarily and later discharge the assumption. In the sequent calculus, statements Γ ⊢ Δ record what follows from what, and a “cut” rule allows lemmas. Gentzen’s main theorem (Hauptsatz) says that cuts can always be removed. A cut-free proof contains only parts of its own conclusion (the subformula property), which yields consistency and makes proof search possible ¹³¹.

Worked example

What it changed

Gentzen proved arithmetic consistent using induction along the ordinal ε₀, the limit of ω, ω^ω, ω^ωω, … This goes beyond Hilbert’s strict finitism, and in 1943 Gentzen showed that arithmetic cannot prove this induction itself, exactly as Gödel’s second theorem requires ¹²⁸. Measuring theories by ordinals became ordinal analysis, and his proof systems became the backbone of structural proof theory and of the link between proofs and programs (✱20).

Misconceptions

• Gentzen’s consistency proof contradicts Gödel.It uses a principle, induction up to ε₀, that arithmetic cannot prove, so it agrees with Gödel’s second theorem ¹²⁸.

Further reading: Handbook vol. 5 (von Plato, “Gentzen’s Logic”) ¹⁰⁸.

Sources for ✱16: 108, 112, 128–131.

✱17Intuitionistic logic

Amsterdam · Moscow · Brouwer 1881–1966 (1907, 1908) · Kolmogorov 1925, 1932 · Heyting 1930 · Kripke 1965 ^113,132,133

Context

L. E. J. Brouwer held that mathematics is mental construction. His 1908 paper on “the unreliability of the logical principles” argued that the law of excluded middle, A ∨ ¬A, was abstracted from finite cases and wrongly extended to infinite ones ¹³². Kolmogorov gave a partial formal treatment in 1925; Arend Heyting formalized intuitionistic logic in 1930; Kolmogorov read it in 1932 as a calculus of problems ^133,134.

The idea

Meaning is given by what counts as a proof. This is the BHK reading, a name Troelstra coined in 1977 ¹³²:

A proof of A ∨ ¬A would have to decide A, and for open problems nobody can. So excluded middle is not asserted in general, although its double negation ¬¬(A ∨ ¬A) is provable ¹³³.

Worked example

What it changed

Glivenko (1929) showed a propositional formula is classically provable exactly when its double negation is intuitionistically provable; Gödel (1932) showed intuitionistic logic is not a many-valued logic with finitely many values; Gödel and Gentzen translated classical arithmetic into intuitionistic arithmetic in 1933 ¹³³. The proof-as-construction reading became the core of type theory and proof assistants (✱20, ✱22).

Misconceptions

• Intuitionists claim that excluded middle is false.They decline to assert it in general; denying it outright is contradictory in their own logic, since ¬¬(A ∨ ¬A) is provable ¹³³.
• Intuitionistic logic is a three-valued logic.Gödel proved in 1932 that no finite truth table captures it ¹³².

Further reading: Handbook vol. 5 (J. R. Moschovakis, “The Logic of Brouwer and Heyting”) ¹⁰⁸.

Sources for ✱17: 108, 113, 132–135.

✱18Many-valued logics

Warsaw · New York · Moscow · Berkeley · Łukasiewicz 1920 · Post 1921 · Kleene 1938 · Bochvar 1938 · Zadeh 1965 ^136,91,137

Context

Jan Łukasiewicz introduced a third truth value in 1920. His motive was indeterminism: a statement about a future free choice, like Aristotle’s sea battle (✱1), seemed to be neither true nor false yet ¹³⁶. Emil Post studied systems with any number of values in 1921. Stephen Kleene’s three-valued tables (1938) read the third value as “undefined”, for computations that may never finish; Bochvar (1938) used a third value to analyse paradoxes ⁹¹. Lotfi Zadeh’s fuzzy sets (1965) allowed degrees of membership between 0 and 1 ¹³⁷.

The idea

Allow values 1, ½, 0 and define connectives as functions on them. Some values are designated (here only 1), and a formula is a tautology if it always takes a designated value. In Łukasiewicz’s logic Ł3 ⁹¹:

Worked example

What it changed

SQL databases treat comparisons with a missing value (NULL) as “unknown”, and their AND, OR and NOT follow Kleene’s strong three-valued tables ¹³⁸. Łukasiewicz’s infinite-valued logic became one basis of fuzzy logic ¹³⁶.

Misconceptions

• Fuzzy truth degrees are probabilities.Fuzzy connectives are truth-functional; probabilities are not, since the probability of “A and B” is not fixed by those of A and B ⁹¹.
• Paraconsistent logicians believe contradictions are true.Only dialetheists, such as Priest, hold that some are; paraconsistency is just the refusal of explosion ¹³⁹.

Further reading: Handbook vol. 8 (Malinowski, “Many-valued Logic”; Priest; Dubois, Prade & Godo, “Fuzzy Logic”) ¹⁴¹.

Sources for ✱18: 84, 91, 136–141.

✱19Modal logic and possible worlds

Harvard · Oxford · Princeton · Lewis 1912–1932 · Carnap 1947 · Prior 1957 · Kripke 1959, 1963 ^{142,143,144,145}

Context

C. I. Lewis objected that the material conditional makes a true statement follow from anything, as in q → (p → q). From 1912 he proposed a stronger strict implication, and with C. H. Langford in 1932 he set out five systems, S1 to S5. They were purely axiomatic, with no account of what makes them true and no way to choose between them ¹⁴². Rudolf Carnap (1947) read “necessary” as true in all state-descriptions, and Arthur Prior built tense logic (Time and Modality, 1957) ^142,143. Saul Kripke’s papers of 1959 and 1963 gave the semantics now standard ^144,145.

The idea

A Kripke model has a set of worlds W, an accessibility relation R between them, and a record of which basic statements hold where ¹⁴⁶. Then:

Properties of R match axioms: reflexive with □A → A (T), transitive with □A → □□A (4), symmetric with B, euclidean with 5 ¹⁴⁶. S4 is the logic of reflexive and transitive frames; S5 of equivalence relations. The same machinery reads □ as “necessarily”, “it is known that”, “it ought to be that”, “always in future” or, following Gödel (1933), “it is provable that” ¹⁴².

Worked example

What it changed

Relational semantics turned a zoo of axiom systems into one theory with many readings: epistemic, deontic and tense logic among them ¹⁴⁶, and the temporal logics used to verify hardware and software (✱22).

Misconceptions

• Kripke invented the idea of possible worlds.Carnap’s state-descriptions (1947) came earlier, and several logicians reached relational ideas at about the same time; Kripke’s contribution was a general relational semantics with completeness proofs ^142,148.
• Lewis’s systems came with a semantics.They were purely axiomatic ¹⁴².

Further reading: Handbook vol. 7 (Goldblatt, “Mathematical Modal Logic”; Øhrstrøm & Hasle, “A. N. Prior’s Logic”) ¹⁴⁹.

Sources for ✱19: 142–149.

✱20Types and Curry–Howard

Princeton · Stockholm · Eindhoven · Paris · Church 1940 · Curry 1934 · Howard 1969 (publ. 1980) · de Bruijn 1968 · Martin-Löf 1972–84 ^{150,151,152,153}

Context

Church’s simple theory of types (1940) attached types to λ-calculus terms ¹⁵⁰. Haskell Curry noticed in 1934 that the types of basic combinators look like axioms of the logic of implication. William Howard extended the observation to natural deduction in a manuscript of 1969 that circulated as a photocopy and was published only in 1980 ^126,151. Independently, N. G. de Bruijn presented Automath, a language for checking mathematics by machine, in 1968 ¹⁵². Per Martin-Löf’s intuitionistic type theory (from 1972; book 1984) ¹⁵³ and Coquand and Huet’s Calculus of Constructions (1985; journal version 1988) ¹⁵⁴ turned the idea into foundations for mathematics. Homotopy type theory, from Voevodsky’s univalent foundations, followed in 2013 ¹⁵⁵.

The idea

A proposition is a type, and a proof of it is a program of that type ¹²⁶:

Simplifying a proof, by removing a detour where a connective is introduced and then immediately eliminated, is the same as running the program ¹²⁶. This is the BHK reading of ✱17 made exact.

Worked example

What it changed

Proof assistants are built on these theories: Agda on Martin-Löf’s type theory, Coq (now Rocq) on the calculus of inductive constructions, and Lean on the calculus of constructions ¹⁵³. Checking a proof there means type-checking a program (✱22).

Misconceptions

• Howard published the correspondence in 1969.He wrote it then; it was published in 1980 ¹²⁶.
• It was one discovery.It emerged in stages, from Curry (1934) through Tait, Howard and de Bruijn to Martin-Löf ¹²⁶.

Further reading: Handbook vol. 5 (Seldin, “The Logic of Church and Curry”) ¹⁰⁸.

Sources for ✱20: 108, 126, 150–155.

✱21Automated reasoning and SAT

RAND · Princeton · Toronto · Moscow · Logic Theorist 1956 · Davis–Putnam 1960 · DLL 1962 · Robinson 1965 · Cook 1971 · Levin 1973 · CDCL 1996–2001 ^{106,156,157,158,159}

Context

In 1955–56 Allen Newell, Cliff Shaw and Herbert Simon’s Logic Theorist proved 38 of the first 52 theorems in chapter 2 of Principia Mathematica ¹⁰⁶. Martin Davis and Hilary Putnam (1960), then Davis, Logemann and Loveland (1962), gave procedures for propositional satisfiability ¹⁵⁶, and J. A. Robinson’s resolution with unification (1965) did the same job for first-order logic ¹⁵⁷. Stephen Cook proved in 1971 that satisfiability (SAT) is NP-complete, and Leonid Levin did so independently in 1973 ^157,158. From 1996 conflict-driven clause learning (CDCL) solvers, starting with GRASP and Chaff, made SAT solving practical at industrial scale ¹⁵⁹.

The idea

SAT asks whether a formula in conjunctive normal form (an AND of ORs of literals) can be made true. A formula A is valid exactly when ¬A is unsatisfiable, so a SAT solver is also a theorem prover. Resolution: from (C ∨ p) and (D ∨ ¬p) infer (C ∨ D); deriving the empty clause □ proves unsatisfiability. DPLL guesses values, propagates forced ones and backtracks; CDCL also learns a new clause from every conflict so that it never repeats a mistake ¹⁵⁹.

Worked example

What it changed

SAT became the reference problem of complexity theory and, in practice, a workhorse for checking hardware and software. In 2016 a SAT solver showed that the numbers 1 to 7824 can be coloured red and blue with no single-coloured Pythagorean triple a² + b² = c², but 1 to 7825 cannot; the proof certificate was about 200 terabytes ¹⁶⁰. In 2020 SAT solving settled Keller’s conjecture in dimension 7, its last open case ¹⁶¹.

Misconceptions

• NP-complete means SAT solvers are useless in practice.Worst cases are hard, yet CDCL solvers settled the Pythagorean triples problem and Keller’s conjecture ^160,161.
• Cook alone discovered NP-completeness.Levin found it independently ¹⁵⁸.

Further reading: Handbook vol. 9 (Siekmann, “Computational Logic”; Fortnow & Homer, “Computational Complexity”) ¹²⁷.

Sources for ✱21: 106, 127, 156–161.

✱22Proof assistants, computing, AI

Edinburgh · Cambridge · Paris · Marseille · LCF 1972/79 · Isabelle 1986 · Coq 1989 → Rocq 2025 · Lean 2013 · Codd 1970 · Prolog 1972 · Pnueli 1977 ^{162,163,164,165,166,167,168}

Context

Next to automatic provers grew interactive proof assistants, where a person guides the proof and a small trusted kernel checks every step. Robin Milner’s LCF began at Stanford in 1972; Edinburgh LCF (1979) introduced the ML language, designed so that theorems could only be produced by the kernel’s rules ¹⁶². HOL, Isabelle (Paulson, from 1986) and Coq (1989) followed ¹⁶³; Coq was renamed Rocq, and Rocq 9.0 (March 2025) was the first release under the new name ¹⁶⁴. Leonardo de Moura started Lean in 2013; Lean 4 was released in 2023, the same year the Lean Focused Research Organization was founded ¹⁶⁵. Its community library, mathlib, holds hundreds of thousands of theorems ¹⁶⁹.

Logic also moved into everyday computing. Codd’s relational model of databases (1970) made queries into first-order formulas ¹⁶⁶. Prolog (Colmerauer and Roussel, Marseille, 1972; Kowalski) ran logic as a program, with resolution as execution ¹⁶⁷. Amir Pnueli brought temporal logic to program verification in 1977, and model checking (Clarke and Emerson; Queille and Sifakis, 1981–82) automated it ^168,170.

The idea

A proof assistant stores definitions and theorems as terms in a type theory (✱20). You state a theorem; you supply a proof term directly or build it with tactics; the kernel type-checks the result. Trust rests on the small kernel, the axioms, and on whether the formal statement says what you meant ^162,153.

Worked example

theorem and_swap (p q : Prop) : p ∧ q → q ∧ p :=
  fun ⟨hp, hq⟩ => ⟨hq, hp⟩

theorem and_swap' (p q : Prop) : p ∧ q → q ∧ p := by
  intro h            -- assume p ∧ q        (→ introduction)
  exact ⟨h.2, h.1⟩   -- take it apart, rebuild in the other order

What it changed

Landmark theorems have been checked by machine: the Four Colour Theorem in Coq (Gonthier and Werner, 2005) ¹⁷¹, the Feit–Thompson theorem (2012) ¹⁷², the Kepler conjecture (Flyspeck, 2014; paper 2017) ¹⁷³ and Scholze’s Liquid Tensor Experiment in Lean (2022) ¹⁷⁴. Machine learning has joined formal logic. At the 2024 International Mathematical Olympiad, DeepMind’s AlphaProof reached silver-medal standard, proving its answers in Lean after the problems were translated into Lean by hand ¹⁷⁵. In 2025, systems reached gold-medal standard in natural language, graded by people ¹⁷⁶, and Harmonic’s Aristotle produced gold-level solutions as Lean proofs ¹⁷⁷. Logic-based AI has a longer history, from McCarthy’s proposals of 1959 to the nonmonotonic logics of 1980 ¹⁷⁸.

Misconceptions

• A machine-checked proof cannot be wrong.The checker guarantees the proof matches the formal statement. Whether that statement says what the mathematician meant, and whether the kernel and axioms deserve trust, still need human judgment; the LCF design keeps the trusted kernel small for that reason ¹⁶².
• The 2025 olympiad golds were all machine-verified.The natural-language results were graded by people; only the Lean-based ones were checked by a proof assistant ^176,177.

Further reading: Handbook vol. 9 (Harrison, Urban & Wiedijk on interactive theorem proving; Kowalski, “Logic Programming”; Minker, Seipel & Zaniolo, “Logic and Databases”) ¹²⁷.

Sources for ✱22: 127, 153, 162–178.