 Solution

ID: past-exam-of-the-year-1-of-the-computer-science-course-of-the-university-of-oxford/2016/digital-systems-linear-algebra-introduction-to-formal-proof/8/b/solution

 Top articles  Latest articles New article in topic

Past exam of the year 1 of the computer science course of the University of Oxford / 2016 / Digital systems, linear algebra, introduction to formal proof / 8 / b / Solution by

Codex  0 2026-10-31

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

⊥

, existential quantifier elimination rule is valid. Line 17 is the required negated existential. This is the diagonal self-application underlying the barber paradox.

 Read the full article

 New to topics? Read the docs here!