Keyboard shortcuts

Press or to navigate between chapters

Press S or / to search in the book

Press ? to show this help

Press Esc to hide this help

Logic

Reference notes on formal logic — the syntax, semantics, and proof theory of the systems that underpin mathematical reasoning. These pages are self-contained and general; other sections link in for definitions of language, model, satisfaction, and proof.

Contents

  1. Sentential (Propositional) Logic — propositional variables and the truth-functional connectives: syntax, semantics, deductive systems, and the metatheorems (soundness, completeness, compactness, decidability of validity).
  2. First-Order (Predicate) Logic — terms, predicates, and quantifiers over a domain: signatures, Tarskian structures, deductive systems, and the metatheoretic landmarks (Gödel completeness, compactness, Löwenheim–Skolem, undecidability, incompleteness).
  3. Second-Order and Higher-Order Logic — quantification over relations and functions and up a type hierarchy: standard vs. Henkin semantics, categoricity of and , and the resulting failure of completeness, compactness, and Löwenheim–Skolem.
  4. Intuitionistic Logic — the constructive alternative to classical logic: the BHK interpretation, failure of excluded middle, the Curry–Howard correspondence with computation, and Kripke/Heyting-algebra semantics.
  5. Paraconsistent Logic — logics that tolerate contradictions without exploding: rejection of ex contradictione quodlibet, truth-value gluts (LP, FDE), relevance logics, logics of formal inconsistency, and dialetheism.
  6. Axiomatic Set Theory (ZFC) — the standard first-order foundation of mathematics: the -language, the ZFC axioms, Russell's paradox and its resolution, the cumulative hierarchy, and the independence of CH and AC (Gödel's and Cohen forcing).
  7. Model Theory — the semantics of first-order logic as a subject in its own right: elementary equivalence and substructures, compactness constructions, quantifier elimination, categoricity (Morley's theorem), types and saturation, and applications to algebra and number theory.
  8. Proof Theory — the syntactic counterpart: formal proofs as mathematical objects — Hilbert/natural-deduction/sequent calculi, cut elimination and normalization, the Curry–Howard correspondence, substructural logics, ordinal analysis (Gentzen's ), reverse mathematics, and provability logic.
  9. Category Theory (Foundations of Mathematics) — the structural, arrows-first alternative to set-theoretic foundations: categories, functors, natural transformations, universal properties and the Yoneda lemma, and the topos-theoretic and homotopy-type-theoretic foundational programs.
  10. Topics — focused deep-dives into individual landmarks, starting with Gödel's Incompleteness Theorems.
  11. Remarks — cross-cutting subtleties, notably the apparent circularity between set theory and first-order logic (object theory vs. metatheory) and first-order logic's canonical status (Lindström's theorem).

Reading order

Sentential logic is the natural starting point: first-order logic is built on top of it by adding quantifiers, variables, and a richer notion of structure, and higher-order logic extends quantification further up the type hierarchy. Read Sentential (Propositional) Logic first, then First-Order (Predicate) Logic, then Second-Order and Higher-Order Logic. Intuitionistic Logic and Paraconsistent Logic are largely independent and can be read after sentential and first-order logic — they reinterpret the same languages by, respectively, dropping excluded middle (allowing truth-value gaps) and dropping explosion (allowing truth-value gluts). Axiomatic Set Theory (ZFC) is an application of first-order logic and should be read after First-Order (Predicate) Logic, on which its metatheory (incompleteness, Skolem's paradox) depends. Model Theory likewise builds directly on first-order logic — especially compactness and Löwenheim–Skolem — and is best read after it. Proof Theory is its syntactic mirror image and pairs naturally with it, building on the deductive systems of sentential and first-order logic and on the proof theory of intuitionistic logic.