Past exam of the logic and set theory course of the University of Oxford / 2011 / A / 3 / c

Write $E(x,y)$ for the displayed equality predicate. A6 and A4 give $⊢E(x,x)$, establishing a reflexive relation.

An instance of A7, replacing just the first occurrence of $x$ in $E(x,x)$, isAssume $E(x,y)$, apply the modus ponens rule twice using reflexivity, and obtain $E(y,x)$. The deduction theorem for propositional logic discharges the assumption. This proves symmetry.

For transitivity, A7 suppliesby replacing $y$ in the atomic formula $E(x,y)$. From assumptions $E(x,y)$ and $E(y,z)$, two applications of the modus ponens rule give $E(x,z)$. Discharging assumptions and universally generalizing givesThus the predicate defines an equivalence relation within the calculus.

No such first-order axiom collection can force actual identity when the displayed symbol is treated as an ordinary relation. The duplication obstruction to axiomatizing identity proves this even for an infinite collection of extra axioms.

Start with any nonempty first-order structure $\mathcal{A}$ in which the symbol is identity. Form $B=A\times \{0,1\}$ and the surjection $\pi :B\to A$. Interpret each relation by pulling it back along $\pi$; in particular,Interpret every function on first coordinates as in $\mathcal{A}$ and choose second coordinate zero; likewise lift constants with second coordinate zero. Induction on first-order terms gives $\pi (t^{\mathcal{B}}(v))=t^{\mathcal{A}}(\pi v)$. Induction on first-order formulas then givesThe quantifier steps use surjectivity of $\pi$, so every witness in $A$ lifts to $B$.

Every proposed axiom valid with actual equality is therefore true in $\mathcal{B}$ under every assignment, along with A1–A7. But $E^{\mathcal{B}}((a,0),(a,1))$ holds for two different domain elements. Thus those axioms cannot enforce identity. The usual interpretation of logical equality as identity is a semantic requirement.