 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/ii/solution

For transitivity of first-order equality, take

ϕ (v)

to be

T_{1} = v

T_{2} = T_{3}

and

ϕ (T_{2})

gives

\frac{T _{2} = T _{3} T _{1} = T _{2}}{T _{1} = T _{3}} = E .

T_{1} = T_{1}

ψ (v)

to be

v = T_{1}

and substitute using

T_{1} = T_{2}

\frac{T _{1} = T _{2} T _{1} = T _{1} = I}{T _{2} = T _{1}} = E .

These choices of formula show exactly which occurrence is replaced, so neither argument assumes the property it is establishing.

 New to topics? Read the docs here!