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 / b / Solution

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.