Induction, bounding and least number principles

In first-order arithmetic, the induction principles, bounding principles, and least number principles are three related families of first-order principles, which may or may not hold in nonstandard models of arithmetic.

These principles are often used in reverse mathematics to calibrate the axiomatic strength of theorems.

Informally, for a first-order formula of arithmetic

with one free variable, the induction principle for

expresses the validity of mathematical induction over

in two free variables, the bounding principle for

states that, for a fixed bound

Formally, the induction principle for

is the sentence:[1] There is a similar strong induction principle for

is the sentence:[1] Finally, the bounding principle for

is the sentence:[1] More commonly, we consider these principles not just for a single formula, but for a class of formulae in the arithmetical hierarchy.

is the axiom schema consisting of

are trivial, and indeed, they hold for all formulae

in the standard model of arithmetic

However, they become more relevant in nonstandard models.

Recall that a nonstandard model of arithmetic has the form

for some linear order

In other words, it consists of an initial copy of

, whose elements are called finite or standard, followed by many copies of

arranged in the shape of

, whose elements are called infinite or nonstandard.

For example, the hypothesis of the induction principle

holds for all elements in the standard part of

- it may not hold for the nonstandard elements, who can't be reached by iterating the successor operation from zero.

Similarly, the bounding principle

is nonstandard, as then the (infinite) collection of

The following relations hold between the principles (over the weak base theory

[3] The induction, bounding and least number principles are commonly used in reverse mathematics and second-order arithmetic.

is part of the definition of the subsystem

The infinite pigeonhole principle is known to be equivalent to