= Solution
Write $H(t)=\forall p\,((S(t,p)\to\neg S(p,p))\land(\neg S(p,p)\to S(t,p)))$. Use <negation introduction> on the existential claim. For its fresh witness $b$, instantiate $p=b$; the resulting self-application says both $S(b,b)\to\neg S(b,b)$ and its reverse. The given <law of excluded middle> then provides the two cases.
``
1 ∀x. ∀y. (S(x,y) ∨ ¬S(x,y)) premise
2 | ∃b. H(b) assumption
3 | | H(b) assumption, b fresh
4 | | (S(b,b) → ¬S(b,b)) ∧ (¬S(b,b) → S(b,b)) ∀-elim 3, p := b
5 | | S(b,b) → ¬S(b,b) ∧-elim-L 4
6 | | ¬S(b,b) → S(b,b) ∧-elim-R 4
7 | | ∀y. (S(b,y) ∨ ¬S(b,y)) ∀-elim 1, x := b
8 | | S(b,b) ∨ ¬S(b,b) ∀-elim 7, y := b
9 | | | S(b,b) assumption
10 | | | ¬S(b,b) →-elim 5,9
11 | | | ⊥ ¬-elim 9,10
12 | | | ¬S(b,b) assumption (new case)
13 | | | S(b,b) →-elim 6,12
14 | | | ⊥ ¬-elim 13,12
15 | | ⊥ ∨-elim 8,9–11,12–14
16 | ⊥ ∃-elim 2,3–15
17 ¬∃b. H(b) ¬-intro 2–16
``
Both case assumptions are discharged at line 15; the witness assumption is discharged at line 16. Since $b$ is absent from the surrounding premise and the exported conclusion $\bot$, <existential quantifier elimination rule> is valid. Line 17 is \b[the required negated existential]. This is the diagonal self-application underlying the <barber paradox>.
Back to article page
