Mathematical logic §

Step 1 — Why formalize? Natural-language arguments are ambiguous: “some”, “and”, “if” shift meaning with context. A formal language removes the ambiguity. A formula is a finite string of symbols, and “provable” becomes a precise, mechanically checkable relation. This is the foundation every later section builds on.

Step 2 — Propositional connectives. Each connective has a fixed truth function. The truth table below lists the value of a compound formula for every assignment of truth values to its atoms. A formula true on every row is a tautology (valid); one false on every row is a contradiction.

Note that $P \to Q$ is false only when $P$ is true and $Q$ is false — this is why “if it rains, the ground is wet” is not falsified by a dry day with no rain.

Step 3 — Quantifiers. First-order logic lets a formula bind variables. $\forall x\, P(x)$ says every object satisfies $P$; $\exists x\, P(x)$ says at least one does. Quantifiers have scope (the formula they bind) and interact: $\forall x\, \exists y\, R(x,y)$ (“everyone has a friend”) is not the same as $\exists y\, \forall x\, R(x,y)$ (“there is one friend of everyone”).

Step 4 — From formulas to truth. A propositional formula is evaluated by a valuation (an assignment of T/F to atoms). A first-order formula is evaluated by a structure (the next section). This split — syntax (the formula) versus semantics (its truth) — is the axis the whole field turns on.

Authoritative sources

• Stanford Encyclopedia of Philosophy: Propositional Logic
• Stanford Encyclopedia of Philosophy: First-Order Logic

Step 1 — The four ingredients. A formal system is fully specified by (i) an alphabet of symbols, (ii) a grammar deciding which strings are well-formed formulas, (iii) a set of axioms (wffs taken as true without proof), and (iv) inference rules (patterns that turn earlier formulas into new ones). For example, modus ponens is the rule: from $A$ and $A \to B$ infer $B$.

Step 2 — A proof is a tree of rule applications. Each formula in a proof cites either an axiom or a rule applied to earlier lines. Because every step is a local, checkable pattern, a whole proof can be verified by a machine that never “understands” the content.

The parse tree of the wff $(P \wedge (Q \to R))$ shows how the grammar recursively builds a formula from its subformulas:

The root is the outermost connective; leaves are the atomic propositions. The tree is what a parser produces and what a proof checker walks.

Step 3 — Provability is decidable. Given a formal system and a formula, “is there a proof of this formula?” is a well-defined question: enumerate all finite strings and check each for being a valid proof. This decidability of proof checking (as opposed to finding proofs) is what makes formal systems the substrate for machine-checked mathematics.

Authoritative sources

• Stanford Encyclopedia of Philosophy: Formalism

Step 1 — What a structure is. A structure for a language $\mathcal{L}$ is a set $D$ (the domain) together with an interpretation of every symbol: each constant is an element of $D$, each $n$-ary function is a map $D^n \to D$, each $n$-ary predicate is a subset of $D^n$. The diagram below shows a structure with domain $\{a, b, c\}$, a constant $c$, a unary function $f$, and a unary predicate $P$:

Here $P$ is true of $a$ and $c$ (green) and false of $b$; the function $f$ cycles the three elements.

Step 2 — Satisfaction. A formula is satisfied by a structure (written $\mathcal{M} \models \varphi$) when it is true under the interpretation. Atomic facts are read off directly: $\mathcal{M} \models P(a)$ because $a \in P$. Compound formulas are evaluated recursively, and quantifiers range over the domain: $\mathcal{M} \models \forall x\, P(x)$ holds only if every element of $D$ is in $P$ — false here, since $b \notin P$.

Step 3 — Completeness. Gödel’s completeness theorem says provability and universal truth coincide for first-order logic: $\Gamma \vdash \varphi$ iff $\Gamma \models \varphi$. This is deep and non-obvious; for second-order logic the two notions diverge (there are valid second-order sentences with no effective proof).

Step 4 — Compactness and Löwenheim–Skolem. Compactness says truth is “local”: if every finite piece of a theory is satisfiable, so is the whole theory. Löwenheim–Skolem says first-order logic cannot fix the size of a model: any theory with an infinite model has models of every infinite cardinality. Together they explain why first-order logic cannot characterize the natural numbers up to isomorphism — non-standard, and arbitrarily large, models always exist.

Authoritative sources

• A. Tarski (1933), Der Wahrheitsbegriff in den formalisierten Sprachen
• Stanford Encyclopedia of Philosophy: Model Theory
• Stanford Encyclopedia of Philosophy: The Completeness Theorem
• Stanford Encyclopedia of Philosophy: The Compactness Theorem

Step 1 — Proofs as objects. In proof theory a proof is a tree whose leaves are axioms and whose internal nodes are rule applications. The cut rule lets you reason through a lemma $L$: from $A \vdash L$ and $L \vdash C$ infer $A \vdash C$. Cuts make proofs short and readable, but they introduce an intermediate formula $L$ that is not forced by the conclusion.

Step 2 — Cut elimination. Gentzen’s theorem says every proof can be transformed, by a mechanical procedure, into an equivalent proof with no cuts. The animation below shows a proof that goes through a lemma $L$ (a cut) being rewritten into a direct proof that reaches $C$ without it:

Step 3 — Why it matters. Cut elimination yields the subformula property (only subformulas of the conclusion occur in the proof), which in turn gives consistency proofs: a consistent logic cannot prove a contradiction, because a cut-free proof of $A \wedge \neg A$ would have to contain both $A$ and $\neg A$ as subformulas of the conclusion in an impossible way. Gentzen used a transfinite version of this argument, indexed by ordinals below $\varepsilon_0$, to prove the consistency of Peano arithmetic — a result that cannot be proved inside the system itself (by the second incompleteness theorem).

Authoritative sources

• G. Gentzen (1936), Über die Zulässigkeit der Cut-Elimination
• Stanford Encyclopedia of Philosophy: Gentzen’s Proof Theory

Step 1 — Arithmetization. The key move is to encode syntax as arithmetic. Every formula and proof is assigned a natural number (its Gödel number), and “x is the Gödel number of a proof of y” becomes an ordinary, primitive-recursive relation on natural numbers. This is where the Computability and decidability machinery enters: provability is a computable (indeed decidable) relation.

The construction of the Gödel sentence proceeds in stages:

Step 2 — The Gödel sentence. The diagonal lemma guarantees a sentence $G$ such that the theory proves $G \leftrightarrow \neg \mathrm{Prov}_T(\ulcorner G\urcorner)$ — that is, $G$ asserts its own unprovability. If $T$ proved $G$, then $\mathrm{Prov}_T(\ulcorner G\urcorner)$ would be true, contradicting $G$; so a consistent $T$ does not prove $G$. But then $\neg \mathrm{Prov}_T(\ulcorner G\urcorner)$ is true, so $G$ is true. Hence $G$ is true but unprovable: the first incompleteness theorem.

Step 3 — The second theorem. Let $\mathrm{Con}(T)$ be the arithmetical sentence asserting that no proof of a contradiction exists. If $T$ proved $\mathrm{Con}(T)$, one could build a sentence that is provable exactly when $T$ is inconsistent, and the first theorem applied to it would force $T$ to be inconsistent. So a consistent $T$ cannot prove its own consistency.

Step 4 — What it means in practice. Incompleteness does not make mathematics unusable: it bounds what any single fixed axiom system can capture, and it explains why proof assistants and set theorists sometimes need new axioms (such as large cardinals) to settle independent statements like the continuum hypothesis.

Authoritative sources

• K. Gödel (1931), Über formal unentscheidbare Sätze der Principia Mathematica und verwandter Systeme I
• Stanford Encyclopedia of Philosophy: Gödel’s Incompleteness Theorems
• Stanford Encyclopedia of Philosophy: The Diagonal Lemma

Problem. A first-order theory $T$ has a model whose domain has exactly 5 elements. By which of the three central results of model theory (completeness, compactness, Löwenheim–Skolem) can you conclude that $T$ also has a model with infinitely many elements? State the reasoning in one or two sentences.