Mathematical Logic

⚡ Key Takeaways

Mathematical logic is the rigorous study of formal systems, proof, and truth using mathematical methods. Its central achievements show that any sufficiently expressive consistent formal system is incomplete (Gödel), that first-order logic is complete and compact, and that the notions of "computable" and "provable" have precise mathematical definitions. It underlies the foundations of mathematics, computer science, and the theory of computation. Pioneered by Frege, Russell, Hilbert, Gödel, Tarski, Church, and Turing (c. 1879–1940s).

💡 The Core Insight

The same symbolic strings can be viewed in two utterly different ways: as purely formal marks manipulated by mechanical rules (syntax / provability, written $\vdash$ ), or as descriptions of structures that are true or false (semantics / truth, written $\models$ ). Mathematical logic is the systematic comparison of these two perspectives. When they coincide — provable iff true in all models — we have soundness and completeness. When they diverge — true but unprovable — we have incompleteness. The entire field lives in the gap and the bridge between $\vdash$ and $\models$ .

DefinitionFirst-Order Language

A first-order language $\mathcal{L}$ consists of:

Logical symbols: variables $x, y, z, \dots$ ; connectives $\neg, \wedge, \vee, \to, \leftrightarrow$ ; quantifiers $\forall, \exists$ ; equality $=$ ; parentheses.
Non-logical symbols (the signature): a set of constant symbols $c_i$ , function symbols $f_i$ (each with an arity), and relation/predicate symbols $R_i$ (each with an arity).

Terms are built from variables and constants by applying function symbols. Formulas are built from atomic formulas ( $R(t_1,\dots,t_n)$ and $t_1 = t_2$ ) using connectives and quantifiers. A sentence is a formula with no free variables.

DefinitionStructure and Satisfaction

An $\mathcal{L}$ -structure $\mathcal{M} = (M, \cdot^{\mathcal{M}})$ consists of a nonempty domain $M$ together with interpretations: each constant $c$ becomes an element $c^{\mathcal{M}} \in M$ , each $n$ -ary function $f$ becomes $f^{\mathcal{M}}: M^n \to M$ , each $n$ -ary relation $R$ becomes $R^{\mathcal{M}} \subseteq M^n$ . The satisfaction relation $\mathcal{M} \models \varphi[s]$ (" $\mathcal{M}$ satisfies $\varphi$ under variable assignment $s$ ") is defined by recursion on formula structure (Tarski's definition of truth):

TheoremGödel's Completeness Theorem (1929)

For first-order logic, syntactic and semantic consequence coincide:

TheoremCompactness Theorem

A set of first-order sentences $\Sigma$ has a model if and only if every finite subset of $\Sigma$ has a model.

TheoremGödel's First Incompleteness Theorem (1931)

Let $T$ be any consistent, effectively axiomatized theory that interprets a modest fragment of arithmetic (Robinson arithmetic $Q$ ). Then there is a sentence $G_T$ (the Gödel sentence) such that neither $G_T$ nor $\neg G_T$ is provable in $T$ :

TheoremGödel's Second Incompleteness Theorem

For a theory $T$ as above, let $\mathrm{Con}(T)$ be the arithmetical sentence expressing the consistency of $T$ . Then:

ProofSketch of the First Incompleteness Theorem

1. Arithmetization (Gödel numbering). Assign to every symbol, formula, and finite sequence of formulas a distinct natural number. Syntactic properties ("is an axiom", "is a valid inference") become arithmetical properties of these numbers. 2. Representability. Because $T$ interprets arithmetic, every computable relation is representable in $T$ : there is a formula $\mathrm{Prf}_T(p, x)$ that is provable exactly when $p$ codes a $T$ -proof of the formula coded by $x$ . Define the provability predicate $\mathrm{Prov}_T(x) := \exists p\,\mathrm{Prf}_T(p,x)$ . 3. The Diagonal (Fixed-Point) Lemma. For any formula $\psi(x)$ with one free variable, there is a sentence $\sigma$ such that

T \vdash \sigma \leftrightarrow \psi(\ulcorner\sigma\urcorner),

where $\ulcorner\sigma\urcorner$ is the numeral for the Gödel number of $\sigma$ . The sentence "talks about itself." 4. Construct the Gödel sentence. Apply diagonalization to $\psi(x) := \neg\,\mathrm{Prov}_T(x)$ , obtaining $G_T$ with $T \vdash G_T \leftrightarrow \neg\mathrm{Prov}_T(\ulcorner G_T\urcorner)$ . Thus $G_T$ says "I am not provable." 5. Unprovability of $G_T$ . Suppose $T \vdash G_T$ . Then there is a proof, so $\mathrm{Prov}_T(\ulcorner G_T\urcorner)$ holds and is provable, hence $T \vdash \mathrm{Prov}_T(\ulcorner G_T\urcorner)$ . But $T \vdash G_T \to \neg\mathrm{Prov}_T(\ulcorner G_T\urcorner)$ . Together these give $T \vdash \neg\mathrm{Prov}_T(\ulcorner G_T\urcorner)$ and its negation — contradiction with consistency. 6. Unprovability of $\neg G_T$ . Symmetric argument using $\omega$ -consistency (Rosser's trick replaces this with plain consistency). $\blacksquare$

∎

mathematician · Kurt Gödel | 1906–1978

Born in Brünn (Brno), Gödel was the most consequential logician of the twentieth century. His 1929 doctoral thesis proved the completeness theorem; in 1931, aged 25, he published Über formal unentscheidbare Sätze, the incompleteness theorems that dismantled Hilbert's program of finding a complete, provably consistent foundation for all mathematics. He later proved the relative consistency of the Axiom of Choice and the Continuum Hypothesis with ZF set theory via the constructible universe $L$ . Emigrating to Princeton's Institute for Advanced Study, he became a close friend of Einstein. Plagued by paranoia in later life, he died of self-starvation. His work demonstrated, with mathematical certainty, the inherent limits of formal axiomatic reasoning.

🧠 Intuition

Think of a formal theory as a game with tokens. The axioms are starting positions; the inference rules are legal moves; a "theorem" is any position reachable by legal play. Soundness says you can never reach a false position. Completeness (for FOL) says every valid position is reachable. Now Gödel's insight: because the rules of the game are mechanical, the game can describe itself — you can write down, inside arithmetic, a statement of the form "this very statement has no winning line." If the game could reach it, that would prove it false (it claims unreachability); if the game could reach its denial, the game proves a falsehood. So the statement is true but stranded — outside the reach of the rules. There is no contradiction, only an inherent horizon: every consistent rule-system rich enough to do arithmetic can see truths it cannot grasp. Compactness has a different flavor: it says infinitely many constraints can be satisfied as long as no finite clump of them clashes. This is the engine behind nonstandard models — e.g., a structure satisfying every true statement of arithmetic plus "there is a number bigger than $0, 1, 2, \dots$ ", yielding infinite natural numbers.

Figure

The bridge and the gap between syntax (

\vdash

) and semantics (

\models

)

```svg

```

ExampleUsing Compactness to Build a Nonstandard Model

Given: Let $\mathrm{Th}(\mathbb{N})$ be the set of all first-order sentences true in the standard natural numbers $(\mathbb{N}, +, \times, <, 0, 1)$ . Add a new constant symbol $c$ and the infinite set of sentences

\Sigma = \mathrm{Th}(\mathbb{N}) \cup \{\, c > 0,\ c > 1,\ c > 2,\ \dots \,\}.

Goal: Show $\Sigma$ has a model, and describe it.

Steps: 1. Take any finite subset $\Sigma_0 \subseteq \Sigma$ . It mentions only finitely many constraints $c > n$ , the largest being $c > N$ for some $N$ . 2. Interpret $c$ as the standard number $N+1$ in $\mathbb{N}$ . Then $\mathbb{N}$ (with this interpretation) satisfies $\mathrm{Th}(\mathbb{N})$ and all of $c > 0, \dots, c > N$ . So $\Sigma_0$ is satisfiable. 3. Since every finite subset is satisfiable, by Compactness ([4]) the whole set $\Sigma$ is satisfiable. 4. A model $\mathcal{M} \models \Sigma$ satisfies every truth of $\mathbb{N}$ yet contains an element $c^{\mathcal{M}}$ exceeding every standard numeral.

Answer: $\boxed{\text{A nonstandard model of arithmetic exists, containing "infinite" natural numbers.}}$ This shows first-order logic cannot pin down $\mathbb{N}$ uniquely (it is not categorical).

ExampleCounting Models via Truth Tables — Propositional Satisfiability

Given: The propositional formula $\varphi = (p \to q) \wedge (q \to r) \wedge (p \vee r)$ over atoms $p, q, r$ .

Goal: Determine whether $\varphi$ is satisfiable and count its satisfying assignments (models).

Steps: Enumerate all $2^3 = 8$ truth assignments. Recall $a \to b$ is false only when $a$ is true and $b$ is false.

$p$	$q$	$r$	$p\to q$	$q\to r$	$p\vee r$	$\varphi$
T	T	T	T	T	T	T
T	T	F	T	F	T	F
T	F	T	F	T	T	F
T	F	F	F	T	T	F
F	T	T	T	T	T	T
F	T	F	T	F	F	F
F	F	T	T	T	T	T
F	F	F	T	T	F	F

Three rows make $\varphi$ true.

Answer: $\boxed{\varphi \text{ is satisfiable with exactly } 3 \text{ models}}$ — namely $(T,T,T)$ , $(F,T,T)$ , $(F,F,T)$ . Note all three have $r = T$ ; indeed $\varphi \models r$ (one can check $\varphi \wedge \neg r$ is unsatisfiable).

⚠️ Common mistake

"Incompleteness means mathematics is broken / arbitrary / unknowable." False. Incompleteness is a precise relative statement: a given consistent, effectively axiomatized theory $T$ cannot prove certain truths expressible in its language. It does not say there are absolutely unknowable mathematical facts, nor that any particular theorem of ordinary mathematics is in doubt. We can always extend $T$ (e.g., add $G_T$ as a new axiom) — but the new system has its own, new Gödel sentence. The lesson is about formal systems, not about truth itself.

"Gödel proved you can't trust mathematics." No — Gödel's theorems are themselves theorems of mathematics, proved with complete rigor. They presuppose, not undermine, the reliability of finitary reasoning.

"Completeness and Incompleteness contradict each other." They concern different things. Completeness (FOL) is about logical validity: provable = true-in-all-models. Incompleteness is about a fixed theory $T$ failing to settle every sentence: there are sentences true in the standard model $\mathbb{N}$ but not provable from $T$ 's axioms. Both hold simultaneously.

CounterexampleSecond-Order Logic Lacks Completeness and Compactness

The completeness ([3]) and compactness ([4]) theorems are special to first-order logic. In second-order logic (where quantifiers range over sets/relations, not just individuals), one can write a single sentence whose only model (up to isomorphism) is $(\mathbb{N}, +, \times)$ — second-order arithmetic is categorical. If second-order logic had compactness, the nonstandard-model construction above would apply, contradicting categoricity. Hence second-order logic is not compact and has no sound, complete, effective proof system. This trade-off — first-order logic's weakness in expressive power buys it completeness and compactness — is one of the deepest structural facts of the subject.

connection

Mathematical logic is the connective tissue of foundational mathematics and theoretical computer science.

Set Theory supplies the universe in which all of mathematics is interpreted; the ZFC axioms, the Axiom of Choice, and the Continuum Hypothesis are studied with logical tools (forcing, inner models).
Computability Theory and the Church–Turing Thesis make "effectively axiomatized" and "computable" precise; the unsolvability of the Halting Problem is a recursion-theoretic twin of incompleteness.
Proof Theory analyzes derivations as combinatorial objects (Gentzen's Sequent Calculus, cut-elimination, ordinal analysis measuring a theory's strength).
Model Theory studies the structures satisfying theories — compactness, Löwenheim–Skolem Theorem, elimination of quantifiers, and stability theory.
<a class="wiki-link" href="/wiki/cs-arch-boolean-algebra">Boolean Algebra</a> and Lambda Calculus link propositional logic and proof to algebra and programming; the Curry–Howard Correspondence identifies proofs with programs and propositions with types.

🔬 Where this appears

⏳ History

- 1854 — George Boole, The Laws of Thought, algebraizes propositional logic, founding Boolean Algebra.

- 1879 — Gottlob Frege's Begriffsschrift introduces quantifiers and a full formal language; the birth of modern predicate logic.

- 1889–1895 — Peano axiomatizes arithmetic; Cantor and Dedekind develop set theory and the theory of the infinite.

- 1901 — Russell's paradox (

\{x : x \notin x\}

) exposes a contradiction in naive set theory, triggering the foundational crisis.

- 1910–1913 — Whitehead & Russell's Principia Mathematica attempts to derive all mathematics from logic (logicism).

- 1920s — Hilbert's program seeks a complete, consistent, decidable axiomatization of mathematics, provable by finitary means.

- 1929–1931 — Gödel proves completeness (thesis) and then the two incompleteness theorems, refuting Hilbert's program in its original form.

- 1933–1936 — Tarski gives the formal semantic definition of truth; Church (lambda calculus) and Turing (Turing machines) independently define computability and prove the undecidability of the Entscheidungsproblem.

- 1938–1963 — Gödel proves

\mathrm{Con}(ZF)\to\mathrm{Con}(ZFC + CH)

via

L

; Cohen invents forcing (1963) to prove the independence of CH and AC, completing the picture that CH is undecidable in ZFC.

open-problem

The boundary of provability remains an active frontier.

Concrete independence. Beyond the self-referential Gödel sentence, are there natural, mathematically interesting statements independent of strong theories? Yes — the Paris–Harrington theorem (a Ramsey-type statement) and Goodstein's theorem are true but unprovable in Peano Arithmetic, requiring transfinite induction up to $\varepsilon_0$ . Identifying the precise proof-theoretic strength (ordinal analysis) of strong theories like full second-order arithmetic and ZF is open.
The Continuum Hypothesis. Shown undecidable in ZFC (Gödel + Cohen). Whether there is a correct answer — and what new axioms (large cardinals, forcing axioms, Woodin's $\Omega$ -logic) might settle it — is a deep open philosophical and mathematical question.
$\mathbf{P}$ vs $\mathbf{NP}$ . Whether there is a tractable algorithm for satisfiability is the central open problem of computer science, with logical content (descriptive complexity characterizes complexity classes by logical expressibility).
Reverse mathematics asks which axioms are necessary to prove ordinary theorems, calibrating them against a hierarchy of subsystems of second-order arithmetic — a program far from complete.

Formal Statement

Why It Holds

Building Intuition

Worked Examples

Common Misconceptions

Connections

Real-World Applications

Historical Development

Subtleties & Limits

See Also