Formal induction over two variables

Question

Induction.

According to the Peano Axioms in this article https://en.wikipedia.org/wiki/Peano_axioms, one axioms states that if $\varphi$ is a unary predicate such that $\varphi(0)$ is true and $$\forall n \in \mathbf{N}[\varphi(n) \implies \varphi(s(n))],$$ then $\forall n \in \mathbf{N}[P(n)]$ is true.

This does not allow $n$-ary predicates for $n \geq 2$, however I have seen that induction can be used for those as well. What is the formal reason for that?

Example.

Consider a formula of the form $\forall n (\forall m [(m \in \mathbf{N} \wedge n \in \mathbf{N}) \implies P(m,n)])$ (I hope this is a correct translation of "For all $n \in \mathbf{N}$ and for all $m \in \mathbf{N}$ the statement $P(m,n)$ is true"). One can prove this statement in the following way. Let $n \in \mathbf{N}$ and $m \in \mathbf{N}$. Then (...) and thus $P(n,m)$. Now, I have read that I can prove such a statement by induction the following way. Let $n \in \mathbf{N}$, that is, fix an element $n$. Prove $P(0,n)$ and for all $k \in \mathbf{N}$ with $P(k,n)$ show that $P(s(k),n)$ is true as well. Now, if I could apply induction to this, one could deduce $\forall m \in \mathbf{N} [P(m,n)] (*).$ Since $n$ was arbitrary, it holds that $\forall n (\forall m[m \in \mathbf{N} \wedge n \in \mathbf{N} \implies P(m,n)]).$

Questions.

The argument of my example, if correct, needs that induction can be applied to predicates of the form $P(m,n)$. $(1)$ Why can this be done/Why is this formally possible?

$(2)$ I have also read the following question Complete Induction on two variables, in which the answer defines $Q(x)=\forall y P(x,y)$. However, is $Q(x)$ then a valid unary predicate, that is, if $P(x,y)$ is a predicate, then $\forall y P(x,y)$ is a unary predicate?

$(3)$ I have also read the following question Double induction. Here the answer says that the formula $\forall m P(m,n)$ is not a sentence and can thus not be proven. However, in $(*)$ I have a similar expression. Did I do something wrong in my argument above?

Answer 1

The argument of my example, if correct, needs that induction can be applied to predicates of the form $P(m,n)$. $(1)$ Why can this be done/Why is this formally possible?

Note that in the example proof you gave, you fix the $n$, and then do induction over $m$. So in that sense the formula $P(m,n)$ really has only one variable: $m$.

$(2)$ I have also read the following question Complete Induction on two variables, in which the answer defines $Q(x)=\forall y P(x,y)$. However, is $Q(x)$ then a valid unary predicate, that is, if $P(x,y)$ is a predicate, then $\forall y P(x,y)$ is a unary predicate?

Here it is even more clear that $Q(x) = \forall y P(x,y)$ is a formula with one unbounded variable $x$. The predicate $P(x,y)$ is still a 2-place predicate, but the formula $\forall y P(x,y)$ has only one free variable. So yes, that fits the Peano Axiom scheme just fine.

$(3)$ I have also read the following question Double induction. Here the answer says that the formula $\forall m P(m,n)$ is not a sentence and can thus not be proven. However, in $(*)$ I have a similar expression. Did I do something wrong in my argument above?

Again, your argument started by saying the $n$ is some arbitrary number: it is the start of any universal proof, where we try to prove $\phi(n)$ and, since $n$ was assumed to be arbtrarily picked, we can then conclude $\forall n \ \phi(n)$. So, within that context of a universal proof, we can treat $\forall m P(m,n)$ as a sentence, even if we don't know what $n$ exactly is, and thus also don't know what $\forall m P(m,n)$ exactly says.

Answer 2

A simple reason that induction works on $n$-ary formulae/predicates is that you can use iterated induction on unary formulae to derive induction on $n$-ary predicates. There is also the method you state. Lets look at the former. Suppose you want to prove $\forall n\in\mathbb{N} \forall m\in\mathbb{N} \phi(n,m)$. We can do this by induction on $n$ in the formula $\forall m\in\mathbb{N} \phi(n,m)$. This is in fact a formula. Since it is a formula with one free variable, it is akin to unary predicate. It just might not be atomic. Now, via induction, our problem has been reduced to proving $\forall m\in\mathbb{N}\phi(0,m)$ and showing that $\forall n\in\mathbb{N}(\forall m\in\mathbb{N}\phi(n,m)\rightarrow\forall m\in\mathbb{N}\phi(S(n),m))$. Proving $\forall m\in\mathbb{N}\phi(0,m)$ can be done by induction on the formula $\phi(0,m)$, i.e., show $\phi(0,0)$ and $\phi(0,m)$ implies $\phi(0,S(m))$. Similarly, assuming the inductive hypothesis, one can prove $\forall m\in\mathbb{N}\phi(S(n),m)$ by induction on $m$.

So, formally, $n$-ary induction can be reduced to iterated unary induction. However, this is not always done in practice. You will see, as you mentioned, proofs of the form "take an arbitrary $n\in\mathbb{N}$, and prove $\phi(n,m)$ by induction on $m$. This is often more economical than iterated induction. The formal reason this work is due to the constructor for dependent functions ($\Pi$-types). Some times (mostly in the context of natural deduction) this is called $\forall$-introduction.

Aside - The reason induction works is due to the eliminator rules for the type $\mathbb{N}$. Using the eliminator rules for $\mathbb{N}$ and using the constructor for $\Pi$-types with the assumption $(n : \mathbb{N})$ both serve to do the same thing -- define a dependent function out of $\mathbb{N}$.