How can I prove transitivity of < in Peano Arithmetic

I wish to prove

$$(\forall x)(\forall y)(\forall z)((x < y \land y < z) \rightarrow x < z)$$

only using the rules of Peano Arithmetic (PA) including the induction rule. I have seen other resources here:

Induction proof of transitivity

Prove by induction that P is transitive

but they do not answer my question and I am stuck on performing the induction given several free variables.

• The first important question is: how have you defined $<$? Equally important, what kind of axioms are you using for Peano Arithmetic? – Carl Mummert Mar 11 at 2:28
• I am using the Robinson's Axioms as described here: web.mit.edu/24.242/www/Robinson'sArithmetic.pdf where Q11 defines <. Sorry - this should be been more specific – Nucl3ic Mar 11 at 2:46
• The system of Robinson's Axioms (Q) is not the same as Peano Arithmetic (PA). Most notably, Q does not include induction which makes it a lot weaker .... indeed, note that the reference you provided states how you can't even prove basic commutativity, associativity, or distribution laws in Q ... and I don't see how you can prove transitivity in Q either. So ... are you using Q or are you using PA? – Bram28 Mar 15 at 16:05

We start proving by Induction in the meta-theory:

$$\forall z \ [(\text m < \text n ∧ \text n < z) → (\text m < z)]$$.

Basis : $$z=0$$.

We assume $$(\text m < \text n ∧ \text n < 0)$$; from it : $$(\text n < 0)$$.

From (Ax.Q9) we get : $$\lnot (\text n < 0)$$. Using tautology : $$\lnot p \to (p \to q)$$ we conclude with :

$$(\text m < 0)$$.

Induction step : let assume $$(\text m < \text n ∧ \text n < z) → (\text m < z)$$.

Assume : $$(\text m < \text n ∧ \text n < s(z))$$. From it we get : $$(\text n < s(z))$$.

Using (Ax.Q10) we get : $$(\text n < z) \lor (\text n = z)$$.

Two cases : (a) $$(\text n < z)$$.

With $$(\text m < \text n)$$ and Induction Hyp we get : $$(\text m < z)$$.

(b) $$(\text n = z)$$. Again, using $$(\text m < \text n)$$ and axioms for equality we get : $$(\text m < z)$$.

From $$(\text m < z)$$ we get $$(\text m < z) \lor (\text m = z)$$.

Using (Ax.Q10) we get : $$(\text m < s(z))$$.

Thus, we conclude with :

$$(\text m < \text n ∧ \text n < s(z)) \to (\text m < s(z))$$.

In this way, we have proved by Induction :

$$\forall z \ [(\text m < \text n ∧ \text n < z) \to (\text m < z)]$$.

By Generalization, we have :

$$\forall x \ \forall y \ \forall z \ [(x < y ∧ y < z) \to (x < z)]$$.