Proof of the Principle of Double Induction I'm working through the exercises in Hrabaceck and Jeck's introductory book on set theory and I'm having some trouble with the proof of the double induction principle. The result is stated as follows: if given fixed $n,m$
$(\forall k)(\forall l)((k<m\vee(k=m\wedge l<n))\Rightarrow P(k,l))\Rightarrow P(m,n)$ (*)
holds, then $P(n,m)$ holds for all $n,m$.
My idea is to try and show that the property $Q(m)=(\forall l)P(m,l)$ holds for all values of $m$, so I assume
$(\forall k)(k<m\Rightarrow(\forall l)P(k,l))$ ($(\forall k)(k<m\Rightarrow Q(k))$)
in an attempt to show that this (together with (*)) implies $Q(m)$  and then use strong induction to conclude the proof.
I'm really not sure where to go from here. Or rather, I seem to get to the answer I'm looking for but I only use strong induction once, which is odd, and makes me think I'm doing something wrong, but I can't find the mistake. I've seen another post with a very similar question about the exact same exercise, but it don't find the answers in there very helpful.
 A: Let us try to walk through the proof methodically. I will write $\mathscr{Ens}$ to succinctly denote the collection of axioms&schemata of Set Theory. Given the hypothesis:
$$R\colon \equiv(\forall m)(\forall n)(m, n \in \mathbb{N} \Rightarrow [(\forall k)(\forall l)((k<m \wedge l \in \mathbb{N})\vee (k=m \wedge l<n) \Rightarrow P(k, l)) \Rightarrow P(m, n)]),$$
we shall establish that:
$$\mathscr{Ens}, R \vdash (\forall m)(\forall n)(m, n \in \mathbb{N} \Rightarrow P(m, n)). \tag{0}$$
However, we have in $\mathscr{Ens}$ (actually it suffices to consider only the purely logical part, disregarding the axioms which concern sets) the equivalence:
$$(\forall m)(\forall n)(m, n \in \mathbb{N} \Rightarrow P(m, n)) \Leftrightarrow (\forall m)(m \in \mathbb{N} \Rightarrow (\forall n)(n \in \mathbb{N} \Rightarrow P(m, n))),$$
so in order to prove (0) it will suffice to establish that:
$$\mathscr{Ens}, R \vdash (\forall m)(m \in \mathbb{N} \Rightarrow Q(m)), \tag{1}$$
where as you quite appropriately indicated we introduce:
$$Q(m)\colon \equiv (\forall n)(n \in \mathbb{N} \Rightarrow P(m, n)).$$
By virtue of the principle of induction in its so-called "strong" form, in order to establish (1) it suffices to prove that:
$$\mathscr{Ens}, R \vdash (\forall m)(m \in \mathbb{N} \Rightarrow ((\forall k)(k<m \Rightarrow Q(k))\Rightarrow Q(m))). \tag{1'}$$
Since neither $\mathscr{Ens}$ nor $R$ contain any letters (variables) -- in other words, the theory whose list of axioms&schemata is given by $\mathscr{Ens}$ together with $R$ has no constants -- it suffices to establish the dequantified version of (1'):
$$\mathscr{Ens}, R \vdash m \in \mathbb{N} \Rightarrow ((\forall k)(k<m \Rightarrow Q(k))\Rightarrow Q(m)), \tag{1''}$$
since requantification is possible (over letters which are not constants). Appealing to the Metatheorem of Deduction, in order to prove (1'') it will suffice to establish:
$$\mathscr{Ens}, R, m \in \mathbb{N} \vdash (\forall k)(k<m \Rightarrow Q(k))\Rightarrow Q(m), \tag{1'''}$$
and by once again applying this metatheorem to reduce to:
$$\mathscr{Ens}, R, m \in \mathbb{N}, (\forall k)(k<m \Rightarrow Q(k)) \vdash Q(m). \tag{1''''}$$
Resorting once again to the strong form of the induction principle, in order to prove (1'''') it will suffice to show that:
$$\mathscr{Ens}, R, m \in \mathbb{N}, (\forall k)(k<m \Rightarrow Q(k)) \vdash (\forall n)(n \in \mathbb{N} \Rightarrow [(\forall l)(l<n \Rightarrow P(m, l)) \Rightarrow P(m, n)]). \tag{2}$$
Since the letter $n$ is not found amongst the constants of the theory described by the collection of $\mathscr{Ens}, R, m \in \mathbb{N}, (\forall k)(k<m \Rightarrow Q(k))$ -- whose only constant is $m$, a distinct letter -- in order to prove (2) establishing the dequantified version:
$$\mathscr{Ens}, R, m \in \mathbb{N}, (\forall k)(k<m \Rightarrow Q(k)) \vdash n \in \mathbb{N} \Rightarrow [(\forall l)(l<n \Rightarrow P(m, l)) \Rightarrow P(m, n)] \tag{2'}$$
will suffice, by the same token mentioned above of dequantification/requantification over non-constants. Similarly, by once again appealing to the metatheorem of deduction, proving (2') will be achieved as long as we establish that:
$$\mathscr{Ens}, R, m, n \in \mathbb{N}, (\forall k)(k<m \Rightarrow Q(k)) \vdash (\forall l)(l<n \Rightarrow P(m, l)) \Rightarrow P(m, n), \tag{2''}$$
and a further application of the metatheorem of deduction reduces our task to that of establishing:
$$\mathscr{Ens}, R, m, n \in \mathbb{N}, (\forall k)(k<m \Rightarrow Q(k)), (\forall l)(l<n \Rightarrow P(m, l)) \vdash P(m, n). \tag{2'''}$$
For simplicity, let $\mathscr{T}$ denote the theory whose list of axioms&schemata is given by the collection $\mathscr{Ens}, R, m, n \in \mathbb{N}, (\forall k)(k<m \Rightarrow Q(k)), (\forall l)(l<n \Rightarrow P(m, l))$. Since $R$ is obviously deducible from $\mathscr{T}$, we can also deduce the dequantified version:
$$\mathscr{T} \vdash m, n \in \mathbb{N} \Rightarrow [(\forall k)(\forall l)((k<m \wedge l \in \mathbb{N})\vee (k=m \wedge l<n) \Rightarrow P(k, l)) \Rightarrow P(m, n)]. \tag{3}$$
Since furthermore $m, n \in \mathbb{N}$ is also deducible from $\mathscr{T}$ we gather by applying modus ponens to (3) that:
$$\mathscr{T} \vdash (\forall k)(\forall l)((k<m \wedge l \in \mathbb{N}) \vee (k=m \wedge l<n) \Rightarrow P(k, l)) \Rightarrow P(m, n). \tag{4}$$
In order to prove that $\mathscr{T} \vdash P(m, n)$, it will suffice by virtue of the modus ponens method of deduction to establish that the antecedent of the implication at (4) is also deducible from $\mathscr{T}$, in other words that: $$\mathscr{T} \vdash (\forall k)(\forall l)((k<m \wedge l \in \mathbb{N}) \vee (k=m \wedge l<n) \Rightarrow P(k, l)). \tag{5}$$
Since the only constants of $\mathscr{T}$ are $m$ and $n$ -- which are distinct from $k$ and $l$ -- in order to prove (5) it will suffice to prove the dequantified version:
$\mathscr{T} \vdash (k<m \wedge l \in \mathbb{N}) \vee (k=m \wedge l<n) \Rightarrow P(k, l), \tag{5'}$
by the same token of dequantification/requantification that we have already mentioned a number of times. In its own turn, relation (5') can be deduced by virtue of the method of disjunction of cases as long as we separately establish that:
$$\mathscr{T} \vdash (k<m \wedge l \in \mathbb{N}) \Rightarrow P(k, l) \tag{6a}$$
respectively:
$$\mathscr{T} \vdash (k=m \wedge l<n) \Rightarrow P(k, l). \tag{6b}$$
By virtue of the metatheorem of deduction, relations (6a) and (6b) can be reformulated as:
$$\begin{align}
\mathscr{T}, k<m \wedge l \in \mathbb{N} &\vdash P(k, l) \tag{6a'}\\
\mathscr{T}, k=m \wedge l<n &\vdash P(k, l). \tag{6b'}
\end{align}$$
We clearly have:
$$\mathscr{T} \vdash (\forall k)(k<m \Rightarrow Q(k)), \tag{7}$$
whence by dequantification we infer in particular that:
$$\mathscr{T} \vdash k<m \Rightarrow Q(k). \tag{7'}$$
Since any theorem of a weaker theory remains a theorem for any stronger theory, it is clear that:
$$\mathscr{T}, k<m \wedge l \in \mathbb{N} \vdash k<m \Rightarrow Q(k). \tag{7''}$$
It is also obvious that:
$$\mathscr{T}, k<m \wedge l \in \mathbb{N} \vdash k<m, l \in \mathbb{N} \tag{7'''}$$ -- as a conjunction always implies any of its terms --
whence by modus ponens in combination with (7'') we obtain:
$$\mathscr{T}, k<m \wedge l \in \mathbb{N} \vdash Q(k),$$
which written out explicitly is precisely:
$$\mathscr{T}, k<m \wedge l \in \mathbb{N} \vdash (\forall n)(n \in \mathbb{N} \Rightarrow P(k, n)). \tag{8}$$
Particularising $n$ as $l$ we further obtain:
$$\mathscr{T}, k<m \wedge l \in \mathbb{N} \vdash l \in \mathbb{N} \Rightarrow P(k, l), \tag{8'}$$
and modus ponens in combination with (7’’’) yields precisely (6a’).
As to (6b’),  we first note that by definition:
$$\mathscr{T} \vdash (\forall l)(l<n \Rightarrow P(m, l)),$$
whence by dequantification we have:
$$\mathscr{T} \vdash l<n \Rightarrow P(m, l) \tag{9}.$$
The same implication is also deducible from the stronger theory:
$$\mathscr{T}, k=m \wedge l<n \vdash l<n \Rightarrow P(m, l), \tag{9’}$$
and we remark that by a token similar to that explained in the case of relation (7’’’) we have in this instance:
$$\mathscr{T}, k=m \wedge l<n \vdash k=m, l<n. \tag{7’’’’}$$
Applying modus ponens to (7’’’’) and (9’) we gather:
$$\mathscr{T}, k=m \wedge l<n \vdash P(m, l). \tag{9’’}$$
By virtue of one of the schemata which axiomatise the relation of equality, we have in particular:
$$\mathscr{T}, k=m \wedge l<n \vdash k=m \Rightarrow (P(k, l) \Leftrightarrow P(m, l)),$$
whence by modus ponens in combination with (7’’’’) it follows that:
$$\mathscr{T}, k=m \wedge l<n \vdash P(k, l) \Leftrightarrow P(m, l),$$
which furthermore entails:
$$\mathscr{T}, k=m \wedge l<n \vdash P(m, l) \Rightarrow P(k, l). \tag{9’’’}$$
A final application of modus ponens between (9'') and (9’’’) establishes (6b’) and concludes our argument.
A: If you assume that for any fixed $m$, $n$ you have
$$(\forall k)(\forall l)((k<m\vee(k=m\wedge l<n))\Rightarrow P(k,l))\Rightarrow P(m,n).$$
Now assume that $P(M,N)$ is false for some $(M,N)$, and take $(M,N)$ to be (among the values for which $P$ is false) the one for which, for every $M^{\prime}$, $N^{\prime}$ such that $P(M^{\prime},N^{\prime})$ is false, either $M < M^{\prime}$ or $M = M^{\prime}$ and $N \leq N^{\prime}$ (i.e. the lexicographically first such pair).
Now you can get an easy contradiction (assuming that $P(1,1)$ is true).
An alternate method if you don't like contradiction, assume $P(1,1)$ and then show that $P(m,1)$ is true for all $m$. Then for each $m$, use $P(m,1)$ to show that $P(m,n)$ is true for all $n$. This seems to be like your attempted proof, you do need to use induction twice here because you need to show that if the statement is true for $m=1$, then it is true for all $m$.
