Strong Induction on Two Variables I know that for proving some $P(m,n)$ we can apply induction as follows: prove some base case $P(m_0, n_0)$, an inductive step given $P(m-1,n)$ to show $P(m,n)$, and an inductive step given $P(m,n-1)$ to show $P(m,n)$. However in a proof I am working on I need a stronger hypothesis. In particular, in order to show $P(m,n)$ given $P(m-1,n)$ I also need to assume that $P(m-1,n-k)$ holds for $1\leq k\leq n$ too, a strong induction of sorts. Is this logically sound, and if not what is the issue with it? If it is sound, how much stronger can we get?
 A: One way to do this is to prove $P(1,n)$ for all values of $n\geq1$.  Then make the induction hypothesis that for some $m>1$, $P(m,n)$ is true for all values of $n\geq1$, and prove that $P(m+1,n)$ is true for all values of $n\geq1$.  This proves that that $P(m,n)$ is true for $m\geq1$ and all values of $m$.  In proving that $P(m+1,n)$ is true for all $m,n\geq1$, you are, of course, free to use any sort of induction you choose.
A: Given $P(m, n)$ you can treat $P(m-1, 0), P(m-1, 1), \cdots P(m-1, n)$ as accessible to your induction step, but you can also go further and take all pairs of natural numbers that are smaller lexicographically, which includes statements of the form $P(m-1, \cdot)$.
I think it would help to explicitly pick a set, explicitly pick a partial order on that set, prove that that partial order is a well-order, and then proceed from there.

You can perform induction on any set equipped with a well-order.
Let's define $\le$ on pairs of numbers as follows. This is the lexicographic order on $\mathbb{N} \times \mathbb{N}$.
$$ (a, b) \le (c, d) \;\;\text{iff}\;\; a \le c \lor (a = c \land b \le d) $$
This order is kind of interesting. There are no infinite descending chains, but if we start with $(1, 0)$ in our chain, we can make an arbitrarily long descending chain by picking the next element to be $(0, n)$ for some $n$ in $\mathbb{N}$. The next next element to be $(0, n-1)$ and so on.
In order to convince ourselves that there are no infinite descending chains, we notice that if we start on the row $(n, \cdot)$ then we must reach the row $(n-1, \cdot)$ in finitely many steps. And if we are on the row $(0, \cdot)$ we must reach $(0, 0)$ in finitely many steps. The sum of finitely many finite numbers is finite.
The strong induction schema looks like this. Here, $\implies$ is a low-precedence version of $\to$. $\vec{0}$ is the minimum element of $\le$. Here, $a < b$ is an abbreviation for $a \ne b \land a \le b$.
$$ \bigg((\forall u < x \mathop. \varphi(u)) \to \varphi(x)\bigg) \land \varphi\!\left( \vec{0} \right) \implies (\forall u \mathop. \varphi(u))  $$
