# Induction with two variables in PA

This probably has been asked before, but apologies, I don't know how to locate it. I want to prove $$\forall x,y: P(x, y)$$. My premises are:

$$P(0, 0) \wedge \\ [\forall x: P(x, 0)] \wedge \\ [\forall y: P(0, y)] \wedge \\ [\forall x,y: P(x, y) \Rightarrow P(Suc(x), Suc(y))]$$

I can prove some basic facts in PA, such as addition is comm, assoc, etc. I can also prove things about less than, such as less than is transitive. Also, if x is less than or equal to y, then there exists a z such x + z = y. But I'm not good at induction with two variables, and so cannot complete the proof.

• Not necessarily by double induction. You can prove $\forall y P(n,y)$ by induction on $y$, with $n$ whatever. If the proof works without any specific assumption regarding $n$, you can generalize on it, getting : $\forall x \ \forall y P(x,y)$. – Mauro ALLEGRANZA Dec 2 '18 at 13:24
• See also the post : Induction on two integer variables. – Mauro ALLEGRANZA Dec 2 '18 at 13:27
• – Mauro ALLEGRANZA Dec 2 '18 at 13:28
• $P(n, 0)$ is proven by the second assumption. However, I don't see how $\forall y : P(n, y) \Rightarrow P(n, Suc(y))$ is proven, because I only have $\forall n, y : P(n, y) \Rightarrow P(Suc(n), Suc(y))$. What am I not grasping? Also, I've seen those two links before, but thank you for sending them as they definitely contain helpful tricks for proof by induction. – anon44508 Dec 2 '18 at 14:27
• Nevermind, the other contributor cleared it all up. Thank you for your help. – anon44508 Dec 3 '18 at 2:36

## 1 Answer

Here's a proof in Fitch, which has a built in Peano Induction rule:

As you can see, the only 'trick' is to just ignore the inductive hypothesis for the inside inductive proof, but instead to use the inductive hypothesis for the outside inductive proof

• Thanks for the mechanically verified proof! – anon44508 Dec 3 '18 at 2:33
• @anon44508 You're welcome! :) – Bram28 Dec 3 '18 at 12:06