Axiom of Double Induction?

What would the set-theoretical axiom of induction look like for double induction^* when stated in the mathematical language of first- or second-order logic?

To questions on this StackExchange:

• 'Double Induction'
• 'Good Examples of Double Induction'
• 'A case of double induction?'
• 'Divisibility Proof with Induction - Stuck on Induction Step' (this answer, in particular…)

To other sources:

• 'Proof method: Multidimensional induction'
• 'Mathematical Induction' (PDF) (See §14.2.4, 'Appendix 2 — The Basic Schemes of Induction: Induction for the Natural Numbers: Double Induction (Weak Form)' on p. 15…)
• 'Mathematical induction: variants and subtleties' (PDF) (See §3, which starts at the end of p. 2…)
• 'Different kinds of Mathematical Induction' (PDF) (See variant 11 at the end of p. 2…)
• 'Proof by Mathematical Induction'/'[The] Principle of Mathematical Induction' (PDF) (See the section on 'Double Induction' that starts at the end of p. 12…)

Here's a straight application of simple induction (not strong induction), twice:

We want to prove $P(m,n)$ by induction over $n$. Thus we need to prove $P(m,0)$ and $P(m,n)\to P(m,n+1)$. But in order to prove $P(m,0)$ we use induction over $m$, so we need to prove $P(0,0)$ and $P(m,0)\to P(m+1,0)$.

In symbols, this amounts to the following assertion:

$$P(0,0)\,\land\,[\forall m,P(m,0)\to P(m+1,0)]\ \land\ [\forall mn,P(m,n)\to P(m,n+1)]\implies\forall xy, P(x,y)$$

In the language of well-founded induction, this corresponds to the order $$(m,n)\prec_1(m',n')\iff (m=m'\land n<n')\lor(n=n'=0\land m<m'),$$ which is not a total order but is well-founded anyway, because there is a (unique) path from $(m,n)$ to the minimum element $(0,0)$ of length $m+n$, so there are no infinite descending sequences.

Alternatively, you could simplify the argument, by encompassing both inductions into one:

We want to prove $P(m,n)$ by induction over $m+n$. Thus we need to prove $P(0,0)$ and $P(m,n)\to P(m,n+1),P(m+1,n)$.

This can be expressed as:

$$P(0,0)\ \land\ [\forall mn,P(m,n)\to P(m+1,n)\land P(m,n+1)]\implies\forall xy, P(x,y)$$

As a partial order, this is talking about the product order on $\Bbb N^2$, that is $$(m,n)\preceq_2(m',n')\iff m\le m'\lor n\le n'.$$ Since this order is an extension of the first one, that is $(m,n)\preceq_1(m',n')$ implies $(m,n)\preceq_2(m',n')$, that means that the first induction theorem is the stronger one (applies to more $P$'s), but the well-foundedness of the second order implies that of the first. The argument is the same: any path from $(m,n)$ to $(0,0)$ must be of length at most $m+n$, so there are no infinite descending sequences.

Using the same partial order, we can even use two values which are less under the order in the induction:

If $P(m-1,n)$ and $P(m,n-1)$ together imply $P(m,n)$ (if one or the other is not defined then this should be provable with the remaining hypothesis), then $P(m,n)$ is true for all $m,n$.

This is a special case of strong induction over $\prec_2$ or simple induction over $z=m+n$ (where the induction hypothesis is $\forall mn,m+n=z\to P(m,n)$).

If we break off the base case and reindex so that it can be written as $P(m+1,n)\land P(m,n+1)\to P(m+1,n+1)$, this leaves the obligations $P(0,0)$, $P(m,0)\to P(m+1,0)$, $P(0,n)\to P(0,n+1)$, and if we simplify this to just $[\forall m,P(m,0)]\land[\forall n,P(0,n)]$, we get the same thing as variant 11 of 'Different kinds of mathematical induction':

If $P(0,n)$ and $P(n,0)$ are true for all $n$, and $P(m+1,n)\land P(m,n+1)\to P(m+1,n+1)$ for all $m,n$, then $P(m,n)$ is true for all $m,n$.

There is yet another alternative approach, which is a bit closer to some of your links:

We want to prove $P(m,n)$, which follows from $\forall n,P(m,n)$. This latter property is proven by induction on $m$, so we need to prove $\forall n,P(0,n)$ and $[\forall n,P(m,n)]\to[\forall n,P(m+1,n)]$. In each case, we have a secondary induction over $n$ to perform.

This translates as:

\begin{align}P(0,0)\ &\land\ [\forall n,P(0,n)\to P(0,n+1)]\ \land\\ (\forall m,[\forall n,P(m,n)]\to P(m+1,0))\ &\land \ \forall mn',[\forall n,P(m,n)]\land P(m+1,n')\to P(m+1,n'+1)\\&\implies\forall xy, P(x,y)\end{align}

In the language of well-orders, this is lexicographic order: $$(m,n)\prec_3(m',n')\iff m<m'\lor(m=m'\land n<n').$$

This last one is easier to state as a strong induction:

We want to prove $P(m,n)$, which follows from $\forall n,P(m,n)$. This is proven by strong induction on $m$, so we need to prove $\forall m'<m,\forall n,P(m',n)$ implies $\forall n,P(m,n)$. The latter for-all is proven by a strong induction over $n$, so assuming additionally that $\forall n'<n,P(m,n')$, we need to prove $P(m,n)$.

Expressed as a closed form rule, this is:

$$\forall m,[\forall m'<m,\forall n,P(m',n)]\to\forall n,[\forall n'<n,P(m,n')]\to P(m,n)\implies\forall xy,P(x,y)$$

which can be simplified to

$$\forall mn,[\forall m'n',m'<m\lor (m=m'\land n<n')\to P(m',n')]\to P(m,n)\implies\forall xy,P(x,y).$$

This is the most generalizable form of the induction principle, using strong instead of simple induction. In general it looks like:

$$\forall x,[\forall x'\prec x,P(x')]\to P(x)\implies\forall y,P(y)$$

where $\prec$ is a well-founded relation or a well-order over the domain. In this case we are using $\prec_3$ as a well-order of $\Bbb N^2$, and the previous cases used $\prec_1$ and $\prec_2$.