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. Definitions. Informally, for a first-order formula of arithmetic formula_1 with one free variable, the induction principle for formula_2 expresses the validity of mathematical induction over formula_2, while the least number principle for formula_2 asserts that if formula_2 has a witness, it has a least one. For  a formula formula_6 in two free variables, the bounding principle for formula_7 states that, for a fixed "bound" formula_8, if for every formula_9 there is formula_10 such that formula_11, then we can find a bound on the formula_10's. Formally, the induction principle for formula_2 is the sentence: There is a similar strong induction principle for formula_2: The least number principle for formula_2 is the sentence: Finally, the bounding principle for formula_7 is the sentence: More commonly, we consider these principles not just for a single formula, but for a class of formulae in the arithmetical hierarchy. For example, formula_21  is the axiom schema consisting of formula_22 for every formula_23 formula formula_1 in one free variable. Nonstandard models. It may seem that the principles formula_22, formula_26, formula_27, formula_28 are trivial, and indeed, they hold for all formulae formula_2, formula_7 in the standard model of arithmetic formula_31. However, they become more relevant in nonstandard models. Recall that a nonstandard model of arithmetic has the form formula_32 for some linear order formula_33. In other words, it consists of an initial copy of formula_31, whose elements are called "finite" or "standard", followed by many copies of formula_35 arranged in the shape of formula_33 , whose elements are called "infinite" or "nonstandard". Now, considering the principles formula_22, formula_26, formula_27, formula_28 in a nonstandard model formula_41, we can see how they might fail. For example, the hypothesis of the induction principle formula_22 only ensures that formula_1 holds for all elements in the "standard" part of formula_41 - it may not hold for the nonstandard elements, who can't be reached by iterating the successor operation from zero. Similarly, the bounding principle formula_28 might fail if the bound formula_46 is nonstandard, as then the (infinite) collection of formula_47 could be cofinal in formula_41. Relations between the principles. The  following relations hold between the principles (over the weak base theory formula_49): Over formula_56, Slaman proved that formula_57. Reverse mathematics. The induction, bounding and least number principles are commonly used in reverse mathematics and second-order arithmetic. For example, formula_58 is part of the definition of the subsystem formula_59 of second-order arithmetic. Hence, formula_60, formula_61 and formula_62 are all theorems of formula_59. The subsystem formula_64 proves all the principles formula_22, formula_26, formula_27, formula_28 for arithmetical formula_2, formula_7. The infinite pigeonhole principle is known to be equivalent to formula_71 and formula_72 over formula_59. Induction, bounding and least number principles In