How can I prove transitivity of < in Peano Arithmetic

Question

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.

Answer 1

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)]$.