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

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.

With generalization restricted to variables not free in open assumptions, the deduction theorem statesThe reverse direction follows by thinning and modus ponens. For the forward direction, induct on a derivation, keeping track of its actual assumption contexts. Axioms and assumptions already in $\Gamma$ yield $\alpha \to \chi$ by A1; the distinguished assumption $\alpha$ yields the permitted theorem $\alpha \to \alpha$. If a line $\chi$ is obtained by modus ponens from $\eta$ and $\eta \to \chi$, the induction hypotheses and A2 derive $\alpha \to \chi$.

If a generalization step depends on the discharged assumption, its variable $x$ is not free in $\alpha$ or the other open assumptions. Generalize the induction conclusion $\alpha \to \eta$ to $\forall x(\alpha \to \eta )$ and use A5 to derive $\alpha \to \forall x\eta$. If the subderivation does not depend on $\alpha$, its generalized conclusion can instead be retained as an independent derivation and A1 applied afterwards. Thinning merely enlarges the remaining context and preserves the induction claim. These cases are why assumption dependence, rather than a careless unrestricted universal rule, is essential.

In a presentation allowing generalization freely from hypotheses, the corresponding theorem must instead explicitly require that no variable free in $\alpha$ is generalized in an $\alpha$-dependent line. Without that restriction $P(x)⊢\forall xP(x)$ would incorrectly yield $⊢P(x)\to \forall xP(x)$.

A first-order structure consists of a nonempty domain $A$, an interpretation $c^A\in A$ of each constant symbol, a total function $f^A:A^n\to A$ for each $n$-ary function symbol, and a relation $R^A\subseteq A^n$ for each $n$-ary predicate symbol. Logical equality is interpreted as actual identity.

An assignment in a first-order structure is a map $s$ from the variables into $A$. It extends recursively to terms: $x^A[s]=s(x)$, $c^A[s]=c^A$, and $f(t_1,\dots ,t_n{)}^A[s]=f^A(t_1^A[s],\dots ,t_n^A[s])$. Atomic truth is determined by membership of the resulting tuple in $R^A$, or equality of the two term values. Negation reverses the truth value, and an implication is false exactly when its antecedent is true and its consequent false.

For a universal quantifier,These clauses define a valuation on every formula by structural recursion. Only free-variable values affect a formula's truth; consequently a sentence has the same truth value under every assignment. This is a semantic assignment of domain elements, not a programming assignment operation.

Fix any structure and any assignment of the three quantified variables, writing their values as $a_0,a_1,a_2$. If either of the nested antecedents is false, the corresponding implication is true. If both are true, then $f^A(a_0)=a_1$ and $f^A(a_0)=a_2$. Actual identity is transitive, so $a_1=a_2$, making the consequent true as well.

Thus the unquantified matrix is true under every assignment in every structure. The universal-quantifier semantic clause then makes its universal closure true in every structure:No assumption that $f$ is injective is used. The argument says that one value cannot equal two distinct elements, not that distinct inputs have distinct outputs.

Choose a fresh variable $x_3$. In A7 take the equality antecedent $x_3=x_1$, the atomic formula $\varphi =(x_3=x_2)$, and replace its occurrence of $x_3$ by $x_1$. This gives directly the theoremGeneralize on $x_3$, with no open assumptions. A4 then instantiates that quantifier with the term $f(x_0)$. The substitution is free for $x_3$, since the matrix contains no quantifiers. One modus-ponens step yieldsFinally generalize, in order, on $x_2$, $x_1$, and $x_0$. The result isEvery step is A7, generalization, A4, or modus ponens. Neither completeness, adequacy, nor an unproved appeal to all propositional tautologies is needed. In particular the proof does not silently upgrade the variable-only equality axiom to an arbitrary-term axiom: quantification and instantiation perform that upgrade explicitly.

Adequacy here means functional completeness: every Boolean truth function of finitely many positive-arity propositional inputs can be expressed by a formula using the available connectives. It is an expressive-power claim, distinct from the completeness theorem relating derivability and semantic entailment.

Negation and implication define conjunction and disjunction byGiven any truth table, for each input row where its output is true form the minterm containing each input positively or negatively according to that row. The disjunction of these minterms is true on exactly the required rows: a disjunctive normal form. Replacing its conjunctions and disjunctions by the displayed definitions gives a formula using only $\neg ,\to$.

The constantly true and constantly false functions are represented by $p\to p$ and $\neg (p\to p)$, using a dummy input if needed. Thus the empty or full truth table also causes no difficulty. If one insists on genuinely nullary formulas with no variables at all, a separate truth constant is needed; ordinary propositional adequacy allows the constant truth functions to be expressed with irrelevant input variables.

There are sixteen binary Boolean functions, one for each four-bit truth table. Exactly eight give an adequate basis together with negation.

The eight affine functions are $0,1,p,\neg p,q,\neg q,p\oplus q,\neg (p\oplus q)$. Each is affine over the field with two elements, and composition with other affine functions or negation remains affine. Since conjunction is not affine, none of these eight bases is adequate.

Each remaining truth table has either one true row or three true rows. In the latter case negate its output to obtain a function with one true row. Negate selected inputs to move that row to $(1,1)$: the resulting function is conjunction. Conjunction together with negation expresses every disjunctive normal form, proving adequacy of all remaining eight. They are AND, NAND, OR, NOR, the two directed implications, and the two asymmetric conjunctions $p\wedge \neg q$, $\neg p\wedge q$. The count treats the binary connective by its truth function rather than by arbitrary choices of its printed symbol.

A graph must assign exactly one output to every input, while the distinguished unary predicate must select exactly one element. Suitable sentences areThe existential clauses provide totality and nonemptiness of the selected output, respectively; the universal clauses provide uniqueness. Thus a structure satisfying $\varphi ,\psi$ uniquely determines a total unary function $f$ and a constant $c$ on its unchanged domain. Conversely any interpretations of $f,c$ determine such relations by $P(x,y)⟺f(x)=y$ and $Q(x)⟺x=c$.

For each term $t$ define an $L_2$-formula $E_t(z)$ expressing its value. Use fresh bound variables at every step:Freshness includes avoiding all relevant free variables of the formula being translated. Define the atomic translation byand extend through the logical operations: $\sigma (\neg \theta )=\neg \sigma (\theta )$, $\sigma (\theta \to \eta )=\sigma (\theta )\to \sigma (\eta )$, and $\sigma (\forall x\theta )=\forall x\sigma (\theta )$. Fresh witnesses prevent variable capture and ensure the translation preserves the original free-variable set.

For an $L_1$-structure $A$, let $A^r$ have the graph relation of $f^A$ and singleton relation $\{c^A\}$. Induction on terms proves that $E_t(z)$ holds precisely when $z$ is the value of $t$. Induction on formulas then provesConversely every $L_2$-structure satisfying $\varphi ,\psi$ is uniquely the relational version of an $L_1$-structure on that same domain. Hence, for arbitrary possibly infinite $\Gamma$, semantic entailment on the left is equivalent to semantic entailment from $\sigma (\Gamma )\cup \{\varphi ,\psi \}$ on the right, with assignments retained in the free-formula case. Applying soundness theorem for first-order logic and Gödel's completeness theorem givesThe prohibition on completeness in the preceding direct equality question is local to that proof; here it supplies the clean semantic-to-syntactic transfer after the actual translation and model correspondence have been established.

Replace each $n$-ary function symbol by an $(n+1)$-ary graph predicate, with axioms asserting exactly one output for each input tuple. Replace each constant by a unary predicate asserted to hold of exactly one element. Recursively introduce witnesses for term values, then translate formulas through their logical connectives and quantifiers as above.

Every original structure has a unique corresponding relational structure satisfying these axioms, on exactly the same carrier, and every such relational structure reconstructs the original functions and constants. Truth under assignments and logical consequences are preserved in both directions. In this precise relative sense, purely relational languages are adequate to represent first-order languages with functions and constants: expressive power is retained after adjoining the graph and uniqueness axioms. Arbitrary relational interpretations that fail those axioms are not claimed to represent functions.

Neither constants alone nor functions alone gives the same uniform adequacy on all nonempty carriers. A one-element set has exactly one interpretation of each function symbol of any finite arity and of every constant symbol. In contrast it has two interpretations of a unary predicate: empty or full. Thus a fixed purely functional or constant-only language has only one structure on that singleton, and cannot encode both truth values of $\exists xP(x)$ by a same-carrier truth-preserving translation with reconstruction. This is the singleton truth-preservation obstruction to expressive completeness, even when logical equality is available.

Constants alone also cannot represent general variable-dependent relations on larger infinite carriers: a fixed formula mentions only finitely many named elements, and its remaining equality tests do not encode an arbitrary binary relation. Functions offer more flexibility. On carriers with at least two elements, predicates can be encoded by characteristic functions taking two distinguished values, and constants can be represented by constant-valued unary functions if explicit constant symbols are forbidden. Such a construction can work after adding axioms for distinct truth markers, but those axioms exclude the singleton case. Enlarging the carrier or adding a Boolean sort is another possible encoding; it changes the same-carrier sense established in the preceding part and must not be silently identified with it.