Induction, bounding and least number principles

Last updated

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.

Contents

Definitions

Informally, for a first-order formula of arithmetic with one free variable, the induction principle for expresses the validity of mathematical induction over , while the least number principle for asserts that if has a witness, it has a least one. For a formula in two free variables, the bounding principle for states that, for a fixed bound, if for every there is such that , then we can find a bound on the 's.

Formally, the induction principle for is the sentence: [1]

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

The least number 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. For example, is the axiom schema consisting of for every formula in one free variable.

Nonstandard models

It may seem that the principles , , , 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.

Now, considering the principles , , , in a nonstandard model , we can see how they might fail. For example, the hypothesis of the induction principle only ensures that 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 might fail if the bound is nonstandard, as then the (infinite) collection of could be cofinal in .

Relations between the principles

The relations between the induction, bounding and least number principles. Induction, bounding, least number principles.png
The relations between the induction, bounding and least number principles.

The following relations hold between the principles (over the weak base theory ): [1] [2]

Over , Slaman proved that . [3]

Reverse mathematics

The induction, bounding and least number principles are commonly used in reverse mathematics and second-order arithmetic. For example, is part of the definition of the subsystem of second-order arithmetic. Hence, , and are all theorems of . The subsystem proves all the principles , , , for arithmetical , . The infinite pigeonhole principle is known to be equivalent to and over . [4]

Related Research Articles

<span class="mw-page-title-main">Original proof of Gödel's completeness theorem</span>

The proof of Gödel's completeness theorem given by Kurt Gödel in his doctoral dissertation of 1929 is not easy to read today; it uses concepts and formalisms that are no longer used and terminology that is often obscure. The version given below attempts to represent all the steps in the proof and all the important ideas faithfully, while restating the proof in the modern language of mathematical logic. This outline should not be considered a rigorous proof of the theorem.

<span class="mw-page-title-main">Uncertainty principle</span> Foundational principle in quantum physics

In quantum mechanics, the uncertainty principle is any of a variety of mathematical inequalities asserting a fundamental limit to the accuracy with which the values for certain pairs of physical quantities of a particle, such as position, x, and momentum, p, can be predicted from initial conditions.

<span class="mw-page-title-main">Noether's theorem</span> Statement relating differentiable symmetries to conserved quantities

Noether's theorem or Noether's first theorem states that every differentiable symmetry of the action of a physical system with conservative forces has a corresponding conservation law. The theorem was proven by mathematician Emmy Noether in 1915 and published in 1918. The action of a physical system is the integral over time of a Lagrangian function, from which the system's behavior can be determined by the principle of least action. This theorem only applies to continuous and smooth symmetries over physical space.

<span class="mw-page-title-main">Arithmetical hierarchy</span> Hierarchy of complexity classes for formulas defining sets

In mathematical logic, the arithmetical hierarchy, arithmetic hierarchy or Kleene–Mostowski hierarchy classifies certain sets based on the complexity of formulas that define them. Any set that receives a classification is called arithmetical.

<span class="mw-page-title-main">Green's function</span> Impulse response of an inhomogeneous linear differential operator

In mathematics, a Green's function is the impulse response of an inhomogeneous linear differential operator defined on a domain with specified initial conditions or boundary conditions.

In computability theory Post's theorem, named after Emil Post, describes the connection between the arithmetical hierarchy and the Turing degrees.

<span class="mw-page-title-main">LSZ reduction formula</span> Connection between correlation functions and the S-matrix

In quantum field theory, the LSZ reduction formula is a method to calculate S-matrix elements from the time-ordered correlation functions of a quantum field theory. It is a step of the path that starts from the Lagrangian of some quantum field theory and leads to prediction of measurable quantities. It is named after the three German physicists Harry Lehmann, Kurt Symanzik and Wolfhart Zimmermann.

Independence-friendly logic is an extension of classical first-order logic (FOL) by means of slashed quantifiers of the form and , where is a finite set of variables. The intended reading of is "there is a which is functionally independent from the variables in ". IF logic allows one to express more general patterns of dependence between variables than those which are implicit in first-order logic. This greater level of generality leads to an actual increase in expressive power; the set of IF sentences can characterize the same classes of structures as existential second-order logic.

In set theory, -induction, also called epsilon-induction or set-induction, is a principle that can be used to prove that all sets satisfy a given property. Considered as an axiomatic principle, it is called the axiom schema of set induction.

In complexity theory, the Karp–Lipton theorem states that if the Boolean satisfiability problem (SAT) can be solved by Boolean circuits with a polynomial number of logic gates, then

In mathematical logic, second-order arithmetic is a collection of axiomatic systems that formalize the natural numbers and their subsets. It is an alternative to axiomatic set theory as a foundation for much, but not all, of mathematics.

In logic a branching quantifier, also called a Henkin quantifier, finite partially ordered quantifier or even nonlinear quantifier, is a partial ordering

In the mathematical discipline of set theory, there are many ways of describing specific countable ordinals. The smallest ones can be usefully and non-circularly expressed in terms of their Cantor normal forms. Beyond that, many ordinals of relevance to proof theory still have computable ordinal notations. However, it is not possible to decide effectively whether a given putative ordinal notation is a notation or not ; various more-concrete ways of defining ordinals that definitely have notations are available.

Constructive set theory is an approach to mathematical constructivism following the program of axiomatic set theory. The same first-order language with "" and "" of classical set theory is usually used, so this is not to be confused with a constructive types approach. On the other hand, some constructive theories are indeed motivated by their interpretability in type theories.

In constructive mathematics, Church's thesis is an axiom stating that all total functions are computable.

In proof theory, ordinal analysis assigns ordinals to mathematical theories as a measure of their strength. If theories have the same proof-theoretic ordinal they are often equiconsistent, and if one theory has a larger proof-theoretic ordinal than another it can often prove the consistency of the second theory.

In mathematical logic and set theory, an ordinal collapsing function is a technique for defining certain recursive large countable ordinals, whose principle is to give names to certain ordinals much larger than the one being defined, perhaps even large cardinals, and then "collapse" them down to a system of notations for the sought-after ordinal. For this reason, ordinal collapsing functions are described as an impredicative manner of naming ordinals.

In mathematics, the spectral theory of ordinary differential equations is the part of spectral theory concerned with the determination of the spectrum and eigenfunction expansion associated with a linear ordinary differential equation. In his dissertation Hermann Weyl generalized the classical Sturm–Liouville theory on a finite closed interval to second order differential operators with singularities at the endpoints of the interval, possibly semi-infinite or infinite. Unlike the classical case, the spectrum may no longer consist of just a countable set of eigenvalues, but may also contain a continuous part. In this case the eigenfunction expansion involves an integral over the continuous part with respect to a spectral measure, given by the Titchmarsh–Kodaira formula. The theory was put in its final simplified form for singular differential equations of even degree by Kodaira and others, using von Neumann's spectral theorem. It has had important applications in quantum mechanics, operator theory and harmonic analysis on semisimple Lie groups.

Lagrangian field theory is a formalism in classical field theory. It is the field-theoretic analogue of Lagrangian mechanics. Lagrangian mechanics is used to analyze the motion of a system of discrete particles each with a finite number of degrees of freedom. Lagrangian field theory applies to continua and fields, which have an infinite number of degrees of freedom.

In set theory and logic, Buchholz's ID hierarchy is a hierarchy of subsystems of first-order arithmetic. The systems/theories are referred to as "the formal theories of ν-times iterated inductive definitions". IDν extends PA by ν iterated least fixed points of monotone operators.

References

  1. 1 2 3 4 5 Hájek, Petr; Pudlák, Pavel (2016). Metamathematics of First-Order Arithmetic. Association for Symbolic Logic c/- Cambridge University Press. ISBN   978-1-107-16841-1. OCLC   1062334376.
  2. Paris, J.B.; Kirby, L.A.S. (1978), "Σn-Collection Schemas in Arithmetic", Logic Colloquium '77, Elsevier, pp. 199–209, doi:10.1016/s0049-237x(08)72003-2, ISBN   978-0-444-85178-9 , retrieved 2021-04-14
  3. Slaman, Theodore A. (2004-08-01). "-bounding and -induction". Proceedings of the American Mathematical Society . 132 (8): 2449. doi: 10.1090/s0002-9939-04-07294-6 . ISSN   0002-9939.
  4. Hirst, Jeffry (August 1987). Combinatorics in Subsystems of Second Order Arithmetic (PhD). Pennsylvania State University.