1

Here is a problem from Enderton's Mathematical Introduction to Logic:

Show that $$\vdash \forall \,x\,\forall\,y\,\forall\,z\,(x = y \rightarrow y = z \rightarrow x = z)$$

One thought I have for this problem are that for proving deduction, I can use equality axiom and rule T. I know this works for reflexivity, but I'm not sure if this proof applies for transitivity.

Any suggestions or comments?

NasuSama
  • 3,364
  • I think you need parentheses. I suspect you need: $$\vdash \forall ,x,\forall,y,\forall,z,\Big(x = y \rightarrow (y = z \rightarrow x = z)\Big)$$ In any case, the conditional connective is not associative. – amWhy Nov 27 '13 at 22:31
  • 1
    @amWhy: it is certainly not associative, but a common convention is to make it right-associative when there are not explicit parentheses. So $A \to B \to C$ is read as $A \to ( B \to C)$. This convention is particularly helpful in on contexts related to type theory and the Curry-Howard isomorphism between $A \times B \to C$ and $A \to B \to C$. – Carl Mummert Nov 27 '13 at 23:48

1 Answers1

2

You need Enderton's version of Leibniz's Law -- see p. 112 in the second edition -- that is to say $\xi = \zeta \to (\varphi(\xi) \to \varphi(\zeta))$.

Suppose (1) $x = y$

Insert here derivation of (1a) $y = x$

Suppose (2) $y = z$

By Leibniz's Law, $y = x \to \varphi(y) \to \varphi(x)$, with $\varphi(y)$ as $y = z$, we get (3) $x = z$.

Use the deduction theorem twice to get $(1) \to ((2) \to (3))$, i.e.

Discharging suppositions, $x = y \to (y = z \to x = z)$

Generalizing on all variables (in three steps), $\forall x\forall y\forall z(x = y \to (y = z \to x = z))$

Community
  • 1
Peter Smith
  • 54,743
  • Wow. You didn't use Rule T and generalization theorem for this problem. Very good approach clearer than Enderton's info from the book. Enderton's approaches for exercises and proofs are so loose and brief. Thanks for the answer! It does make sense! – NasuSama Nov 29 '13 at 03:45