42.01.05 · mathematical-logic / first-order-logic-completeness

A Deductive Calculus for First-Order Logic and Soundness

shipped3 tiersLean: none

Anchor (Master): Enderton 2001 *A Mathematical Introduction to Logic* 2e §2.4-2.5 (the full Hilbert calculus with the equality axioms and normal models, the generalization theorem, the deduction theorem, the soundness theorem, and the syntactic notions of consistency and inconsistency that the completeness theorem will tie to satisfiability); Mendelson 2015 *Introduction to Mathematical Logic* 6e (CRC) Ch. 2 (the predicate calculus, its axioms and the generalization rule, the deduction theorem with its eigenvariable restriction); Shoenfield 1967 *Mathematical Logic* (Addison-Wesley) Ch. 2-3 (an economical Hilbert system, the equality and substitution axioms); van Dalen 2013 *Logic and Structure* 5e (Springer) Ch. 2-3 (natural deduction for first-order logic as an alternative calculus); Takeuti 1987 *Proof Theory* 2e (North-Holland) Ch. 1 (the sequent calculus LK, the cut rule, and the cut-elimination theorem)

Intuition Beginner

The previous unit answered when a sentence is true: you pick a world, fix what every symbol means, and check. That is a question about meaning. This unit answers a completely different question, one that never mentions meaning at all: when can a sentence be proved? A proof here is a chain of written lines, each one either an assumption you started with, or a fixed logical starting-line that is allowed no matter what, or a single mechanical step that reads two earlier lines and writes a third. The last line of the chain is what you proved.

The striking thing is that this rule-pushing game refuses to look at any world. It never asks what the objects are or what the symbols mean. It only checks the shape of the lines. A clerk who knew no mathematics could verify a proof by pattern-matching alone, and a machine certainly can. So we now have two separate notions sitting side by side: "true in every world," which is about meaning, and "reachable by the chain game," which is about shape.

A natural worry is whether the shape game might cheat — whether it could prove something that is actually false in some world. This unit shows it cannot. Every starting-line is true in every world, and the one mechanical step never turns truths into a falsehood. So everything you can prove really is true everywhere. That guarantee is called soundness. The harder reverse question — is everything true-everywhere also provable? — is saved for the next unit.

Visual Beginner

A proof is a vertical list of lines. Each line is justified by one of exactly three things: it is an assumption, it is a free logical starting-line, or it is built from two lines already above it by the single detachment step. The diagram shows a short proof and how each line earns its place.

   THE ONLY MECHANICAL STEP (detachment):

        if you have written     A
        and you have written     A then B
        you may write down       B

   A SHORT PROOF of  q  from the assumptions  { p ,  p then q }:

      line 1     p                  (an assumption)
      line 2     p then q           (an assumption)
      line 3     q                  (detachment from lines 1 and 2)
                 ^^^ the last line is what was proved

   NOTHING in this proof ever asked what p or q MEAN.

Read it top to bottom. Lines 1 and 2 are just the assumptions, copied in. Line 3 is the only real move: it sees the pattern "A" on line 1 and "A then B" on line 2, and writes "B." The whole proof is finite, every line is justified by a line above it or by a fixed rule, and at no point does anyone decide whether $p$ is true.

line	what it says	why it is allowed
1	$p$	it is an assumption
2	$p$ then $q$	it is an assumption
3	$q$	detachment from lines 1 and 2

Because the rule only matches shapes, the same three-line proof works whatever $p$ and $q$ stand for.

Worked example Beginner

We build a complete proof of one specific sentence and then check, by hand, that the move we relied on is safe in every world. The target: from the single assumption "for-all $x$ , ( $x$ is happy)," prove " $a$ is happy," where $a$ is one fixed name.

Step 1. Write the assumption as the first line: "for-all $x$ , ( $x$ is happy)." This is our only starting material.

Step 2. Use a free logical starting-line. One of the allowed starting-lines says: from "for-all $x$ , (something about $x$ )" you may pass to "the same thing with the name $a$ put in for $x$ ." Written as a line it reads: "( for-all $x$ , ( $x$ is happy) ) then ( $a$ is happy)." We are allowed to write this down for free, because it is one of the fixed logical axioms.

Step 3. Now we have two lines: the assumption "for-all $x$ , ( $x$ is happy)," and the starting-line "( for-all $x$ , ( $x$ is happy) ) then ( $a$ is happy)." These match the detachment pattern: line 1 is "A," line 2 is "A then B." Apply detachment.

Step 4. Detachment writes the third line: " $a$ is happy." That is the target, so the proof is finished in three lines.

Step 5. Check the move is safe in any world. Suppose a world makes "for-all $x$ , ( $x$ is happy)" true. Then every object of that world is happy, and the object named $a$ is one of those objects, so " $a$ is happy" is true there too. The step never failed.

What this tells us: a single fixed starting-line ("drop the for-all to any name") plus detachment already proves a real fact, and the starting-line is true in every world for the same plain reason a universal claim covers each of its instances. The next sections turn "every starting-line is safe in every world" into the precise guarantee that proof can never outrun truth.

Check your understanding Beginner

Exercise (easy, multiple choice).

In a proof, what are the only three ways a line can earn its place?

A. It is true, it is short, or it is famous.

B. It is an assumption, a fixed logical starting-line, or a detachment step from two earlier lines.

C. It is checked in some world, then copied.

D. It is guessed, then verified by a truth table.

Hint

A proof is pure shape-matching. Recall the three justifications every line may carry.

Answer

B. Every line is one of: an assumption, a free logical starting-line, or the result of detachment applied to two lines already written. Feedback-correct: these three justifications are exactly what a clerk or a machine pattern-matches against. Feedback-wrong: truth, fame, length, and truth-table checks all refer to meaning, but a proof never consults meaning.

Formal definition Intermediate+

Fix a first-order language $L$ with equality and the syntax of 42.01.04 pending. The deductive calculus is Hilbert-style: many logical axioms, one rule. The logical axioms are all generalizations (prefixing zero or more $\forall$ 's) of formulas of the following groups, where $φ, ψ$ range over formulas, $x$ over variables, $t$ over terms substitutable for $x$ in $φ$ , and $u, v$ over variables ^{[Enderton §2.4]}:

(A1) (A2) (A3) (A4) (A5) (A6) every tautology (a formula that is a propositional tautology when its prime subformulas are read as atoms), \forall x φ \to φ_{t}^{x} (t substitutable for x in φ), \forall x (φ \to ψ) \to (\forall x φ \to \forall x ψ), φ \to \forall x φ (x not free in φ), u = u, u = v \to (φ \to φ^{'}),

where in (A6) $φ$ is atomic and $φ^{'}$ arises from $φ$ by replacing some occurrences of $u$ by $v$ . The single rule of inference is modus ponens (detachment): from $φ$ and $φ \to ψ$ infer $ψ$ . There is no separate quantifier-introduction rule; generalization is recovered as a derived rule below.

A deduction of $φ$ from a set $Γ$ of formulas is a finite sequence $⟨ α_{0}, \dots, α_{m} ⟩$ with $α_{m} = φ$ in which each $α_{i}$ is a logical axiom, a member of $Γ$ , or follows from two earlier entries $α_{j}, α_{k}$ ( $j, k < i$ ) by modus ponens. One writes $Γ ⊢ φ$ (" $Γ$ proves $φ$ "), and $⊢ φ$ for $\emptyset ⊢ φ$ (a theorem). The relation $⊢$ is the purely syntactic counterpart of the semantic $⊨$ of 42.01.04 pending, defined without any reference to structures or truth.

A set $Γ$ is inconsistent if $Γ ⊢ β$ for every formula $β$ ; equivalently (using a tautology axiom) if $Γ ⊢ β$ and $Γ ⊢ \neg β$ for some $β$ . Otherwise $Γ$ is consistent. A structure $A$ with an assignment $s$ is a model of $Γ$ if $A ⊨ γ [s]$ for all $γ \in Γ$ ; when $=$ is read as genuine identity, $A$ is a normal model, the only kind the equality axioms (A5)–(A6) are designed to be sound for.

Counterexamples to common slips Intermediate+

"Generalization is a basic rule of the calculus." It is not a primitive rule here; the only primitive rule is modus ponens. Generalization is a derived rule with a side condition (the variable must not be free in the premises). Treating it as unconditional licenses the false deduction ${φ} ⊢ \forall x φ$ from a formula with $x$ free.
"The instantiation axiom (A2) holds for every term $t$ ." It requires $t$ substitutable for $x$ in $φ$ . Without that, $\forall x \exists y (x \neq = y) \to \exists y (y \neq = y)$ would be an instance with $t = y$ , which is false in any two-element structure. Substitutability blocks the variable capture.
"Consistency means $Γ$ proves no contradiction of the form $β \land \neg β$ ." Equivalently, but the working definition is that $Γ$ does not prove every formula. The two agree because a single proved contradiction, via the tautology $\neg β \to (β \to γ)$ (A1) and modus ponens, proves an arbitrary $γ$ .
"The equality axioms make $=$ definable." They constrain its behavior to a congruence but do not define it. A structure may satisfy (A5)–(A6) with $=^{A}$ a coarser congruence than identity; such a non-normal model is repaired by quotienting, the maneuver the completeness theorem 42.01.06 pending uses to manufacture a normal model.

Key theorem with proof Intermediate+

The load-bearing metatheorem of the syntax-versus-semantics match is soundness: nothing the calculus proves can fail in a model. It is the routine half of the bridge whose hard half is completeness 42.01.06 pending, and its proof is the template for every "induction on a deduction" argument in the subject.

Theorem (Soundness). If $Γ ⊢ φ$ then $Γ ⊨ φ$ . In particular every theorem $⊢ φ$ is valid, and every satisfiable set of formulas is consistent.

Proof. It suffices to prove two lemmas: every logical axiom is valid (satisfied by every structure under every assignment), and modus ponens preserves satisfaction by a fixed pair $(A, s)$ . Granting these, fix $Γ, φ$ with a deduction $⟨ α_{0}, \dots, α_{m} = φ ⟩$ , and fix any $(A, s)$ with $A ⊨ γ [s]$ for all $γ \in Γ$ . Induct on $i$ to show $A ⊨ α_{i} [s]$ . If $α_{i} \in Γ$ this holds by choice of $(A, s)$ ; if $α_{i}$ is a logical axiom it holds by the validity lemma; if $α_{i}$ comes by modus ponens from earlier $α_{j}, α_{k} = (α_{j} \to α_{i})$ , then $A ⊨ α_{j} [s]$ and $A ⊨ (α_{j} \to α_{i}) [s]$ by induction, so $A ⊨ α_{i} [s]$ by the preservation lemma. At $i = m$ this is $A ⊨ φ [s]$ , so $Γ ⊨ φ$ .

Validity of the axioms. A generalization $\forall x_{1} \dots \forall x_{n} θ$ is valid iff $θ$ is, since $A ⊨ \forall x θ [s]$ for all $s$ iff $A ⊨ θ [s]$ for all $s$ ; so it is enough to validate each base form. (A1): a tautology is true under every assignment of truth values to its prime subformulas, hence under the actual truth values $A$ and $s$ supply, so it is satisfied by every $(A, s)$ . (A2): suppose $A ⊨ \forall x φ [s]$ ; then $A ⊨ φ [s (x ∣ a)]$ for all $a$ , in particular for $a = \overset{s}{ˉ} (t)$ , and the substitution lemma of 42.01.04 pending gives $A ⊨ φ_{t}^{x} [s]$ , using substitutability of $t$ . (A3): if $A ⊨ \forall x (φ \to ψ) [s]$ and $A ⊨ \forall x φ [s]$ , then for every $a$ both $A ⊨ (φ \to ψ) [s (x ∣ a)]$ and $A ⊨ φ [s (x ∣ a)]$ , whence $A ⊨ ψ [s (x ∣ a)]$ for all $a$ , i.e. $A ⊨ \forall x ψ [s]$ . (A4): if $x$ is not free in $φ$ and $A ⊨ φ [s]$ , then by the coincidence lemma of 42.01.04 pending $A ⊨ φ [s (x ∣ a)]$ for every $a$ , so $A ⊨ \forall x φ [s]$ . (A5): $\overset{s}{ˉ} (u) = \overset{s}{ˉ} (u)$ always. (A6): if $\overset{s}{ˉ} (u) = \overset{s}{ˉ} (v)$ , then replacing some occurrences of $u$ by $v$ in an atomic $φ$ leaves the tuple fed to the relation (or to identity) unchanged, so $A ⊨ φ [s] \Leftrightarrow A ⊨ φ^{'} [s]$ , and the conditional holds.

Preservation by modus ponens. If $A ⊨ φ [s]$ and $A ⊨ (φ \to ψ) [s]$ , then by the satisfaction clause for $\to$ either $A \neq ⊨ φ [s]$ or $A ⊨ ψ [s]$ ; the first is excluded, so $A ⊨ ψ [s]$ . $□$

Corollary (consistency from satisfiability). If $Γ$ has a model then $Γ$ is consistent. For if $Γ$ were inconsistent it would prove some $β$ and $\neg β$ ; soundness gives $Γ ⊨ β$ and $Γ ⊨ \neg β$ , so a model $(A, s)$ of $Γ$ satisfies both $β$ and $\neg β$ , impossible.

Bridge. Soundness is the foundational reason the syntactic turnstile $⊢$ can never overshoot the semantic $⊨$ , and this is exactly the validity of axiom (A2) read off the substitution lemma of 42.01.04 pending: the lemma converts the semantic instantiation at $\overset{s}{ˉ} (t)$ into the syntactic substitution $φ_{t}^{x}$ , so the one axiom that touches terms is correct precisely on the substitutability side condition isolated in the syntax unit. The argument builds toward the deduction theorem and the generalization theorem below, whose proofs reuse the same induction-on-deductions skeleton, and it appears again in the completeness theorem 42.01.06 pending, where the converse inclusion $Γ ⊨ φ \Rightarrow Γ ⊢ φ$ is proved by building a model out of a consistent set — making consistency and satisfiability coincide, the equivalence whose easy half is the corollary just proved. The central insight is that an inductive syntax (deductions built by one rule from fixed axioms) admits proof-by-induction of any property preserved by the rule and held by the axioms; this is exactly the schema soundness instantiates, and it generalises from "being valid" to consistency, conservativity, and the subformula property of the sequent calculus. Putting these together, the calculus is now pinned to the semantics from one side, and the entire weight of the chapter shifts to the single open inclusion that the next unit closes.

Exercises Intermediate+

Exercise 4 (medium, symbolic).

Prove the generalization theorem in the base case: if $⊢ φ$ (a theorem, no premises) then $⊢ \forall x φ$ for every variable $x$ .

Hint

With $Γ = \emptyset$ the side condition " $x$ not free in any premise" is vacuous. Induct on a deduction of $φ$ , using (A4) for axioms and (A3) for modus-ponens steps.

Answer

Let $⟨ α_{0}, \dots, α_{m} = φ ⟩$ be a deduction with no premises. Show $⊢ \forall x α_{i}$ by induction. If $α_{i}$ is a logical axiom, then $\forall x α_{i}$ is also a logical axiom (axioms are closed under prefixing $\forall$ , by the generalization clause of the axiom definition), so $⊢ \forall x α_{i}$ . If $α_{i}$ comes by modus ponens from $α_{j}$ and $α_{k} = (α_{j} \to α_{i})$ , then by induction $⊢ \forall x α_{j}$ and $⊢ \forall x (α_{j} \to α_{i})$ ; the (A3) instance $\forall x (α_{j} \to α_{i}) \to (\forall x α_{j} \to \forall x α_{i})$ with two modus ponens steps yields $⊢ \forall x α_{i}$ . At $i = m$ this gives $⊢ \forall x φ$ . Rubric: full credit for the closure-of-axioms observation and the (A3)-driven inductive step.

Exercise 5 (medium, symbolic).

Show the deduction theorem fails without the eigenvariable restriction by exhibiting a $Γ, γ, φ$ for which $Γ \cup {γ} ⊢ φ$ under an unrestricted generalization rule but $Γ \neq ⊢ (γ \to φ)$ semantically.

Hint

Take $γ = P x$ (with $x$ free) and generalize $x$ . Then ask whether $P x \to \forall x P x$ is valid.

Answer

Let $Γ = \emptyset$ , $γ = P x$ , $φ = \forall x P x$ . With an unrestricted generalization rule, from the premise $P x$ one would generalize $x$ to get ${P x} ⊢ \forall x P x$ . But $P x \to \forall x P x$ is not valid: in a two-element structure with $P$ true of one element and false of the other, an assignment sending $x$ to the $P$ -element satisfies $P x$ yet not $\forall x P x$ , so by soundness $\neq ⊢ (P x \to \forall x P x)$ . The restriction " $x$ not free in the discharged premise" is exactly what blocks generalizing on a variable held fixed by the hypothesis. Rubric: full credit for the explicit counter-structure and the link to the eigenvariable condition.

Exercise 7 (hard, symbolic).

Prove the deduction theorem: $Γ \cup {γ} ⊢ φ$ iff $Γ ⊢ (γ \to φ)$ , taking care that the forward direction respects the generalization-free use of premises (modus ponens is the only rule, so no eigenvariable issue arises).

Hint

Induct on a deduction $⟨ β_{0}, \dots, β_{m} = φ ⟩$ from $Γ \cup {γ}$ , showing $Γ ⊢ (γ \to β_{i})$ at each step, using the tautologies $β \to (γ \to β)$ and the (A1) instance feeding the modus-ponens case.

Answer

( $\Leftarrow$ ) If $Γ ⊢ (γ \to φ)$ then appending $γ$ as a premise and one modus ponens gives $Γ \cup {γ} ⊢ φ$ . ( $\Rightarrow$ ) Let $⟨ β_{0}, \dots, β_{m} = φ ⟩$ be a deduction from $Γ \cup {γ}$ ; show $Γ ⊢ (γ \to β_{i})$ by induction. If $β_{i}$ is a logical axiom or lies in $Γ$ , then from $β_{i}$ and the tautology instance $β_{i} \to (γ \to β_{i})$ (an (A1) axiom) modus ponens gives $γ \to β_{i}$ . If $β_{i} = γ$ , then $γ \to γ$ is a tautology (A1), so $Γ ⊢ (γ \to β_{i})$ . If $β_{i}$ comes by modus ponens from $β_{j}$ and $β_{k} = (β_{j} \to β_{i})$ , then by induction $Γ ⊢ (γ \to β_{j})$ and $Γ ⊢ (γ \to (β_{j} \to β_{i}))$ ; the tautology $(γ \to (β_{j} \to β_{i})) \to ((γ \to β_{j}) \to (γ \to β_{i}))$ (A1) with two modus ponens steps yields $Γ ⊢ (γ \to β_{i})$ . At $i = m$ this is $Γ ⊢ (γ \to φ)$ . Because the only rule is modus ponens, no generalization occurs inside the deduction and no eigenvariable side condition can be violated. Rubric: full credit for both directions, the three cases of the induction, and the remark that single-rule deductions sidestep the generalization restriction.

Exercise 8 (hard, symbolic).

Prove the generalization-on-constants theorem in usable form: if $Γ ⊢ φ$ and the constant $c$ does not occur in $Γ$ , then for some variable $y$ not in $φ$ , $Γ ⊢ \forall y φ_{y}^{c}$ , and moreover $Γ ⊢ φ_{y}^{c}$ already. Sketch the substitution-into-the-deduction argument.

Hint

Replace $c$ by a fresh variable $y$ throughout a deduction of $φ$ . Check each line stays a valid deduction line, then apply the generalization theorem since $y$ is not free in $Γ$ .

Answer

Let $⟨ α_{0}, \dots, α_{m} = φ ⟩$ be a deduction from $Γ$ , and pick a variable $y$ occurring in none of the $α_{i}$ . Replace every occurrence of $c$ by $y$ throughout, obtaining $⟨(α_{0})_{y}^{c}, \dots, (α_{m})_{y}^{c} = φ_{y}^{c} ⟩$ . Each line remains legitimate: a member of $Γ$ is unchanged (since $c \in / Γ$ ); a logical axiom maps to a logical axiom (the axiom groups are closed under replacing a constant by a variable not already present, because substitutability and the tautology/equality shapes are preserved); and a modus-ponens step $α_{i}$ from $α_{j}, α_{j} \to α_{i}$ maps to $(α_{i})_{y}^{c}$ from $(α_{j})_{y}^{c}, (α_{j})_{y}^{c} \to (α_{i})_{y}^{c}$ . Hence $Γ ⊢ φ_{y}^{c}$ . Since $c \in / Γ$ , the fresh $y$ is not free in any member of $Γ$ , so the generalization theorem gives $Γ ⊢ \forall y φ_{y}^{c}$ . Rubric: full credit for the line-by-line stability of the substituted deduction, the fresh-variable choice, and the appeal to the generalization theorem via $y \in / FV (Γ)$ .

Advanced results Master

The calculus fixed in the Formal definition supports four developments: the derived metarules (deduction theorem, generalization, generalization on constants, the rule of substitution) that make $⊢$ workable; the soundness theorem refined to the equality axioms and normal models; the syntactic theory of consistency and its soundness-given link to satisfiability; and the alternative calculi — natural deduction and the sequent calculus with cut — that compute the same $⊢$ by other means.

Theorem 1 (the derived rules: deduction, generalization, substitution). The deduction theorem $Γ \cup {γ} ⊢ φ \Leftrightarrow Γ ⊢ (γ \to φ)$ holds with no side condition, because modus ponens is the sole rule ^{[Enderton §2.4]}. The generalization theorem states that if $Γ ⊢ φ$ and $x$ is free in no member of $Γ$ , then $Γ ⊢ \forall x φ$ ; the restriction is the eigenvariable condition, and dropping it falsifies ${P x} ⊢ \forall x P x$ . The generalization-on-constants theorem says that if $Γ ⊢ φ$ and $c$ occurs in no member of $Γ$ , then $Γ ⊢ \forall y φ_{y}^{c}$ for a fresh $y$ , the syntactic embodiment of " $c$ was arbitrary." The rule of substitution follows: from $⊢ φ$ one obtains $⊢ φ_{t}^{x}$ for substitutable $t$ , and from $⊢ \forall x φ$ one obtains every instance $⊢ φ_{t}^{x}$ by (A2) and modus ponens. These four turn the spartan axiomatic system into the calculus actually used in proofs.

Theorem 2 (soundness with equality and normal models). Soundness $Γ ⊢ φ \Rightarrow Γ ⊨ φ$ holds over the class of all structures interpreting $=$ as genuine identity ^{[Enderton §2.4]}. The equality axioms (A5) $u = u$ and (A6) $u = v \to (φ \to φ^{'})$ are valid in exactly the normal models, where $=^{A}$ is identity; they fail if $=$ is read as a proper congruence, which is why a model produced syntactically must be quotiented by the provable-equality relation to become normal. The validity argument is the axiom-by-axiom check of the Key theorem, with (A6) reflecting that a relation cannot distinguish equal tuples. Soundness for sentences specializes to $⊢ σ \Rightarrow⊨ σ$ : every closed theorem is true in every normal model.

Theorem 3 (syntactic consistency and the easy half of the equivalence). A set $Γ$ is consistent iff it does not prove every formula, iff for no $β$ does $Γ ⊢ β$ and $Γ ⊢ \neg β$ ^{[Shoenfield Ch. 3]}. Consistency is finitary: $Γ$ is inconsistent iff some finite $Γ_{0} \subseteq Γ$ is, since any deduction of a contradiction uses finitely many premises — the syntactic root of compactness 42.01.02 pending. Soundness yields the easy direction of the consistency–satisfiability equivalence: every satisfiable $Γ$ is consistent, equivalently every inconsistent $Γ$ is unsatisfiable. The hard direction — every consistent $Γ$ is satisfiable, by a Henkin model construction — is the completeness theorem 42.01.06 pending, and the two together make $⊢$ and $⊨$ extensionally identical and consistency a synonym for "has a model."

Theorem 4 (alternative calculi: natural deduction, sequent calculus, cut). The Hilbert turnstile is reproduced by natural deduction, whose introduction/elimination rules for $\forall, \exists$ carry eigenvariable (proper-variable) conditions; $\forall$ -introduction discharges a fresh-variable derivation exactly as the generalization theorem does ^{[van Dalen Ch. 2]}. Gentzen's sequent calculus LK manipulates sequents $Γ \Rightarrow Δ$ with left/right rules per connective and quantifier, the structural rules, and the cut rule — from $Γ \Rightarrow Δ, φ$ and $φ, Π \Rightarrow Λ$ infer $Γ, Π \Rightarrow Δ, Λ$ — which is modus ponens internalized ^{[Takeuti Ch. 1]}. The cut-elimination theorem (Gentzen's Hauptsatz) shows every LK derivation transforms into a cut-free one, whence the subformula property and a syntactic consistency proof of pure logic. All three calculi prove the same theorems; the full development of cut-elimination and its consequences belongs to proof theory 42.05.01 pending.

Synthesis. Soundness is the foundational reason $⊢$ is pinned below $⊨$ , and putting these together it organizes all four developments: it is exactly what turns a proved contradiction into an unsatisfiable theory, so the consistency–satisfiability link of Theorem 3 is its corollary, and the eigenvariable condition of Theorems 1 and 4 is the precise syntactic shadow of the semantic fact that a free variable held fixed by a premise cannot be universally generalized — this is the central insight that the generalization restriction and the (A4) vacuous-quantification axiom both encode. The deduction theorem generalises the propositional deduction theorem of 42.01.01 pending to the first-order setting unchanged, because the lone rule is still modus ponens, while the generalization and constants theorems are the genuinely first-order additions, dual to one another across " $x$ free" versus " $c$ fresh." The equality axioms and the quotient-to-normal-model maneuver are the bridge from the bare term model to a structure where $=$ is identity, the maneuver completeness 42.01.06 pending performs in full. And the alternative calculi — natural deduction's eigenvariable rules and LK's cut, whose elimination is the namesake theorem of proof theory 42.05.01 pending — show the same syntactic-consequence relation computed three ways, so that soundness, proved once for the Hilbert system, transfers by mutual simulation. This is the syntactic half of the architecture: a meaning-free engine for $⊢$ , sound for the Tarski semantics of 42.01.04 pending, standing ready to be proved complete in 42.01.06 pending.

Full proof set Master

Proposition 1 (soundness, full statement). If $Γ ⊢ φ$ then $Γ ⊨ φ$ .

Proof. Fix $(A, s)$ with $A ⊨ γ [s]$ for all $γ \in Γ$ and a deduction $⟨ α_{0}, \dots, α_{m} = φ ⟩$ . Induct on $i$ to show $A ⊨ α_{i} [s]$ . Premise lines hold by hypothesis. Axiom lines hold by the validity lemma below. A modus-ponens line $α_{i}$ from $α_{j}, α_{k} = (α_{j} \to α_{i})$ inherits $A ⊨ α_{j} [s]$ and $A ⊨ (α_{j} \to α_{i}) [s]$ from the inductive hypothesis; the $\to$ -clause forces $A ⊨ α_{i} [s]$ . At $i = m$ , $A ⊨ φ [s]$ ; as $(A, s)$ was an arbitrary model of $Γ$ , $Γ ⊨ φ$ .

Validity lemma. Every generalization $\forall \overset{x}{ˉ} θ$ of a base axiom is valid iff $θ$ is, so check the bases. (A1): a propositional tautology stays true under the truth values $(A, s)$ assigns its prime subformulas. (A2): $A ⊨ \forall x φ [s]$ gives $A ⊨ φ [s (x ∣ \overset{s}{ˉ} (t))]$ , and the substitution lemma of 42.01.04 pending rewrites this as $A ⊨ φ_{t}^{x} [s]$ . (A3): universal hypotheses on $φ \to ψ$ and $φ$ at every $a$ give $ψ$ at every $a$ . (A4): with $x \in / FV (φ)$ , coincidence makes $A ⊨ φ [s]$ entail $A ⊨ φ [s (x ∣ a)]$ for all $a$ . (A5): identity is reflexive. (A6): $\overset{s}{ˉ} (u) = \overset{s}{ˉ} (v)$ equalizes the tuples in an atomic $φ$ versus $φ^{'}$ . $□$

Proposition 2 (deduction theorem). $Γ \cup {γ} ⊢ φ$ iff $Γ ⊢ (γ \to φ)$ .

Proof. ( $\Leftarrow$ ) Adjoin $γ$ and apply modus ponens. ( $\Rightarrow$ ) Induct on a deduction $⟨ β_{0}, \dots, β_{m} = φ ⟩$ from $Γ \cup {γ}$ , proving $Γ ⊢ (γ \to β_{i})$ . If $β_{i}$ is an axiom or in $Γ$ : from $β_{i}$ and the (A1) tautology $β_{i} \to (γ \to β_{i})$ , modus ponens gives $γ \to β_{i}$ . If $β_{i} = γ$ : $γ \to γ$ is an (A1) tautology. If $β_{i}$ is modus ponens of $β_{j}, β_{k} = (β_{j} \to β_{i})$ : from the inductive $Γ ⊢ (γ \to β_{j})$ and $Γ ⊢ (γ \to (β_{j} \to β_{i}))$ and the (A1) tautology $(γ \to (β_{j} \to β_{i})) \to ((γ \to β_{j}) \to (γ \to β_{i}))$ , two modus ponens steps give $γ \to β_{i}$ . The lone rule being modus ponens, no generalization-restriction can be violated. At $i = m$ , $Γ ⊢ (γ \to φ)$ . $□$

Proposition 3 (generalization theorem). If $Γ ⊢ φ$ and $x$ is free in no member of $Γ$ , then $Γ ⊢ \forall x φ$ .

Proof. Induct on a deduction $⟨ α_{0}, \dots, α_{m} = φ ⟩$ from $Γ$ , proving $Γ ⊢ \forall x α_{i}$ . If $α_{i}$ is a logical axiom, then $\forall x α_{i}$ is a logical axiom (closure under prefixing $\forall$ ), so $Γ ⊢ \forall x α_{i}$ . If $α_{i} \in Γ$ , then $x \in / FV (α_{i})$ by hypothesis, so the (A4) axiom $α_{i} \to \forall x α_{i}$ with modus ponens on the premise $α_{i}$ gives $Γ ⊢ \forall x α_{i}$ . If $α_{i}$ is modus ponens of $α_{j}, α_{k} = (α_{j} \to α_{i})$ , then by induction $Γ ⊢ \forall x α_{j}$ and $Γ ⊢ \forall x (α_{j} \to α_{i})$ ; the (A3) axiom $\forall x (α_{j} \to α_{i}) \to (\forall x α_{j} \to \forall x α_{i})$ with two modus ponens steps gives $Γ ⊢ \forall x α_{i}$ . At $i = m$ , $Γ ⊢ \forall x φ$ . The hypothesis $x \in / FV (Γ)$ is used exactly at the premise case, where (A4) demands $x$ not free in $α_{i}$ . $□$

Proposition 4 (generalization on constants). If $Γ ⊢ φ$ and the constant $c$ occurs in no member of $Γ$ , then $Γ ⊢ φ_{y}^{c}$ and $Γ ⊢ \forall y φ_{y}^{c}$ for a variable $y$ occurring nowhere in the chosen deduction.

Proof. Take a deduction $⟨ α_{0}, \dots, α_{m} = φ ⟩$ from $Γ$ and a variable $y$ in none of its lines. Replace every $c$ by $y$ throughout. A premise line $α_{i} \in Γ$ is unchanged ( $c \in / Γ$ ). A logical axiom maps to a logical axiom: the tautology shape (A1) is preserved under a uniform constant-for-variable replacement, (A2)'s substitutability is preserved because $y$ is new and so substitutable wherever $t$ was, and (A3)–(A6) are shape-closed under the replacement. A modus-ponens step maps to a modus-ponens step since the replacement commutes with the connective $\to$ . Hence $⟨(α_{i})_{y}^{c} ⟩_{i}$ is a deduction of $φ_{y}^{c}$ from $Γ$ , giving $Γ ⊢ φ_{y}^{c}$ . As $c \in / Γ$ the fresh $y$ is free in no member of $Γ$ , so Proposition 3 gives $Γ ⊢ \forall y φ_{y}^{c}$ . $□$

Proposition 5 (consistency from satisfiability, and finitary inconsistency). Every satisfiable $Γ$ is consistent; and $Γ$ is inconsistent iff some finite $Γ_{0} \subseteq Γ$ is inconsistent.

Proof. If $Γ$ has a model $(A, s)$ but is inconsistent, then $Γ ⊢ β$ and $Γ ⊢ \neg β$ for some $β$ ; Proposition 1 gives $Γ ⊨ β$ and $Γ ⊨ \neg β$ , so $A ⊨ β [s]$ and $A \neq ⊨ β [s]$ , a contradiction. Hence satisfiable sets are consistent. For finitariness: if $Γ$ is inconsistent, fix deductions of some $β$ and $\neg β$ from $Γ$ ; each is finite and cites finitely many premises, and the union $Γ_{0}$ of those cited premises is a finite subset with $Γ_{0} ⊢ β$ and $Γ_{0} ⊢ \neg β$ , so $Γ_{0}$ is inconsistent. Conversely an inconsistent finite $Γ_{0} \subseteq Γ$ makes $Γ$ inconsistent since deductions from $Γ_{0}$ are deductions from $Γ$ . $□$

Connections Master

Structures and Tarski's definition of truth 42.01.04 pending supplies the semantics this calculus is matched against. The validity of the instantiation axiom (A2) is exactly the substitution lemma of 42.01.04 pending — converting semantic instantiation at $\overset{s}{ˉ} (t)$ into syntactic substitution $φ_{t}^{x}$ — and the validity of the vacuous-quantification axiom (A4) is the coincidence lemma there. That unit owns the meaning of formulas; this unit owns the meaning-free engine that derives them, the two meeting in the soundness proof, where each axiom's validity is read off a semantic lemma of 42.01.04 pending.
The completeness theorem for first-order logic, co-produced as 42.01.06 pending, proves the converse inclusion this unit leaves open: Gödel's theorem gives $Γ ⊨ φ \Rightarrow Γ ⊢ φ$ , so that with the soundness of this unit the turnstile $⊢$ and the semantic consequence $⊨$ of 42.01.04 pending coincide. Henkin's construction extends a consistent $Γ$ to a maximal consistent set with witnesses and reads a normal model off the term algebra quotiented by provable equality — the quotient the equality axioms (A5)–(A6) of this unit make a congruence — so consistency (defined here) becomes synonymous with satisfiability.
Compactness for first-order logic 42.01.02 pending rests on the finitariness of consistency proved here: a deduction of a contradiction uses finitely many premises, so an inconsistent theory has an inconsistent finite subtheory, and through completeness 42.01.06 pending this becomes "a theory with no model has a finite subtheory with no model." The syntactic finiteness of this unit's deductions is the proof-theoretic engine behind that semantic theorem.
Proof theory and cut-elimination 42.05.01 pending takes the alternative calculi previewed in Theorem 4 as its subject: Gentzen's sequent calculus LK, where the cut rule internalizes the modus ponens of this unit, and the Hauptsatz that eliminates cut to yield the subformula property and a syntactic consistency proof. Natural deduction's eigenvariable conditions are the proof-theoretic form of this unit's generalization restriction, and the mutual simulation of the three calculi transfers the soundness proved here.

Historical & philosophical context Master

The axiomatic style of this calculus descends from Gottlob Frege's Begriffsschrift (1879), the first formal system with explicit axioms, a conditional and negation, the universal quantifier, and a single detachment rule, and from the predicate-logic axiomatizations of David Hilbert and Wilhelm Ackermann's Grundzüge der theoretischen Logik (1928), which posed the completeness of the calculus as an open problem ^{[Enderton §2.4]}. Kurt Gödel's 1930 dissertation Die Vollständigkeit der Axiome des logischen Funktionenkalküls answered it, proving that the Hilbert-style first-order calculus derives exactly the valid formulas; the soundness half — that derivations cannot overshoot validity — is the routine direction his theorem packages with the substantive converse.

Gerhard Gentzen's Untersuchungen über das logische Schließen (1934-35) introduced both natural deduction, with its introduction and elimination rules and eigenvariable conditions, and the sequent calculus LK, proving the cut-elimination Hauptsatz that gives a constructive consistency argument for pure logic ^{[Takeuti Ch. 1]}. The economical Hilbert systems and the deduction-theorem technique were standardized by Stephen Kleene's Introduction to Metamathematics (1952), by Joseph Shoenfield's Mathematical Logic (1967) ^{[Shoenfield Ch. 2]}, and by Elliott Mendelson's textbook ^{[Mendelson Ch. 2]}, while the natural-deduction presentation became standard through Dirk van Dalen's Logic and Structure ^{[van Dalen Ch. 2]}; the equality axioms and the normal-model reading trace to the same period's treatment of identity as a logical, rather than nonlogical, relation.

Bibliography Master

@book{enderton2001logic,
  author    = {Enderton, Herbert B.},
  title     = {A Mathematical Introduction to Logic},
  edition   = {2},
  publisher = {Harcourt/Academic Press},
  year      = {2001}
}

@book{mendelson2015logic,
  author    = {Mendelson, Elliott},
  title     = {Introduction to Mathematical Logic},
  edition   = {6},
  publisher = {CRC Press},
  year      = {2015}
}

@book{shoenfield1967logic,
  author    = {Shoenfield, Joseph R.},
  title     = {Mathematical Logic},
  publisher = {Addison-Wesley},
  year      = {1967}
}

@book{vandalen2013logic,
  author    = {van Dalen, Dirk},
  title     = {Logic and Structure},
  edition   = {5},
  publisher = {Springer},
  year      = {2013}
}

@book{takeuti1987prooftheory,
  author    = {Takeuti, Gaisi},
  title     = {Proof Theory},
  edition   = {2},
  publisher = {North-Holland},
  year      = {1987}
}

@phdthesis{godel1930completeness,
  author = {G\"{o}del, Kurt},
  title  = {Die Vollst\"{a}ndigkeit der Axiome des logischen Funktionenkalk\"{u}ls},
  school = {University of Vienna},
  year   = {1930},
  note   = {Published in Monatshefte f\"{u}r Mathematik und Physik 37 (1930), 349--360}
}

@article{gentzen1935untersuchungen,
  author  = {Gentzen, Gerhard},
  title   = {Untersuchungen \"{u}ber das logische Schlie{\ss}en},
  journal = {Mathematische Zeitschrift},
  volume  = {39},
  year    = {1935},
  pages   = {176--210, 405--431}
}

@book{frege1879begriffsschrift,
  author    = {Frege, Gottlob},
  title     = {Begriffsschrift, eine der arithmetischen nachgebildete Formelsprache des reinen Denkens},
  publisher = {Louis Nebert, Halle},
  year      = {1879}
}

@book{hilbertackermann1928,
  author    = {Hilbert, David and Ackermann, Wilhelm},
  title     = {Grundz\"{u}ge der theoretischen Logik},
  publisher = {Springer},
  year      = {1928}
}

@book{kleene1952metamathematics,
  author    = {Kleene, Stephen Cole},
  title     = {Introduction to Metamathematics},
  publisher = {North-Holland},
  year      = {1952}
}

Prerequisites

42.01.04

Tier anchors

beginner: Enderton 2001 *A Mathematical Introduction to Logic* 2e (Harcourt/Academic Press) §2.4 (a proof read informally as a chain of statements, each a starting assumption or an allowed logical axiom or a one-line consequence of two earlier lines by the detachment rule; the difference between a statement being provable — reachable by such a chain — and a statement being true in every world; checking a short chain of reasoning by hand and seeing that it never appeals to any particular meaning of the symbols)
intermediate: Enderton 2001 *A Mathematical Introduction to Logic* 2e §2.4 (a Hilbert-style proof system for first-order logic: the logical axiom groups — tautologies, the quantifier-instantiation axiom, the quantifier-distribution axiom, the vacuous-quantifier axiom, and the equality axioms — together with the single rule modus ponens; the syntactic-consequence relation Γ ⊢ φ and formal deductions as finite sequences; the deduction theorem; generalization and generalization on constants; the soundness theorem Γ ⊢ φ ⟹ Γ ⊨ φ proved by induction on deductions; consistency and its relation to satisfiability)
master: Enderton 2001 *A Mathematical Introduction to Logic* 2e §2.4-2.5 (the full Hilbert calculus with the equality axioms and normal models, the generalization theorem, the deduction theorem, the soundness theorem, and the syntactic notions of consistency and inconsistency that the completeness theorem will tie to satisfiability); Mendelson 2015 *Introduction to Mathematical Logic* 6e (CRC) Ch. 2 (the predicate calculus, its axioms and the generalization rule, the deduction theorem with its eigenvariable restriction); Shoenfield 1967 *Mathematical Logic* (Addison-Wesley) Ch. 2-3 (an economical Hilbert system, the equality and substitution axioms); van Dalen 2013 *Logic and Structure* 5e (Springer) Ch. 2-3 (natural deduction for first-order logic as an alternative calculus); Takeuti 1987 *Proof Theory* 2e (North-Holland) Ch. 1 (the sequent calculus LK, the cut rule, and the cut-elimination theorem)

References

Enderton, H. B. — A Mathematical Introduction to Logic · 2nd edition, Harcourt/Academic Press (2001), §2.4-2.5. Fixes a Hilbert-style deductive calculus for first-order logic. The logical axioms are all generalizations of formulas of the following groups (here φ, ψ are formulas, x a variable, t a term substitutable for x in φ, c a constant): (1) tautologies — every formula that is a tautology in the propositional sense, reading atomic and quantified subformulas as prime; (2) the instantiation axiom ∀x φ → φ^x_t for t substitutable for x in φ; (3) the distribution axiom ∀x(φ → ψ) → (∀x φ → ∀x ψ); (4) the vacuous-quantification axiom φ → ∀x φ when x does not occur free in φ; and the equality axiom group (5) x = x and (6) x = y → (φ → φ') where φ' is φ with some occurrences of x replaced by y, each substitution legal. A generalization of θ is any formula ∀x_1 ... ∀x_n θ (n ≥ 0). The single rule of inference is modus ponens: from φ and φ → ψ infer ψ. A deduction of φ from a set Γ is a finite sequence ⟨α_0, ..., α_m⟩ with α_m = φ in which each α_i is a logical axiom, a member of Γ, or follows from two earlier α_j, α_k by modus ponens; one writes Γ ⊢ φ. The generalization rule is a derived rule: if Γ ⊢ φ and x does not occur free in any member of Γ, then Γ ⊢ ∀x φ (Generalization Theorem). The Deduction Theorem holds: Γ ∪ {γ} ⊢ φ iff Γ ⊢ (γ → φ). The Generalization-on-Constants theorem: if Γ ⊢ φ and c is a constant not occurring in Γ, then there is a variable y not occurring in φ such that Γ ⊢ ∀y φ^c_y, and the deduction may be taken not to use c. The Soundness Theorem: if Γ ⊢ φ then Γ ⊨ φ; proved by showing every logical axiom is valid (true in every structure under every assignment) and that modus ponens preserves the property of being satisfied by a given structure-assignment pair, then inducting on the length of the deduction. A set Γ is consistent (syntactically) if for no formula β do both Γ ⊢ β and Γ ⊢ ¬β; equivalently Γ does not prove every formula. Soundness gives the easy half of the consistency/satisfiability link: every satisfiable Γ is consistent. The converse — every consistent Γ is satisfiable — is the completeness theorem. The equality axioms force the interpretation of = to behave as a congruence; a structure where = is read as genuine identity is a normal model, and the completeness theorem produces a normal model by quotienting the Henkin term model by the provable-equality congruence.
Mendelson, E. — Introduction to Mathematical Logic · 6th edition, CRC Press / Chapman & Hall (2015), Chapter 2 ('First-Order Logic and Model Theory'). Presents the predicate calculus as a Hilbert system: the propositional axiom schemata A1-A3, the quantifier axioms (∀x φ(x) → φ(t) for t free for x in φ, and ∀x(φ → ψ) → (φ → ∀x ψ) when x is not free in φ), the equality axioms, the inference rules modus ponens and generalization (from φ infer ∀x φ). Proves the Deduction Theorem with the eigenvariable restriction: Γ ∪ {φ} ⊢ ψ implies Γ ⊢ φ → ψ provided no application of generalization in the deduction is to a variable free in φ. Establishes the soundness of the calculus relative to the Tarskian semantics and develops consistency, the equivalence of consistency with the existence of a model (Gödel's completeness theorem, via the Henkin/Lindenbaum method), and the compactness and Löwenheim-Skolem theorems as corollaries.
Shoenfield, J. R. — Mathematical Logic · Addison-Wesley (1967), Chapters 2-3. Develops an economical first-order Hilbert calculus with propositional, substitution, identity, and equality axioms together with the rules of expansion, contraction, associativity, cut, and ∃-introduction. Proves the basic syntactic metatheorems — the tautology theorem, the deduction theorem, the theorem on constants, and the generalization and substitution rules — and the reduction theorem relating consistency to deducibility. Soundness is the validity of the axioms and the truth-preservation of the rules; consistency is defined syntactically and shown, with the completeness theorem of Chapter 4, to coincide with the existence of a model.
van Dalen, D. — Logic and Structure · 5th edition, Springer (2013), Chapters 2-3. Presents natural deduction for first-order logic as the primary calculus: the introduction and elimination rules for ∧, ∨, →, ⊥, ¬, ∀, ∃, with the eigenvariable (proper-variable) conditions on ∀-introduction and ∃-elimination guaranteeing the rules are sound. Derivations are trees with discharged hypotheses; Γ ⊢ φ means a derivation with open hypotheses among Γ and conclusion φ. Proves soundness (every derivable sequent is valid) by induction on the derivation tree, and completeness by a Henkin-style model existence theorem. The equivalence of the natural-deduction turnstile with the Hilbert turnstile is established by mutual simulation.
Takeuti, G. — Proof Theory · 2nd edition, North-Holland / Dover reprint (1987/2013), Chapter 1. Develops Gentzen's sequent calculus LK for first-order logic: sequents Γ ⟹ Δ, the logical inference rules introducing each connective and quantifier on the left and right, the structural rules (weakening, contraction, exchange), and the cut rule (from Γ ⟹ Δ, φ and φ, Π ⟹ Λ infer Γ, Π ⟹ Δ, Λ). Proves the cut-elimination theorem (Gentzen's Hauptsatz): every LK derivation can be transformed into a cut-free derivation of the same sequent, whence the subformula property and consistency of pure logic follow. The eigenvariable conditions on the quantifier rules are the sequent-calculus analogue of the Hilbert generalization restriction.

Estimated time

beginner: 18m
intermediate: 50m
master: 85m