 Solution

ID: 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/c/iii/solution

Choose fresh arbitrary eigenvariables

u, v

. Under

u = v

P (u)

P (v)

. For the reverse direction, first derive

v = u

by the symmetry derivation above. In full natural deduction form:

12345678910111213 [u = v]^{a} [P (u)]^{b} P (v) P (u) \to P (v) u = u v = u [P (v)]^{c} P (u) P (v) \to P (u) (P (u) \to P (v)) \land (P (v) \to P (u)) u = v \to ((P (u) \to P (v)) \land (P (v) \to P (u))) \forall y (u = y \to ((P (u) \to P (y)) \land (P (y) \to P (u)))) \forall x \forall y (x = y \to ((P (x) \to P (y)) \land (P (y) \to P (x)))) assumption assumption = E 1, 2 \to I (2 - 3) = I = E 1, 5 (ϕ (w) \equiv w = u) assumption = E 6, 7 \to I (7 - 8) \land I 4, 9 \to I (1 - 10) \forall I 11 \forall I 12.

⊢ \forall x \forall y (x = y \to ((P (x) \to P (y)) \land (P (y) \to P (x)))) .

 New to topics? Read the docs here!