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.

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

![enter image description here](

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