<!-- Generated from https://www.teclamairme.com/#group-T8 by readviews.py; never edited by hand. -->

# Glossary cards — Chapter ᚆ(H): The observation car

*Teclam Áirme, the Mathematical Compendium — a copy for AI readers of https://www.teclamairme.com/#group-T8, as of 2026-09-30. Links are relative to https://www.teclamairme.com/fortheaireaders/.*

[Guide for AI readers](index.md) · [The chapter](ch08.md)

*Logic: the Iverson bracket, Boolean algebra, and statements with known truth values. Each card: its symbol, type, one-line headline, the longer note, the reference entries it cites and the cards it links to.*

### the letter Uath — `ᚆ` {#g-og-uath}

*Ogham letter*

Ogham letter name meaning ‘horror’ or ‘fear’; the medieval glossators read it as the whitethorn.

Úath means ‘horror, fear’. It is unattested in the orthodox Irish inscriptions, and both its etymology and its original sound value are unclear; McManus has suggested [y]. The three Old Irish word-oghams, the Bríatharogaim ascribed to Morann mac Moín, to Mac ind Óc, and to Cú Chulainn, give condál cúan, “assembly of packs of hounds”; bánad gnúise, “blanching of faces”; and ansam aidche, “most difficult at night.” The Auraicept glosses sce, whitethorn, and gives both readings at once: “a meet of hounds is huath, that is, white-thorn; or because it is formidable for its thorns”—the Irish for formidable being uathmar, from the letter name itself. Modern tree lore and ogham divination descend from the medieval plant glosses by way of Robert Graves’s The White Goddess of 1948, which read the letter order as an ancient seasonal calendar of tree magic. Celtic scholarship rejects that reconstruction; the associations in circulation today are modern, not ancient.

Cites: [2.15](ch02-refs.md#r-2.15), [2.16](ch02-refs.md#r-2.16), [2.17](ch02-refs.md#r-2.17), [2.19](ch02-refs.md#r-2.19)

### Fermat’s Last Theorem as a bit — `[∃ n, x, y, z ∈ ℤ⁺, n > 2 : xⁿ + yⁿ = zⁿ]` {#g-fermat}

*Integer or rational*

Asserted false in a margin about 1637; shown false when Wiles proved the theorem (announced 1993, completed with Richard Taylor in 1994, published 1995), so the bracket is 0 after 358 years.

Fermat’s Last Theorem says xⁿ + yⁿ = zⁿ has no solution in positive integers for any n > 2. Fermat claimed it in a margin about 1637; Euler settled n = 3, Sophie Germain the first case for a whole class of primes, Kummer the regular primes in ~1847; the tilde is there because the two standard histories date it differently: MacTutor has the paper reaching Dirichlet and the Berlin Academy in September 1847, while Wikipedia’s Regular prime gives 1850, the year of the published general proof in Crelle 40. Both are cited at 8.5. Andrew Wiles announced a proof in 1993 and closed a gap in it in September 1994 with his former student Richard Taylor; it appeared in 1995 as two papers in the Annals of Mathematics, one by Wiles and one by Taylor and Wiles. The bracket contains the negation, the existence of a solution, which is false, so its value is 0. A truth value is an integer, hence the tag.

Cites: [8.4](ch08-refs.md#r-8.4), [8.5](ch08-refs.md#r-8.5), [8.6](ch08-refs.md#r-8.6)

### four true statements — `[1+1=2] + [√2 ∉ ℚ] + [∞ many primes] + [ℵ₀ < 𝔠]` {#g-truths}

*Integer or rational*

Each bracket is 1, so these four sum to 4, and the law of excluded middle beside them makes the denominator 5; only established statements are placed below the line, which keeps the denominator provably nonzero.

Four theorems, each with an old proof: 1 + 1 = 2 (a consequence of the Peano axioms of 1889, and the famous proposition *54.43 on page 379 of the first volume of Whitehead and Russell’s Principia Mathematica in 1910, which remarks only that it will follow once addition has been defined; the proof itself arrives in the second volume, in 1912), √2 is irrational (attributed to the Pythagoreans, before 400 BC), there are infinitely many primes (Euclid, Elements IX.20, about 300 BC), and ℵ₀ < 𝔠 (Cantor, 1874 and the diagonal argument of 1891). Each bracket is 1, so the sum is 4. Only statements with proven truth values are placed in the denominator, which keeps it provably nonzero.

Cites: [8.10](ch08-refs.md#r-8.10), [8.11](ch08-refs.md#r-8.11), [8.14](ch08-refs.md#r-8.14), [8.8](ch08-refs.md#r-8.8), [8.9](ch08-refs.md#r-8.9)

See also: [cardinality of the natural numbers](ch27-cards.md#g-aleph0), [the axioms](ch08-cards.md#g-axioms), [cardinality of the continuum](ch27-cards.md#g-cont), [the diagonal argument](ch27-cards.md#g-diagonal), [Euclid’s theorem](ch08-cards.md#g-euclidprimes), [the law of excluded middle](ch08-cards.md#g-excluded), [Russell’s paradox](ch27-cards.md#g-russell), [square root of two](ch04-cards.md#g-sqrt2)

### the law of non-contradiction — `x ∧ ¬x` {#g-boolean}

*Integer or rational*

In Boolean algebra a statement x and its negation ¬x, joined by AND, give 0, whatever x is.

In the Boolean algebra that George Boole published in The Mathematical Analysis of Logic (1847) and The Laws of Thought (1854), ∧ is AND, ¬ is NOT, and x ∧ ¬x = 0 for every x: a statement and its negation cannot both hold. Aristotle called this principle, now known as the law of non-contradiction, the firmest of all principles. The value is the Boolean zero, which comes home as the integer 0, so it carries the integer tag.

Cites: [8.2](ch08-refs.md#r-8.2), [8.7](ch08-refs.md#r-8.7)

See also: [Boolean algebra](ch08-cards.md#g-boolealg)

### the law of excluded middle — `x ∨ ¬x` {#g-excluded}

*Integer or rational*

A statement or its negation is always true, so in Boolean algebra x ∨ ¬x = 1 for every x; the partner of the numerator’s zero.

The law of excluded middle, tertium non datur, is the third of the classical laws of thought and in Boole’s algebra (1847, 1854) reads x ∨ ¬x = 1: every statement is true or its negation is. It is the complement of the numerator’s x ∧ ¬x = 0, and in Boolean algebra the two laws are De Morgan duals (Augustus De Morgan, 1847). Intuitionists after Brouwer (1908) decline to assume it, which is why constructive mathematics will not prove that something exists by showing that its absence is contradictory. Its value is the Boolean 1, which comes home as the integer 1.

Cites: [8.16](ch08-refs.md#r-8.16), [8.20](ch08-refs.md#r-8.20), [8.7](ch08-refs.md#r-8.7)

See also: [Boolean algebra](ch08-cards.md#g-boolealg), [the law of non-contradiction](ch08-cards.md#g-boolean), [De Morgan’s laws](ch08-cards.md#g-demorgan)

### Iverson bracket — `[ · ]` {#g-iverson}

*Function or operator*

1 if the statement inside is true and 0 if it is false (Iverson 1962, popularized by Knuth).

The Iverson bracket [P] equals 1 when the statement P is true and 0 when it is false. Kenneth Iverson introduced the notation in his 1962 book A Programming Language, restricted to a single relation in parentheses; the square brackets and the generality are Donald Knuth’s, who campaigned for them in a 1992 article, Two Notes on Notation. It is a function from statements to integers rather than a number, so it is tagged as an operator, and the chapters that use it (this one, D, G, and the epilogue) treat its output as an ordinary integer.

Cites: [8.1](ch08-refs.md#r-8.1)

### the symbols of logic — `∀ ∃ ¬ ∧ ∨ ⇒ ⇔` {#g-logicsyms}

*Function or operator*

For all, there exists, not, and, or, implies, if and only if: the seven signs from which logic builds its statements.

The quantifiers ∀ (for all) and ∃ (there exists) were introduced by Gerhard Gentzen in 1935 and Giuseppe Peano in 1897 respectively, Gentzen’s by analogy with Peano’s; Frege’s Begriffsschrift (1879) had already invented quantification, in a two-dimensional notation of which only the turnstile survives. The connective ∨ is Russell’s, from 1908, and ¬ and ∧ are Heyting’s, from 1930; ⇒ and ⇔ are Bourbaki’s, from 1954. The Fermat bracket in the numerator is read ∃ n, x, y, z ∈ ℤ⁺ (n > 2 ∧ xⁿ + yⁿ = zⁿ). They are notation, hence the tool tag.

Cites: [8.15](ch08-refs.md#r-8.15)

See also: [the turnstiles: provable and true](ch08-cards.md#g-turnstile)

### Gödel’s incompleteness theorems — `Con(ZFC)` {#g-godel}

*Function or operator*

Any consistent, effectively axiomatized system strong enough for arithmetic has true statements it cannot prove, and cannot prove its own consistency; so some brackets have a value that system itself can never read.

Kurt Gödel proved in 1931 that any consistent, effectively axiomatized theory containing arithmetic is incomplete (first theorem) and cannot prove the statement Con(T) expressing its own consistency (second theorem). Con(ZFC) is therefore a definite statement whose Iverson bracket has a value, 1 if set theory is consistent, that ZFC itself can never establish. It is the reason Chapter ᚆ(H) separates truth from proof within a formal system: a bracket can have a value that a given system cannot establish. A theorem, hence the tool tag.

Cites: [8.12](ch08-refs.md#r-8.12)

See also: [the axioms](ch08-cards.md#g-axioms), [Iverson bracket](ch08-cards.md#g-iverson), [the standard axioms of set theory](ch27-cards.md#g-zfc)

### the continuum hypothesis, undecided — `[CH]` {#g-chindep}

*Function or operator*

Cantor’s guess that no infinity sits between the integers and the reals is neither provable nor refutable from the usual axioms, if those axioms are consistent (Gödel 1938, in full 1940; Cohen 1963).

The continuum hypothesis, Cantor’s 1878 conjecture that 2^ℵ₀ = ℵ₁, was the first of Hilbert’s 1900 problems. Gödel showed in 1940 that, assuming the usual consistency background, CH cannot be refuted from ZFC; Cohen showed in 1963 that it cannot be proved from ZFC. Thus ZFC decides neither CH nor its negation. Each model of ZFC nevertheless makes CH either true or false (Gödel’s model satisfies it, Cohen’s does not); independence means only that ZFC’s axioms do not decide which. Chapter ᚚ(P) carries ℵ₁ and 𝔠 as objects. An independent statement, hence the tool tag.

Cites: [27.22](ch27-refs.md#r-27.22), [8.11](ch08-refs.md#r-8.11), [8.13](ch08-refs.md#r-8.13)

See also: [the first uncountable cardinal](ch27-cards.md#g-aleph1), [the axioms](ch08-cards.md#g-axioms), [the continuum hypothesis](ch27-cards.md#g-ch), [cardinality of the continuum](ch27-cards.md#g-cont), [Hilbert’s problems of 1900](ch28-cards.md#g-hilbert23), [the integers](ch01-cards.md#g-ints), [the real numbers](ch01-cards.md#g-reals), [the turnstiles: provable and true](ch08-cards.md#g-turnstile), [the standard axioms of set theory](ch27-cards.md#g-zfc)

### the axioms — `PA, ZFC` {#g-axioms}

*Function or operator*

Peano’s axioms (1889) for the natural numbers and Zermelo–Fraenkel set theory with choice (1908, 1922) for everything else: the ground the brackets stand on.

Giuseppe Peano published his axioms for the natural numbers in 1889, building on Dedekind’s 1888 analysis: zero, successor, and induction. Ernst Zermelo axiomatized set theory in 1908 and Abraham Fraenkel and Thoralf Skolem repaired it in 1922, giving ZF; with the axiom of choice it is ZFC, the default foundation of modern mathematics, in which 1 + 1 = 2 is a theorem and the truths in this chapter’s denominator are provable. Axioms are tools rather than values.

Cites: [8.14](ch08-refs.md#r-8.14), [8.20](ch08-refs.md#r-8.20)

See also: [the axiom of choice](ch27-cards.md#g-ac), [the natural numbers](ch01-cards.md#g-nats), [the turnstiles: provable and true](ch08-cards.md#g-turnstile), [the standard axioms of set theory](ch27-cards.md#g-zfc)

### the turnstiles: provable and true — `⊢, ⊨` {#g-turnstile}

*Function or operator*

⊢ φ says φ has a proof, ⊨ φ says φ is true in every model; Gödel’s completeness theorem of 1929 says the two agree for first-order logic.

Frege drew the turnstile ⊢ in the Begriffsschrift (1879) as his judgment stroke, and it now reads as syntactic consequence: Γ ⊢ φ means φ can be derived from Γ by the rules. The double turnstile ⊨ is semantic consequence: every model of Γ makes φ true. Gödel’s completeness theorem (1929) proves ⊢ and ⊨ coincide for first-order logic, and his incompleteness theorems of 1931 show that truth in arithmetic still outruns proof. The Iverson bracket of this chapter records whether a statement is true; the denominator’s four theorems are also provable (⊢). A relation, hence the tool tag.

Cites: [8.15](ch08-refs.md#r-8.15), [8.20](ch08-refs.md#r-8.20)

See also: [Iverson bracket](ch08-cards.md#g-iverson)

### De Morgan’s laws — `¬(x ∧ y) = ¬x ∨ ¬y` {#g-demorgan}

*Function or operator*

Negation swaps AND with OR: not (both) is (not one) or (not the other), and not (either) is (not one) and (not the other).

Augustus De Morgan stated the laws in modern form in Formal Logic (1847), though William of Ockham and Jean Buridan had them in the fourteenth century and Aristotle noticed cases. They are why this chapter’s x ∧ ¬x = 0, in the numerator, and x ∨ ¬x = 1, the fifth term of the denominator, are mirror images: negate one law and you get the other. In set theory they read (A ∩ B)ᶜ = Aᶜ ∪ Bᶜ, and in circuit design they let NAND gates build everything. A pair of identities, hence the tool tag.

Cites: [8.16](ch08-refs.md#r-8.16)

See also: [the law of non-contradiction](ch08-cards.md#g-boolean), [the law of excluded middle](ch08-cards.md#g-excluded)

### therefore, and the end of a proof — `∴, ∎` {#g-qedsyms}

*Function or operator*

∴ is therefore, ∵ is because, and the tombstone ∎ marks the end of a proof where older books wrote Q.E.D.

The three-dot therefore ∴ appears in Johann Rahn’s Teutsche Algebra (1659) and its inverse ∵ was reserved for because only in the nineteenth century. The tombstone or halmos ∎, closing a proof, was introduced, on his own account, by Paul Halmos, who took it from magazine typography; before it, proofs ended with Q.E.D., quod erat demonstrandum, Euclid’s ὅπερ ἔδει δεῖξαι. The four theorems in this chapter’s denominator each end with one. Punctuation of the framework, hence the tool tag.

Cites: [8.17](ch08-refs.md#r-8.17)

### Boolean algebra — `0, 1, ∧, ∨, ¬` {#g-boolealg}

*Function or operator*

The algebra of truth values George Boole published in 1847 and 1854, in which statements are 0 and 1 and can be added and multiplied; Shannon showed in 1937 that it is also the arithmetic of switching circuits.

George Boole gave logic an algebra in The Mathematical Analysis of Logic (1847) and The Laws of Thought (1854): a statement carries the value 0 or 1, and the connectives can be written arithmetically—in the two-element algebra x ∧ y is the product xy, ¬x is 1 − x, and x ∨ y is x + y − xy. That is what lets this chapter add and multiply brackets at all. Its two constants are the chapter’s numerator and the fifth term of its denominator: x ∧ ¬x = 0 and x ∨ ¬x = 1. Claude Shannon’s master’s thesis of 1937 showed that the same algebra describes relay and switching circuits.

Cites: [8.2](ch08-refs.md#r-8.2), [8.3](ch08-refs.md#r-8.3)

See also: [the law of non-contradiction](ch08-cards.md#g-boolean), [the law of excluded middle](ch08-cards.md#g-excluded)

### Euclid’s theorem — `∞ many primes` {#g-euclidprimes}

*Function or operator*

There are infinitely many primes; the proof is Elements IX.20, about 300 BC, and it is the third of the four brackets in this chapter’s denominator.

Euclid’s proof that the primes do not run out stands at Elements IX.20 and is conventionally dated to about 300 BC. Take any finite list of primes, multiply them together and add 1. No prime on the list divides the result, because each of them divides the product and would then have to divide 1 as well; so the result has a prime factor the list does not contain. The constructed number need not itself be prime, and the argument needs no contradiction, though it is often reported as one. The bracket around the statement is 1.

Cites: [8.10](ch08-refs.md#r-8.10)