Introduction to Logic

Starting with the axioms for e given in Section 11.6, it is possible to prove that e is transitive, i.e. ∀x.∀y.∀z.(e(x,y) ∧ e(y,z) ⇒ e(x,z)). Doing this requires a three variable induction, and it is quite messy. Your job in this problem is to prove just the base case for the outermost induction, i.e. prove ∀y.∀z.(e(a,y) ∧ e(y,z) ⇒ e(a,z)). Hint: Use the strategy illustrated in section 10.6. Extra credit: Do the full proof of transitivity.

Show Instructions
Herbrand
Objects a, b, c
Functions f, g
Goal  Incomplete