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

Table of contents
- Solution ii

Solution

For transitivity of first-order equality, take

ϕ (v)

to be

T_{1} = v

. The equality elimination rule applied to

T_{2} = T_{3}

and

ϕ (T_{2})

gives

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

For symmetry of first-order equality, first obtain

T_{1} = T_{1}

by the equality introduction rule. Now take

ψ (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.

 Ancestors (12)

 View article source

 Discussion (0) New discussion

There are no discussions about this article yet.

 Articles by others on the same topic (0)

There are currently no matching articles.

  See all articles in the same topic Create my own version