Logic

Job: formalize mathematical reasoning — syntax and semantics of propositional and predicate logic; set-theoretic foundations with independence phenomena (AC, CH).

Core

Logic separates what can be written (syntax), what is true in a structure (semantics), and what can be proved (deductive systems). Completeness theorems link the last two for first-order logic; incompleteness and independence show hard limits once arithmetic or set theory is strong enough.

Layer Content
Propositional formulas, valuations, SAT; completeness; compactness
Predicate (FOL) languages, structures, \(\models\); Gödel completeness
Proof theory Hilbert/ND/sequent systems; cut-elimination (pointer)
Model theory elementary embeddings, compactness, Löwenheim–Skolem
Set theory ZFC axioms; ordinals/cardinals; independence
Limits Gödel incompleteness; undecidability of FOL validity (Church)

Reading map

Page Focus
Propositional logic syntax, semantics, completeness, compactness
Predicate logic FOL structures; completeness; incompleteness pointer
Set theory ZFC; AC/CH independence contexts

Dependency order

  1. Propositional — Boolean skeleton
  2. Predicate — quantifiers and structures
  3. Set theory — foundation layer for ordinary math
  4. Model theory / proof theory / computability as specialized layers
  5. Category theory / topos theory for categorical logic

Where it appears

  • All of mathematics: implicit FOL + ZFC (or ETCS/HoTT alternatives)
  • Discrete math: proof patterns, Boolean algebra
  • CS/complexity interface: SAT as Boolean satisfiability; type systems via HoTT
  • HoTT: propositions-as-types alternative foundation

Signature results

Result Content
Compactness (prop/FOL) finitely satisfiable \(\Rightarrow\) satisfiable
Completeness (Gödel) FOL: \(\Gamma\vdash\phi\Leftrightarrow\Gamma\models\phi\)
Löwenheim–Skolem satisfiable FOL theory has countable model (countable language)
Incompleteness sufficiently strong recursively axiomatized arithmetic is incomplete
CH independence \(\mathrm{Con}(\mathrm{ZFC})\Rightarrow\mathrm{Con}(\mathrm{ZFC}+\mathrm{CH})\) and \(+\neg\mathrm{CH}\) (Gödel \(L\) + Cohen)

See it

Compactness \(\Rightarrow\) nonstandard models of arithmetic. Any finite subset of \(\{\,c>n:n\in\mathbb{N}\,\}\cup\mathrm{Th}(\mathbb{N})\) is satisfiable \(\Rightarrow\) whole set has a model with an infinite element. Same engine builds ultraproducts and nonstandard analysis skeletons.

Forcing (one-liner). Cohen forcing adds generic reals / collapses cardinals in Boolean-valued or poset-generic extensions while preserving ZFC — modern independence proofs are geometric/order-theoretic, not “just syntax.”

Check

State soundness vs completeness for a proof system.

Soundness: \(\Gamma\vdash\phi\Rightarrow\Gamma\models\phi\). Completeness: \(\Gamma\models\phi\Rightarrow\Gamma\vdash\phi\). FOL has both for standard systems; second-order logic with full semantics is incomplete for any effective proof system.

Why does completeness of FOL not contradict incompleteness of arithmetic?

Completeness: semantic consequence \(=\) provability in FOL. Incompleteness: a particular theory \(T\) (e.g. PA) has sentences undecided by \(T\), though each sentence or its negation is true in \(\mathbb{N}\) and thus a semantic consequence of the full theory of \(\mathbb{N}\) — which is not recursively axiomatizable.

Pitfalls

  • Second-order logic “categorical” characterizations (Dedekind arithmetic) sacrifice effective completeness.
  • Skolem paradox: countable models of ZFC still “think” uncountable sets exist (external vs internal cardinality).
  • AC is independent and contested constructively; many “existence” proofs use it silently.
  • Syntax vs meta-theory: consistency proofs need a stronger meta-system (2nd incompleteness).

Refs

Enderton, A Mathematical Introduction to Logic; Mendelson; Kunen / Jech (set theory); Marker (model theory); Shoenfield.

Next

Propositional logic · Predicate logic · Set theory · Discrete math · Category theory · HoTT