Past exam of the logic and set theory course of the University of Oxford / 2009 / A / 1

The assertion $\Gamma ⊢\varphi$ means that there is a finite formal derivation ending in $\varphi$ with its undischarged assumptions contained in $\Gamma$. In a context-labelled presentation, an axiom instance is available with empty context, a formula $\alpha$ is available from the context $\{\alpha \}$, modus ponens combines derivations of $\alpha$ and $\alpha \to \beta$ to derive $\beta$, and generalization derives $\forall x\alpha$ provided $x$ is not free in its open assumptions. Thinning enlarges a context without changing its conclusion.

Each line or node must specify an axiom instance, an assumption, or an application of a permitted rule to earlier lines or subderivations. The side conditions on substitution, quantification and contexts are part of correctness. In particular a derivation is a finite syntactic object, even when $\Gamma$ is infinite; it uses only finitely many assumptions before a final thinning to $\Gamma$ if necessary. Derivability $⊢$ is thus distinct in definition from semantic entailment $\models$, which quantifies over structures and assignments.

A term $t$ is free for substitution for $x_i$ in $\alpha$ when none of its variables becomes bound at a free occurrence of $x_i$ being replaced. Equivalently, no quantifier surrounding such an occurrence binds a variable of $t$. Bound occurrences of $x_i$ are not replaced. This occurrence-sensitive condition prevents variable capture.

For example take $\alpha (x)=\exists y\neg (x=y)$ and $t=y$. On a two-element domain, $\forall x\exists y\neg (x=y)$ is true. Naive textual substitution produces $\exists y\neg (y=y)$, which is false on every nonempty domain. Thus the corresponding unrestricted A4 implication would be invalid. The problem is that the inserted free $y$ was captured by the existing existential quantifier. Renaming that binder first instead gives the correct instance $\exists z\neg (y=z)$, with $z$ fresh.

Take $\alpha =\beta =P(x)$ for a unary predicate symbol. The premise $\forall x(P(x)\to P(x))$ is valid, but the proposed conclusion is $P(x)\to \forall xP(x)$. On a domain $\{0,1\}$ with $P=\{0\}$ and assignment $x\mapsto 0$, its antecedent is true and its consequent false.

Hence dropping the condition that $x$ is not free in $\alpha$ would turn a valid premise into an invalid conclusion. The condition permits the antecedent to remain fixed while the quantified variable ranges over the domain; an antecedent depending on that variable cannot be held true for all its values merely because it is true at the current assignment.

Capture-safe equality replacement gives the corrected scheme:where ${\varphi }^{\prime }$ replaces selected free occurrences of $x_i$ by $x_j$, without capture. One may equivalently use full capture-avoiding substitution, after renaming conflicting binders. Replacing bound occurrences as though they were free is not permitted.

Here is a syntactic proof. Write $e$ for $x_i=x_j$. First derive symmetry under $e$: A6 and A4 give $x_i=x_i$, and A7 applied to the first position in that atomic equality gives $e\to (x_i=x_i\to x_j=x_i)$. Modus ponens and the deduction theorem give $⊢e\to x_j=x_i$. Atomic replacement in the forward direction is A7 itself; in the reverse direction apply A7 with $i,j$ exchanged and use this symmetry. Thus under $e$, an atomic formula and its designated replacement imply each other.

Induct on the formation of $\varphi$, proving both directions simultaneously. For negation, the reverse implication for the immediate subformula gives the forward implication of its negations by contraposition, and vice versa. For $\theta \to \eta$, the two induction equivalences combine propositionally to $(\theta \to \eta )\leftrightarrow ({\theta }^{\prime }\to {\eta }^{\prime })$. This uses only the propositional tautologies allowed in this part.

For $\varphi =\forall z\theta$, first take $z$ distinct from $x_i,x_j$. From assumptions $e$ and $\forall z\theta$, A4 gives $\theta$, the induction hypothesis gives ${\theta }^{\prime }$, and generalization gives $\forall z{\theta }^{\prime }$: $z$ is free in neither open assumption. Discharge the two assumptions to obtain $e\to (\forall z\theta \to \forall z{\theta }^{\prime })$. The reverse direction is identical. If the binder is $x_i$, no free occurrence of that variable lies beneath it and the replacement there is empty. If it is $x_j$, capture avoidance likewise forbids a changed free $x_i$ below that binder unless the binder is first renamed to a fresh variable. Bound-variable renaming is derived from A4 followed by admissible generalization and A5, with the same freshness restriction. This completes the structural induction and proves the scheme for arbitrary formulas.

The thinning rule, or weakening, isIt expresses that extra unused assumptions do not destroy a proof. In the context-sensitive predicate-calculus presentation it also allows a theorem first proved with a fresh generalization variable to be used later in a context containing that variable free. Simply replaying the same generalization under the larger context could violate its side condition. For instance a proof of $\forall x(x=x)$ from the empty context may generalize on $x$; it should remain available when an unused assumption $P(x)$ is added, even though that last generalization could not be replayed with $P(x)$ open.

In propositional calculus the axiom schemes and modus ponens have no analogous free-variable restriction. An induction on the original proof simply reuses each axiom, assumption and modus-ponens step under the enlarged assumptions, so weakening is admissible and need not be postulated separately. Context-sensitive Hilbert weakening concerns this proof presentation: systems already tracking only the assumptions on which each line depends can build admissible weakening into their treatment of predicate-calculus generalization as well.