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

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.

 Ancestors (12)

There are no discussions about this article yet.

There are currently no matching articles.