Past exam of the year 1 of the computer science course of the University of Oxford / 2015 / Digital systems, linear algebra, introduction to formal proof (resit) / 8

Apply the negation introduction rule to an assumed existential statement and the existential quantifier elimination rule with a fresh witness $u$:The eigenvariable condition holds: $u$ is absent from the surrounding premise, the existential assumption and the exported conclusion $\perp$. Its local assumption is discharged before the final negation introduction rule.

The dot after $\forall x$ gives it scope over the following implication: read the premise as $H=\forall x(P(x)\to Q(x))$. Choose a fresh arbitrary eigenvariable $u$. A natural deduction proof isAt line 6, $u$ is free in no undischarged assumption, so the universal quantifier introduction rule is valid.

The proposed variant is not derivable in a sound first-order logic. For a countermodel, use the two-element domain $\{0,1\}$, interpret both predicates $P,Q$ as $\{0\}$, and assign the free variable $x$ the value 0. Then $\forall x(P(x)\to Q(x))$ is true, as is $P(x)$ under the assignment, but $\forall xQ(x)$ is false at element 1. The premise's bound $x$ and the conclusion's free $x$ have different scopes.Attempting to generalize from $Q(x)$ in the variant would violate the eigenvariable condition, because $x$ remains free in the undischarged assumption $P(x)$.

Let $H=\forall x\forall y(S(x,y)\vee \neg S(x,y))$ and abbreviateAssume $\exists bB(b)$ and eliminate the existential quantifier using a fresh eigenvariable $u$. Inside that subproof, specialize $B(u)$ at $p=u$. Write $s=S(u,u)$. The premise $H$ supplies $s\vee \neg s$, so a disjunction elimination rule finishes the contradiction:Line 7 abbreviates two consecutive universal quantifier elimination rule applications; no new rule is used. The fresh witness $u$ is absent from $H$, the assumed existential statement and the exported $\perp$, so the existential quantifier elimination rule satisfies its eigenvariable condition. This is the self-application behind the barber paradox, written entirely with the supplied rules.

The equality introduction rule is reflexivity, with no premise. The equality elimination rule is substitution of equal first-order terms into a first-order formula:The indicated substitution must be capture-avoiding substitution in first-order logic: the first-order terms must be free for the replaced variable. One can designate a particular argument occurrence by choosing $\varphi (v)$ appropriately; the rule does not demand replacing every occurrence of an identical-looking term in a formula.

For transitivity of first-order equality, take $\varphi (v)$ to be $T_1=v$. The equality elimination rule applied to $T_2=T_3$ and $\varphi (T_2)$ givesFor symmetry of first-order equality, first obtain $T_1=T_1$ by the equality introduction rule. Now take $\psi (v)$ to be $v=T_1$ and substitute using $T_1=T_2$:These choices of formula show exactly which occurrence is replaced, so neither argument assumes the property it is establishing.

Choose fresh arbitrary eigenvariables $u,v$. Under $u=v$, use the equality elimination rule to transport $P(u)$ to $P(v)$. For the reverse direction, first derive $v=u$ by the symmetry derivation above. In full natural deduction form:All temporary assumptions are discharged before either universal quantifier introduction rule application, so both eigenvariable conditions hold. No premises remain: