Past exam of the year 1 of the computer science course of the University of Oxford / 2014 / Digital systems, linear algebra, introduction to formal proof / 8 / c

t_{1} = t_{1}

ϕ (z)

to be

z = t_{1}

. Substituting

t_{2}

for

t_{1}

Line	Context	Formula	Justification
1	${1}$	$t_{1} = t_{2}$	Premise
2	${1}$	$t_{1} = t_{1}$	equality introduction rule $= -intro$
3	${1}$	$t_{2} = t_{1}$	equality elimination rule $= -elim$ on 1, 2

Thus

t_{1} = t_{2} ⊢ t_{2} = t_{1}

. This uses only the two supplied equality rules; symmetry has not been assumed as an additional rule.

ii

Eliminate the existential premise with fresh witness

a

. Its first conjunct gives

Q (a)

and its second gives

\forall y (Q (y) \to y = a)

. For a fresh arbitrary

b

, one direction of the desired logical biconditional follows by universal elimination. For the other,

b = a

must be reversed before transporting

Q (a)

Q (b)

using the supplied oriented equality elimination rule.

Line	Context	Formula	Justification
1	${1}$	$\exists x (Q (x) \land \forall y (Q (y) \to y = x))$	Premise
2	${1, 2}$	$Q (a) \land \forall y (Q (y) \to y = a)$	Temporary assumption
3	${1, 2}$	$Q (a)$	conjunction elimination rule $\land -elim-L$ on 2
4	${1, 2}$	$\forall y (Q (y) \to y = a)$	conjunction elimination rule $\land -elim-R$ on 2
5	${1, 2}$	$Q (b) \to b = a$	universal elimination $\forall -elim$ on 4; instantiate at $b$
6	${1, 2, 6}$	$b = a$	Temporary assumption
7	${1, 2, 6}$	$b = b$	equality introduction rule $= -intro$
8	${1, 2, 6}$	$a = b$	equality elimination rule $= -elim$ on 6, 7
9	${1, 2, 6}$	$Q (b)$	equality elimination rule $= -elim$ on 8, 3
10	${1, 2}$	$b = a \to Q (b)$	implication introduction rule $\to -intro$ on 9; discharge 6
11	${1, 2}$	$Q (b) \leftrightarrow b = a$	biconditional introduction rule $\leftrightarrow -intro$ on 5, 10
12	${1, 2}$	$\forall y (Q (y) \leftrightarrow y = a)$	universal introduction $\forall -intro$ on 11; $b$ fresh
13	${1, 2}$	$\exists x \forall y (Q (y) \leftrightarrow y = x)$	existential quantifier introduction rule $\exists -intro$ on 12; witness $a$
14	${1}$	$\exists x \forall y (Q (y) \leftrightarrow y = x)$	existential quantifier elimination rule $\exists -elim$ on 1, 13; discharge 2; $a$ fresh

Here

b

is absent from every open assumption when line 12 uses universal introduction. In line 13 the existential quantifier binds the witness position occupied by