A Deductive Calculus for First-Order Logic

The semantic account of first-order logic answers what follows from a set of hypotheses: $Γ ⊨ φ$ holds when every structure satisfying all of $Γ$ also satisfies $φ$ . That definition quantifies over all structures and all variable assignments, an uncountable search with no obvious stopping point.¹ A proof settles the same question by finite, inspectable means. The syntactic counterpart is a deductive calculus whose proofs are finite strings, checkable without insight.

Two constraints fix the design.² A proof must be finite, because it is an object handed from one person to another, and an infinite set of hypotheses cannot be handed over whole. A proof must also be effectively checkable: verifying that a purported proof contains no fallacy must be a mechanical procedure, not a matter of flashes of insight. In particular, the set of proofs from no hypotheses should be decidable, so that the provable-from-nothing formulas can be effectively listed by generating all strings and sorting proofs from non-proofs.

To keep the two levels apart we reserve the word deduction for the formal object and leave proof for the ordinary mathematical arguments (in English) that we make about deductions. A deduction lives in the object language; our reasoning about deductions lives in the meta-language.

The two levels kept apart throughout: ordinary mathematical reasoning in the meta-language studies the formal calculus below it.

Deductions from a rule of inference

Fix a first-order language. We will select an infinite set $Λ$ of formulas, the logical axioms, and one rule of inference. For a set $Γ$ of formulas, a formula counts as a theorem of $Γ$ if and only if it is obtainable from $Γ \cup Λ$ by applying the rule finitely many times.

The single rule is modus ponens: from $α$ and $α \to β$ , infer $β$ .

\frac{α , α \to β}{β}

The choice of $Λ$ and of the rules is far from unique; every deductive calculus trades axioms against rules. Taking $Λ = \emptyset$ forces many rules of inference; the opposite extreme, taken here, keeps a single rule and pays for it with an infinite axiom set.

Checking a purported deduction is the mechanical procedure the design demanded: scan the sequence once, verifying each line locally.

Algorithm:

\textsc{CheckDeduction}(\alpha_0, \dots, \alpha_n;\ \Gamma)

— verify a purported deduction

1
for each $k \gets 0, 1, \dots, n$ do
2
if $\alpha_k \in \Gamma \cup \Lambda$ then accept line $k$
3
else if some $i, j < k$ have $\alpha_j = (\alpha_i \to \alpha_k)$ then accept line $k$
4
else reject the sequence
5
accept the sequence as a deduction of $\alpha_n$

Line-by-line acceptance needs membership in $Γ \cup Λ$ to be checkable; for $Λ$ that is arranged below by giving the axioms a purely syntactic definition, and for hypotheses it holds whenever $Γ$ is decidable.

The word theorem now lives on two levels. Inside the object language, $α$ is a theorem of $Γ$ when $Γ ⊢ α$ . In the meta-language, statements about deductions (each proved in English) are also called theorems; when the distinction matters we call the latter metatheorems.

A deduction is a construction sequence: it records how $φ$ is obtained from the base set $Γ \cup Λ$ by applying modus ponens zero or more times. This resembles building a wff from atoms, with two differences. Modus ponens is partial (its domain is only pairs of the form $α, α \to β$ ), and it can produce a shorter formula from longer ones. The deeper difference is that the set of theorems is not freely generated: a theorem has many deductions, and its construction tree is not unique.³ An induction principle still holds.

Every metatheorem below that quantifies over all theorems of $Γ$ is proved by exhibiting a set $S$ of the right shape and invoking this principle.

Substitution

The logical axioms depend on substituting a term for a variable, so we pin that operation down first. For a formula $α$ , a variable $x$ , and a term $t$ , the expression $α_{t}^{x}$ is the result of replacing $x$ by $t$ at every free occurrence of $x$ in $α$ . Officially this is a recursion on $α$ (with an auxiliary recursion on terms for the atomic case).⁴

For example $φ_{x}^{x} = φ$ , and $(Q x \to \forall x P x)_{y}^{x} = (Q y \to \forall x P x)$ : the $x$ inside $\forall x P x$ is bound and untouched.

Substitution alone is not always safe. Take $α = \neg\forall y x = y$ and substitute $y$ for $x$ :

\forall x α \to α_{y}^{x} is \forall x \neg\forall y x = y \to \neg\forall y y = y .

The antecedent $\forall x \neg\forall y x = y$ is true in any structure whose universe has two or more elements. The consequent $\neg\forall y y = y$ is false in every structure, since $y = y$ holds always. So this instance of the plausible-looking schema if $α$ holds of everything, it holds of $t$ is nearly always false. The fault is capture: the substituted $y$ was seized by the $\forall y$ quantifier already present.

Variable capture. Substituting the term for the free variable sends it under a quantifier that binds the same letter, changing its meaning.

To exclude capture we define when a term may be substituted at all.

Two easy cases: $x$ is always substitutable for itself, and any $t$ whose variables all avoid $α$ is substitutable for $x$ in $α$ . The word choice is deliberate: even when $t$ is not substitutable, $α_{t}^{x}$ is still formed by replacing every free $x$ with $t$ . Substitutability is a licensing condition on the axioms, not on the operation. It coincides with the free for condition studied for the substitution lemma.

The logical axioms

Before listing $Λ$ we widen each schema to its generalizations. A wff $φ$ is a generalization of $ψ$ iff $φ = \forall x_{1} \dots \forall x_{n} ψ$ for some $n \geq 0$ and variables $x_{1}, \dots, x_{n}$ ; the case $n = 0$ makes every wff a generalization of itself. The logical axioms are all generalizations of wffs of the following six forms, where $x, y$ are variables and $α, β$ are wffs.

Group	Schema	Reads as
1	tautologies	the sentential content
2	$\forall x α \to α_{t}^{x}$ , with $t$ substitutable for $x$ in $α$	instantiation of a universal
3	$\forall x (α \to β) \to (\forall x α \to \forall x β)$	$\forall$ distributes over $\to$
4	$α \to \forall x α$ , with $x$ not free in $α$	vacuous quantification
5	$x = x$	reflexivity of equality
6	$x = y \to (α \to α^{'})$ , $α$ atomic, $α^{'}$ replaces $x$ by $y$ at some places	equals substitute into atoms

Groups 5 and 6 are included only when the language carries equality. The list is not meant to look natural; each group is justified below. Group 2 encodes the meaning of the quantifier; groups 3 and 4 exist precisely to make the generalization theorem go through; groups 5 and 6 are exactly enough to prove the properties of equality.

The six axiom schemas as one reference card, grouped by the fragment of the logic each governs: sentential, quantifier, and equality.

Deciding whether a formula is a group-2 axiom means matching it against $\forall x α \to α_{t}^{x}$ and checking substitutability. Both halves have to hold.

Worked example. Is $\forall v_{3} (\forall v_{1} (A v_{1} \to \forall v_{2} A v_{2}) \to (A v_{2} \to \forall v_{2} A v_{2}))$ a group-2 axiom? Strip the leading generalization $\forall v_{3}$ and read the body as $\forall x α \to α_{t}^{x}$ with $x = v_{1}$ , $α = (A v_{1} \to \forall v_{2} A v_{2})$ , $t = v_{2}$ . Compute the substitution:

α_{v_{2}}^{v_{1}} = (A v_{2} \to \forall v_{2} A v_{2}),

since $A v_{1}$ becomes $A v_{2}$ and $\forall v_{2} A v_{2}$ is untouched ( $v_{2}$ is bound). Substitutability holds: $v_{2}$ enters $A v_{1}$ freely, and $v_{1}$ is not free in $\forall v_{2} A v_{2}$ . The body is $\forall v_{1} α \to α_{v_{2}}^{v_{1}}$ and the whole is its $\forall v_{3}$ -generalization, so it is in group 2.

The near-miss $\forall v_{1} \forall v_{2} B v_{1} v_{2} \to \forall v_{2} B v_{2} v_{2}$ matches the shape with $α = \forall v_{2} B v_{1} v_{2}$ , $t = v_{2}$ : indeed $α_{v_{2}}^{v_{1}} = \forall v_{2} B v_{2} v_{2}$ . But $v_{2}$ is not substitutable for $v_{1}$ in $\forall v_{2} B v_{1} v_{2}$ , because $v_{1}$ occurs free there and the incoming $v_{2}$ is captured by $\forall v_{2}$ . The side condition fails, so this one is not an axiom.

Tautologies as axioms

Group 1 needs spelling out, because tautology was defined for sentential logic. Split the wffs into prime formulas (atomic formulas and those of the form $\forall x α$ ) and nonprime formulas (the $\neg α$ and $α \to β$ ). Every wff is built from prime formulas by the two operations for $\neg$ and $\to$ . Now treat the prime formulas as sentence symbols. A wff is in axiom group 1 iff, read this way, it is a tautology of sentential logic in the connectives $\neg, \to$ . No replacement is needed; the prime formulas already are first-order wffs.

The prime / nonprime split behind group 1. Prime formulas become the sentence symbols; the two connectives rebuild every wff on top of them.

For example, the contraposition tautology $(A \to \neg B) \to (B \to \neg A)$ , with $A = \forall y \neg P y$ and $B = P x$ , yields the group-1 axiom

(\forall y \neg P y \to \neg P x) \to (P x \to \neg\forall y \neg P y) .

Its truth table has four rows (two prime formulas), and every row comes out true.

Worked example. Treat the prime formulas $A = \forall y \neg P y$ and $B = P x$ as sentence symbols and tabulate $(A \to \neg B) \to (B \to \neg A)$ over the four assignments.

$A$	$B$	$A \to \neg B$	$B \to \neg A$	$(A \to \neg B) \to (B \to \neg A)$
T	T	F	F	T
T	F	T	T	T
F	T	T	T	T
F	F	T	T	T

The final column is constant $T$ , so the wff is a tautology of sentential logic in $\neg, \to$ , hence a group-1 axiom. The row $A = B = T$ is the only one where both branches are false, and a conditional with a false antecedent is true, so the whole comes out $T$ there as well.

By contrast $\forall x (P x \to P x)$ and $\forall x P x \to P x$ are not tautologies: their quantified prime formulas can independently take either truth value, even though both are in fact valid for quantifier-level reasons.

Taking all tautologies as axioms is more than needed. The tautologies form a decidable set (which matters for the enumerability theorem in soundness and completeness), but there is no known fast decision procedure for them. One could instead take a polynomial-time-decidable subset of tautologies as axioms and derive the rest by modus ponens.

Deducibility as tautological implication

First-order formulas are now also sentential wffs (over the prime formulas), so sentential concepts apply to them. If $Σ$ tautologically implies $φ$ then $Σ$ logically implies $φ$ , but not conversely: $\forall x P x$ logically implies $P c$ , yet does not tautologically imply it, because $\forall x P x$ and $P c$ are distinct prime formulas.⁵

The following metatheorem reduces the whole deductive calculus to sentential tautological implication from $Γ \cup Λ$ .

The proof uses sentential compactness for a possibly uncountable language, since we never assumed the first-order language has only countably many symbols.

A worked deduction

Consider deducing, from no hypotheses, that a property holds of $x$ implies it holds of some element:

⊢ P x \to \exists y P y .

The existential is an abbreviation: $\exists y P y$ is $\neg\forall y \neg P y$ . The deduction has three lines.

#	Formula	Justification
1	$\forall y \neg P y \to \neg P x$	axiom group 2: instance of $\forall y α \to α_{x}^{y}$ with $α = \neg P y$
2	$(\forall y \neg P y \to \neg P x) \to (P x \to \neg\forall y \neg P y)$	axiom group 1: contraposition tautology
3	$P x \to \neg\forall y \neg P y$ , i.e. $P x \to \exists y P y$	modus ponens, lines 1 and 2

Line 1 is a group-2 instantiation: substituting the term $x$ for the quantified $y$ in $\neg P y$ gives $\neg P x$ , and $x$ is substitutable for $y$ there. Line 2 is a tautology by the truth table above. One application of modus ponens closes the deduction. The same three formulas, drawn as a pedigree tree, show modus ponens as a single node with the two axioms as inputs.

The same deduction as a pedigree tree; the two axioms feed one modus ponens node whose output is the theorem. Squashing the tree gives the linear deduction above.

Generalizing to $⊢ \forall x (P x \to \exists y P y)$ prepends quantifiers, licensed by the generalization theorem. The derived rules replace these hand-drawn trees with reusable moves.

The choice of a syntactic axiom set

It might seem cleaner to take the set of all valid formulas as $Λ$ . Two objections rule it out.⁶ First, validity is a semantic notion, defined by quantifying over structures and truth. To prove that the validities are effectively enumerable we need $Λ$ to have a finitary, syntactic definition, one that inspects only the arrangement of symbols. Second, we want $Λ$ to be decidable, and the set of validities is not decidable (Church's theorem, reached in the incompleteness chapter). The six schemas meet both demands: membership in $Λ$ is a mechanical syntax check, run group by group.

The design succeeds only if the syntactic relation $⊢$ matches the semantic relation $⊨$ . That two-way match is the content of the soundness and completeness theorems. The metatheorems (deduction theorem, generalization, the derived rules) make the calculus usable by hand.

Enderton, §2.2. Logical implication $Γ ⊨ φ$ is truth in all models under all assignments; the deductive calculus of §2.4 is its finitary syntactic counterpart. ↩
Enderton, §2.4, opening remarks on what constitutes a proof: finiteness and effective checkability, with the promised compactness and enumerability theorems (proved in §2.5) as the necessary and sufficient conditions for finite proofs of logical implication to exist. ↩
Enderton, §2.4; contrast with the free generation of wffs in §1.4 and §2.3. A theorem never has a unique deduction, so its construction tree is not unique, unlike a formula's formation tree. ↩
Enderton, §2.4, Substitution; the atomic case is elaborated as Exercise 1 of that section. ↩
Enderton, §2.4, third remark on tautologies, and Exercise 3: a truth assignment on prime formulas extends to all wffs exactly as in Chapter 1, so tautological implication entails logical implication. Theorem 24B then reduces deducibility from $Γ$ to tautological implication from $Γ \cup Λ$ . ↩
Enderton, §2.4, Final Comments; the meta-language / object-language separation is Enderton's Figure 8. ↩

Deductions from a rule of inference

Substitution

The logical axioms

Tautologies as axioms

Deducibility as tautological implication

A worked deduction

The choice of a syntactic axiom set

Footnotes