= Solution
Let $H=\forall x\forall y(S(x,y)\lor\neg S(x,y))$ and abbreviate
$$
B(b)=\forall p\,((S(b,p)\to\neg S(p,p))\land(\neg S(p,p)\to S(b,p))).
$$
Assume $\exists b\,B(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\lor\neg s$, so a <disjunction elimination rule> finishes the contradiction:
$$
\begin{array}{rll}
1&H&\text{premise}\\
2&[\exists b\,B(b)]^a&\text{assumption}\\
3&\quad[B(u)]^b&\text{fresh witness assumption}\\
4&\qquad(s\to\neg s)\land(\neg s\to s)&\forall E\ 3\ (p=u)\\
5&\qquad s\to\neg s&\land E\ 4\\
6&\qquad\neg s\to s&\land E\ 4\\
7&\qquad s\lor\neg s&\forall E\text{ twice on }1\ (x=y=u)\\
8&\qquad[s]^c&\text{assumption}\\
9&\qquad\quad\neg s&\to E\ 8,5\\
10&\qquad\quad\bot&\neg E\ 8,9\\
11&\qquad[\neg s]^d&\text{assumption}\\
12&\qquad\quad s&\to E\ 11,6\\
13&\qquad\quad\bot&\neg E\ 12,11\\
14&\qquad\bot&\lor E\ 7,(8\text{--}10),(11\text{--}13)\\
15&\quad\bot&\exists E\ 2,(3\text{--}14)\\
16&\neg\exists b\,B(b)&\neg I\ (2\text{--}15).
\end{array}
$$
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 $\bot$, 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.
$$
\boxed{H\vdash\neg\exists b\,\forall p\,((S(b,p)\to\neg S(p,p))\land(\neg S(p,p)\to S(b,p))).}
$$
Back to article page
