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

For transitivity of first-order equality, take the substitution formula

ϕ (u) \equiv (T_{1} = u)

1  T₁ = T₂  premise
2  T₂ = T₃  premise
3  T₁ = T₃  =-elim 2,1; φ(u) := (T₁ = u)

For symmetry, use reflexivity and

ψ (u) \equiv (u = T_{1})

1  T₁ = T₂  premise
2  T₁ = T₁  =-intro
3  T₂ = T₁  =-elim 1,2; ψ(u) := (u = T₁)

Thus both transitivity and symmetry follow from the two equality rules. In the symmetry proof, only the designated first occurrence in

T_{1} = T_{1}

is replaced; the second remains fixed.

 New to topics? Read the docs here!