Logic — flashcards
Everything on this map that touches Logic: its own shape, its concepts, the statements resting on them, and the lens edges crossing into it.
Theorems 5
State: Gödel's first incompleteness theorem.
Any consistent, effectively axiomatised theory interpreting arithmetic contains a sentence neither provable nor refutable in it.
derived from st/godel-1 by the statement rule
State: Independence of the continuum hypothesis.
If ZFC is consistent, then neither CH nor its negation is provable from ZFC — Gödel 1940 for one direction, Cohen 1963 for the other.
derived from st/ch-independent by the statement rule
State: Independence of the axiom of choice.
If ZF is consistent, both ZFC and ZF plus the negation of choice are consistent. In Lean, choice is an axiom rather than a theorem, which makes the dependency mechanically visible.
derived from st/ac-independent by the statement rule
State: The Curry–Howard correspondence.
Propositions correspond to types, proofs to terms, and proof normalisation to evaluation. In a dependently typed proof assistant this is not an analogy but the implementation.
derived from st/curry-howard by the statement rule
State: The Ax–Kochen theorem.
For each degree d, Artin's conjecture on forms over ℚ_p holds for all but finitely many p — proved by model theory, by showing ℚ_p and 𝔽_p((t)) become elementarily equivalent as p grows.
derived from st/ax-kochen by the statement rule
Names and dates 5
Gödel's first incompleteness theorem — who, and when?
Kurt Gödel, 1931.
derived from st/godel-1 by the attribution rule
Independence of the continuum hypothesis — who, and when?
Paul Cohen, 1963.
derived from st/ch-independent by the attribution rule
Independence of the axiom of choice — who, and when?
Paul Cohen, 1963.
derived from st/ac-independent by the attribution rule
The Curry–Howard correspondence — who, and when?
Haskell Curry, then William Howard, 1934 (Curry), 1969 (Howard).
derived from st/curry-howard by the attribution rule
The Ax–Kochen theorem — who, and when?
James Ax and Simon Kochen, 1965.
derived from st/ax-kochen by the attribution rule
Connections 12
Why is Algebra taught before Logic? [Pedagogical]
Formal proof and logic are usually introduced once symbolic fluency exists.
derived from pedagogical:algebra→logic by the connection rule
Why is Logic taught before Computation? [Pedagogical]
Algorithms are often taught as precise logic, after a foundations course.
derived from pedagogical:logic→computation by the connection rule
What does Arithmetic need from Logic before it can even be stated? [First principles]
The natural numbers are built from a formal base (e.g. Peano axioms over logic and sets).
derived from first-principles:logic→arithmetic by the connection rule
What does Combinatorics need from Logic before it can even be stated? [First principles]
Counting is direct set-theoretic reasoning — it doesn't actually need arithmetic first.
derived from first-principles:logic→combinatorics by the connection rule
What does Computation need from Logic before it can even be stated? [First principles]
Computability is a question about formal systems, logically prior to any physical machine.
derived from first-principles:logic→computation by the connection rule
What is the correspondence between Propositional & predicate calculus and Typed λ-calculus? [Correspondences]
Propositions ↔ types, proofs ↔ programs, proof normalisation ↔ program evaluation. Logic and computation turn out to be the same subject written twice.
derived from correspondences:propositional-calculus→lambda-calculus by the connection rule
What is the correspondence between Boolean algebra and Topological spaces? [Correspondences]
Boolean algebras ↔ compact totally disconnected Hausdorff spaces, as an anti-equivalence of categories. Pure logic ↔ pure geometry.
derived from correspondences:boolean-algebra→topology by the connection rule
What is the correspondence between Propositional & predicate calculus and Peano arithmetic? [Correspondences]
Formulas and proofs ↔ natural numbers, so that provability becomes an arithmetic relation. This is what lets arithmetic talk about itself.
derived from correspondences:propositional-calculus→peano by the connection rule
What is the correspondence between Turing machines / P vs NP and Gödel's incompleteness theorems? [Correspondences]
The halting problem's undecidability yields incompleteness directly: if provability were complete, halting would be decidable.
derived from correspondences:turing-machine→godel-incompleteness by the connection rule
Gödel's incompleteness theorems and Non-Euclidean geometry look like one thing. What separates them? [Forks]
Your objection, and it was right: axiomatic independence is not Gödelian self-reference. One is a choice the axioms leave open; the other is a statement the system cannot settle about itself.
derived from forks:godel-incompleteness→noneuclidean by the connection rule
Zermelo–Fraenkel set theory and Axiom of choice look like one thing. What separates them? [Forks]
The third return, and the one where you named the schema explicitly rather than just using it. ZFC and ZF¬C are both consistent if ZF is.
derived from forks:set-theory→axiom-of-choice by the connection rule
Zermelo–Fraenkel set theory and Continuum hypothesis look like one thing. What separates them? [Forks]
Same shape again: Gödel showed CH cannot be disproved, Cohen that it cannot be proved. A fork you reached for but did not develop — the thread stalled for want of forcing.
derived from forks:set-theory→continuum-hypothesis by the connection rule
Concepts 6
What is Propositional & predicate calculus, in one sentence?
Formal systems for reasoning, and the proofs expressible inside them.
derived from propositional-calculus by the concept rule
What is Boolean algebra, in one sentence?
The algebraic structure of truth values, meets, joins and complements.
derived from boolean-algebra by the concept rule
What is Gödel's incompleteness theorems, in one sentence?
No consistent formal system strong enough for arithmetic can prove all truths about itself.
derived from godel-incompleteness by the concept rule
What is Zermelo–Fraenkel set theory, in one sentence?
The standard foundation: sets built from the empty set by a short list of construction axioms.
derived from set-theory by the concept rule
What is Axiom of choice, in one sentence?
Given any family of nonempty sets, a set can be formed by picking one element from each. Independent of ZF: assuming it and denying it both give consistent theories.
derived from axiom-of-choice by the concept rule
What is Continuum hypothesis, in one sentence?
There is no cardinality strictly between the integers and the reals. Gödel and Cohen together showed it can be neither proved nor refuted from ZFC.
derived from continuum-hypothesis by the concept rule
Shape of the area 1
Logic: what kind of question does it answer well, and what kind does it answer badly?
Good at — Limitative results and relative consistency. What a system cannot prove, which statements are independent of it, what is undecidable, and what follows if you assume something unprovable. It is the only area that can answer questions *about* the map.
Bad at — Producing mathematics. It rarely settles an ordinary mathematical question, and having shown two alternatives are equally consistent, it has nothing whatever to say about which one is right.
derived from logic by the area rule