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?

*References as to What Double Induction Is:

To questions on this StackExchange:

To other sources:

  • 1
    $\begingroup$ @WillieWong: 'Double induction' is the use of mathematical induction to prove the truth of a logical predicate that depends on two variables instead of just one, hence the 'double' in its name. As I understand it, the technique can be implemented either by using a map from the bivariate predicate $\phi(x, y)$ in question to a univariate $\phi(z)$ as a shim allowing one to perform univariate mathematical induction over that or as recursive mathematical induction. I'm wondering what the axiom of induction might look like for a use of the latter implementation. $\endgroup$ Nov 11, 2015 at 21:22
  • $\begingroup$ Judging by the examples, it is not clear that "double induction" would have an axiom or axiom schema separate from an "axiom of induction" in number theory or from some principle of well-ordering/axiom of choice in set theory. $\endgroup$
    – hardmath
    Nov 13, 2015 at 23:04
  • $\begingroup$ @hardmath: Right, an 'axiom of double induction' would likely just be the axiom resulting from some kind of substitution of the univariate axiom of induction back into itself in one or more places. The reason I asked this question is because I can't seem to figure out what, exactly, that result would turn out to look like. $\endgroup$ Nov 13, 2015 at 23:13
  • $\begingroup$ One improvement to the Question would be to clarify whether the formal "axiom" is for number theory or set theory. It seems related to the topic of defining arithmetic functions by recursion. $\endgroup$
    – hardmath
    Nov 13, 2015 at 23:22
  • $\begingroup$ @hardmath: OK, then I'll go clarify that now. $\endgroup$ Nov 14, 2015 at 0:00

1 Answer 1


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$.

  • 1
    $\begingroup$ @RandomDSdevel 'closed form rule': basically the same thing as what you mean by 'axiom': one giant mathematical expression for the whole thing with no intervening english words such as in the preceding boxed paragraphs. $\endgroup$ Nov 28, 2015 at 3:58
  • 1
    $\begingroup$ @RandomDSdevel The approach on page 15 matches the first box of the section using $\prec_3$. The four parts of the antecedent correspond to the steps BC1, IS1, BC2, IS2; the hypotheses are written explicitly in my version but they wrote it out on several lines, that is IH1 -> IS1, IH0 -> BC2, IH0 & IH2 -> IS2. So it really is the same formula being applied. $\endgroup$ Nov 28, 2015 at 4:09
  • 1
    $\begingroup$ @RandomDSdevel No Iverson brackets here, jut trying to distinguish all the scopes of the expression without making it look too hairy. They are the same as parentheses. I use the convention that $\forall$ has a looser scope than connectives, so $\forall x,P\to Q$ means $\forall x,(P\to Q)$ and the brackets are needed when that's not the case. $\endgroup$ Dec 1, 2015 at 3:52
  • 1
    $\begingroup$ @RandomDSdevel I edited the question to adhere more strictly to the precedence rules. The precedence order is: $\land,\lor$; $\to$ (right assoc); $\forall,\exists$; $\implies$ (which is the same as $\to$ except for the precedence). $\forall$ binds everything of equal or higher precedence to the right of it, so $A\land\forall x,B\lor C$ means $A\land (\forall x,(B\lor C))$. $\endgroup$ Dec 1, 2015 at 4:09
  • 1
    $\begingroup$ @RandomDSdevel The extra variables $x,y$ and $n'$ are used so that they are not confused with different bound variables in adjacent scopes. The BC2 and IS2 parts each use an antecedent $\forall n,P(m,n)$, corresponding to IH0. This is because they are both part of the top level induction step, proving $[\forall n,P(m,n)]\to[\forall n,P(m+1,n)]$, so they both have access to the assumption $\forall n,P(m,n)$. $\endgroup$ Dec 5, 2015 at 5:47

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .