Reverse mathematics
Encyclopedia
Reverse mathematics is a program in mathematical logic
that seeks to determine which axioms are required to prove theorems of mathematics. Its defining method can briefly be described as "going backwards from the theorem
s to the axiom
s", in contrast to the ordinary mathematical practice of deriving theorems from axioms. The reverse mathematics program was foreshadowed by results in set theory such as the classical theorem that the axiom of choice and Zorn's lemma
are equivalent over ZF set theory. The goal of reverse mathematics, however, is to study ordinary theorems of mathematics rather than possible axioms for set theory.
Reverse mathematics is usually carried out using subsystems of second-order arithmetic
, where many of its definitions and methods are inspired by previous work in constructive analysis and proof theory
. The use of second-order arithmetic also allows many techniques from recursion theory
to be employed; many results in reverse mathematics have corresponding results in computable analysis
.
The program was founded by . A standard reference for the subject is .
s has a supremum
” it is necessary to use a base system which can speak of real numbers and sequences of real numbers.
For each theorem that can be stated in the base system but is not provable in the base system, the goal is to determine the particular axiom system (stronger than the base system) that is necessary to prove that theorem. To show that a system S is required to prove a theorem T, two proofs are required. The first proof shows T is provable from S; this is an ordinary mathematical proof along with a justification that it can be carried out in the system S. The second proof, known as a reversal, shows that T itself implies S; this proof is carried out in the base system. The reversal establishes that no axiom system S′ that extends the base system can be weaker than S while still proving T.
. The body of research in reverse mathematics has established that weak subsystems of second-order arithmetic suffice to formalize almost all undergraduate-level mathematics. In second-order arithmetic, all objects must be represented as either natural number
s or sets of natural numbers. For example, in order to prove theorems about real numbers, the real numbers must be represented as Cauchy sequence
s of rational number
s, each of which can be represented as a set of natural numbers.
The axiom systems most often considered in reverse mathematics are defined using axiom schemes called comprehension schemes. Such a scheme states that any set of natural numbers definable by a formula of a given complexity exists. In this context, the complexity of formulas is measured using the arithmetical hierarchy
and analytical hierarchy
.
The reason that reverse mathematics is not carried out using set theory as a base system is that the language of set theory is too expressive. Extremely complex sets of natural numbers can be defined by simple formulas in the language of set theory (which can quantify over arbitrary sets). In the context of second-order arithmetic, results such as Post's theorem
establish a close link between the complexity of a formula and the (non)computability of the set it defines.
Another effect of using second-order arithmetic is the need to restrict general mathematical theorems to forms that can be expressed within arithmetic. For example, second-order arithmetic can express the principle "Every countable vector space
has a basis" but it cannot express the principle "Every vector space has a basis". In practical terms, this means that theorems of algebra and combinatorics are restricted to countable structures, while theorems of analysis and topology are restricted to separable spaces. Many principles that imply the axiom of choice in their general form (such as "Every vector space has a basis") become provable in weak subsystems of second-order arithmetic when they are restricted. For example, "every field has an algebraic closure" is not provable in ZF set theory, but the restricted form "every countable field has an algebraic closure" is provable in RCA0, the weakest system typically employed in reverse mathematics.
rings
, groups
, and fields
, as well as points in effective Polish space
s, can be represented as sets of natural numbers, and modulo this representation can be studied in second order arithmetic.
Reverse mathematics makes use of several subsystems of second order arithmetic. A typical reverse mathematics theorem shows that a particular mathematical theorem T is equivalent to a particular subsystem S of second order arithmetic over a weaker subsystem B. This weaker system B is known as the base system for the result; in order for the reverse mathematics result to have
meaning, this system must not itself be able to prove the mathematical theorem T.
describes five particular subsystems of second order arithmetic, which he calls the Big Five, that occur frequently in reverse mathematics. In order of increasing strength, these systems are named by the initialisms RCA0, WKL0, ACA0, ATR0, and
Π11-CA0.
The following table summarizes the "big five" systems
The subscript 0 in these names means that the induction scheme has been restricted from the full second-order induction scheme . For example, ACA0 includes the induction axiom (0∈X ∧ ∀n(n∈X → n+1∈X)) → ∀n n∈X. This together with the full comprehension axiom of second order arithmetic implies the full second-order induction scheme given by the universal closure of (φ(0) ∧ ∀n(φ(n) → φ(n+1))) → ∀n φ(n) for any second order formula φ. However ACA0 does not have the full comprehension axiom, and the subscript 0 is a reminder that it does not have the full second-order induction scheme either. This restriction is important: systems with restricted induction have significantly lower proof-theoretical ordinals than systems with the full second-order induction scheme.
, induction for Σ formulas, and comprehension for Δ formulas.
The subsystem RCA0 is the one most commonly used as a base system for reverse mathematics. The initials "RCA" stand for "recursive comprehension axiom", where "recursive" means "computable", as in recursive function
. This name is used because RCA0 corresponds informally to "computable mathematics". In particular, any set of natural numbers that can be proven to exist in RCA0 is computable, and thus any theorem which implies that noncomputable sets exist is not provable in RCA0. To this extent, RCA0 is a constructive system, although it does not meet the requirements of the program of constructivism
because it is a theory in classical logic including the excluded middle.
Despite its seeming weakness (of not proving any noncomputable sets exist), RCA0 is sufficient to prove a number of classical theorems which, therefore, require only minimal logical strength. These theorems are, in a sense, below the reach of the reverse mathematics enterprise because they are already provable in the base system. The classical theorems provable in RCA0 include:
The first-order part of RCA0 (the theorems of the system that do not involve any set variables) is the set of theorems of first-order Peano arithmetic with induction limited to Σ01 formulas. It is provably consistent, as is RCA0, in full first-order Peano arithmetic.
, namely the statement that every infinite subtree of the full binary tree (the tree of all finite sequences of 0's and 1's) has an infinite path. This proposition, which is known as weak König's lemma, is easy to state in the language of second-order arithmetic. WKL0 can also be defined as the principle of Σ01 separation (given two Σ01 formulas of a free variable n which are exclusive, there is a class containing all n satisfying the one and no n satisfying the other).
The following remark on terminology is in order. The term “weak König's lemma” refers to the sentence which says that any infinite subtree of the binary tree has an infinite path. When this axiom is added to RCA0, the resulting subsystem is called WKL0. A similar distinction between particular axioms, on the one hand, and subsystems including the basic axioms and induction, on the other hand, is made for the stronger subsystems described below.
In a sense, weak König's lemma is a form of the axiom of choice (although, as stated, it can be proven in classical Zermelo–Fraenkel set theory without the axiom of choice). It is not constructively valid in some senses of the word constructive.
To show that WKL0 is actually stronger than (not provable in) RCA0, it is sufficient to exhibit a theorem of WKL0 which implies that noncomputable sets exist. This is not difficult; WKL0 implies the existence of separating sets for effectively inseparable recursively enumerable sets.
It turns out that RCA0 and WKL0 have the same first-order part, meaning that they prove the same first-order sentences. WKL0 can prove a good number of classical mathematical results which do not follow from RCA0, however. These results are not expressible as first order statements but can be expressed as second-order statements.
The following results are equivalent to weak König's lemma and thus to WKL0 over RCA0:
The first-order part of ACA0 is exactly first-order Peano arithmetic; ACA0 is a conservative extension of first-order Peano arithmetic. The two systems are provably (in a weak system) equiconsistent. ACA0 can be thought of as a framework of predicative mathematics, although there are predicatively provable theorems that are not provable in ACA0. Most of the fundamental results about the natural numbers, and many other mathematical theorems, can be proven in this system.
One way of seeing that ACA0 is stronger than WKL0 is to exhibit a model of WKL0 that doesn't contain all arithmetical sets. In fact, it is possible to build a model of WKL0 consisting entirely of low sets
using the low basis theorem
, since low sets relative to low sets are low.
The following assertions are equivalent to ACA0
over RCA0:
, the supremum of that of predicative systems.
ATR0 proves the consistency of ACA0, and thus by Gödel's theorem
it is strictly stronger.
The following assertions are equivalent to
ATR0 over RCA0:
In a sense, Π11-CA0 comprehension is to arithmetical transfinite recursion (Σ11 separation) as ACA0 is to weak König's lemma (Σ01 separation). It is equivalent to several statements of descriptive set theory whose proofs make use of strongly impredicative arguments; this equivalence shows that these impredicative arguments cannot be removed.
The following theorems are equivalent to Π11-CA0 over RCA0:
A β model is an ω model that is equivalent to the standard ω-model for Π and Σ sentences (with parameters).
Non-ω models are also useful, especially in the proofs of conservation theorems.
Mathematical logic
Mathematical logic is a subfield of mathematics with close connections to foundations of mathematics, theoretical computer science and philosophical logic. The field includes both the mathematical study of logic and the applications of formal logic to other areas of mathematics...
that seeks to determine which axioms are required to prove theorems of mathematics. Its defining method can briefly be described as "going backwards from the theorem
Theorem
In mathematics, a theorem is a statement that has been proven on the basis of previously established statements, such as other theorems, and previously accepted statements, such as axioms...
s to the axiom
Axiom
In traditional logic, an axiom or postulate is a proposition that is not proven or demonstrated but considered either to be self-evident or to define and delimit the realm of analysis. In other words, an axiom is a logical statement that is assumed to be true...
s", in contrast to the ordinary mathematical practice of deriving theorems from axioms. The reverse mathematics program was foreshadowed by results in set theory such as the classical theorem that the axiom of choice and Zorn's lemma
Zorn's lemma
Zorn's lemma, also known as the Kuratowski–Zorn lemma, is a proposition of set theory that states:Suppose a partially ordered set P has the property that every chain has an upper bound in P...
are equivalent over ZF set theory. The goal of reverse mathematics, however, is to study ordinary theorems of mathematics rather than possible axioms for set theory.
Reverse mathematics is usually carried out using subsystems of second-order arithmetic
Second-order arithmetic
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. It was introduced by David Hilbert and Paul Bernays in their...
, where many of its definitions and methods are inspired by previous work in constructive analysis and proof theory
Proof theory
Proof theory is a branch of mathematical logic that represents proofs as formal mathematical objects, facilitating their analysis by mathematical techniques. Proofs are typically presented as inductively-defined data structures such as plain lists, boxed lists, or trees, which are constructed...
. The use of second-order arithmetic also allows many techniques from recursion theory
Recursion theory
Computability theory, also called recursion theory, is a branch of mathematical logic that originated in the 1930s with the study of computable functions and Turing degrees. The field has grown to include the study of generalized computability and definability...
to be employed; many results in reverse mathematics have corresponding results in computable analysis
Computable analysis
In mathematics, computable analysis is the study of which parts of real analysis and functional analysis can be carried out in a computable manner. It is closely related to constructive analysis.- Basic results :...
.
The program was founded by . A standard reference for the subject is .
General principles
In reverse mathematics, one starts with a framework language and a base theory—a core axiom system—that is too weak to prove most of the theorems one might be interested in, but still powerful enough to develop the definitions necessary to state these theorems. For example, to study the theorem “Every bounded sequence of real numberReal number
In mathematics, a real number is a value that represents a quantity along a continuum, such as -5 , 4/3 , 8.6 , √2 and π...
s has a supremum
Supremum
In mathematics, given a subset S of a totally or partially ordered set T, the supremum of S, if it exists, is the least element of T that is greater than or equal to every element of S. Consequently, the supremum is also referred to as the least upper bound . If the supremum exists, it is unique...
” it is necessary to use a base system which can speak of real numbers and sequences of real numbers.
For each theorem that can be stated in the base system but is not provable in the base system, the goal is to determine the particular axiom system (stronger than the base system) that is necessary to prove that theorem. To show that a system S is required to prove a theorem T, two proofs are required. The first proof shows T is provable from S; this is an ordinary mathematical proof along with a justification that it can be carried out in the system S. The second proof, known as a reversal, shows that T itself implies S; this proof is carried out in the base system. The reversal establishes that no axiom system S′ that extends the base system can be weaker than S while still proving T.
Use of second-order arithmetic
Most reverse mathematics research focuses on subsystems of second-order arithmeticSecond-order arithmetic
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. It was introduced by David Hilbert and Paul Bernays in their...
. The body of research in reverse mathematics has established that weak subsystems of second-order arithmetic suffice to formalize almost all undergraduate-level mathematics. In second-order arithmetic, all objects must be represented as either natural number
Natural number
In mathematics, the natural numbers are the ordinary whole numbers used for counting and ordering . These purposes are related to the linguistic notions of cardinal and ordinal numbers, respectively...
s or sets of natural numbers. For example, in order to prove theorems about real numbers, the real numbers must be represented as Cauchy sequence
Cauchy sequence
In mathematics, a Cauchy sequence , named after Augustin-Louis Cauchy, is a sequence whose elements become arbitrarily close to each other as the sequence progresses...
s of rational number
Rational number
In mathematics, a rational number is any number that can be expressed as the quotient or fraction a/b of two integers, with the denominator b not equal to zero. Since b may be equal to 1, every integer is a rational number...
s, each of which can be represented as a set of natural numbers.
The axiom systems most often considered in reverse mathematics are defined using axiom schemes called comprehension schemes. Such a scheme states that any set of natural numbers definable by a formula of a given complexity exists. In this context, the complexity of formulas is measured using the arithmetical hierarchy
Arithmetical hierarchy
In mathematical logic, the arithmetical hierarchy, arithmetic hierarchy or Kleene-Mostowski hierarchy classifies certain sets based on the complexity of formulas that define them...
and analytical hierarchy
Analytical hierarchy
In mathematical logic and descriptive set theory, the analytical hierarchy is a higher type analogue of the arithmetical hierarchy. It thus continues the classification of sets by the formulas that define them.-The analytical hierarchy of formulas:...
.
The reason that reverse mathematics is not carried out using set theory as a base system is that the language of set theory is too expressive. Extremely complex sets of natural numbers can be defined by simple formulas in the language of set theory (which can quantify over arbitrary sets). In the context of second-order arithmetic, results such as Post's theorem
Post's theorem
In computability theory Post's theorem, named after Emil Post, describes the connection between the arithmetical hierarchy and the Turing degrees.- Background :The statement of Post's theorem uses several concepts relating to definability and recursion theory...
establish a close link between the complexity of a formula and the (non)computability of the set it defines.
Another effect of using second-order arithmetic is the need to restrict general mathematical theorems to forms that can be expressed within arithmetic. For example, second-order arithmetic can express the principle "Every countable vector space
Vector space
A vector space is a mathematical structure formed by a collection of vectors: objects that may be added together and multiplied by numbers, called scalars in this context. Scalars are often taken to be real numbers, but one may also consider vector spaces with scalar multiplication by complex...
has a basis" but it cannot express the principle "Every vector space has a basis". In practical terms, this means that theorems of algebra and combinatorics are restricted to countable structures, while theorems of analysis and topology are restricted to separable spaces. Many principles that imply the axiom of choice in their general form (such as "Every vector space has a basis") become provable in weak subsystems of second-order arithmetic when they are restricted. For example, "every field has an algebraic closure" is not provable in ZF set theory, but the restricted form "every countable field has an algebraic closure" is provable in RCA0, the weakest system typically employed in reverse mathematics.
The big five subsystems of second order arithmetic
Second order arithmetic is a formal theory of the natural numbers and sets of natural numbers. Many mathematical objects, such as countableCountable set
In mathematics, a countable set is a set with the same cardinality as some subset of the set of natural numbers. A set that is not countable is called uncountable. The term was originated by Georg Cantor...
rings
Ring (mathematics)
In mathematics, a ring is an algebraic structure consisting of a set together with two binary operations usually called addition and multiplication, where the set is an abelian group under addition and a semigroup under multiplication such that multiplication distributes over addition...
, groups
Group (mathematics)
In mathematics, a group is an algebraic structure consisting of a set together with an operation that combines any two of its elements to form a third element. To qualify as a group, the set and the operation must satisfy a few conditions called group axioms, namely closure, associativity, identity...
, and fields
Field (mathematics)
In abstract algebra, a field is a commutative ring whose nonzero elements form a group under multiplication. As such it is an algebraic structure with notions of addition, subtraction, multiplication, and division, satisfying certain axioms...
, as well as points in effective Polish space
Effective Polish space
In mathematical logic, an effective Polish space is a complete separable metric space that has a computable presentation. Such spaces are studied in effective descriptive set theory and in constructive analysis.- Definition :...
s, can be represented as sets of natural numbers, and modulo this representation can be studied in second order arithmetic.
Reverse mathematics makes use of several subsystems of second order arithmetic. A typical reverse mathematics theorem shows that a particular mathematical theorem T is equivalent to a particular subsystem S of second order arithmetic over a weaker subsystem B. This weaker system B is known as the base system for the result; in order for the reverse mathematics result to have
meaning, this system must not itself be able to prove the mathematical theorem T.
describes five particular subsystems of second order arithmetic, which he calls the Big Five, that occur frequently in reverse mathematics. In order of increasing strength, these systems are named by the initialisms RCA0, WKL0, ACA0, ATR0, and
Π11-CA0.
The following table summarizes the "big five" systems
| Subsystem | Stands for | Ordinal | Corresponds roughly to | Comments |
|---|---|---|---|---|
| RCA0 | Recursive comprehension axiom | ωω | Constructive mathematics (Bishop) | The base system for reverse mathematics |
| WKL0 | Weak König's lemma | ωω | Finitistic reductionism (Hilbert) | Conservative over PRA Primitive recursive arithmetic Primitive recursive arithmetic, or PRA, is a quantifier-free formalization of the natural numbers. It was first proposed by Skolem as a formalization of his finitist conception of the foundations of arithmetic, and it is widely agreed that all reasoning of PRA is finitist... for sentences. Conservative over RCA0 for sentences. |
| ACA0 | Arithmetical comprehension axiom | ε0 | Predicativism (Weyl, Feferman) | Conservative over Peano arithmetic for arithmetical sentences |
| ATR0 | Arithmetical transfinite recursion | Γ0 Feferman–Schütte ordinal In mathematics, the Feferman–Schütte ordinal Γ0 is a large countable ordinal.It is the proof theoretic ordinal of several mathematical theories, such as arithmetical transfinite recursion.It is named after Solomon Feferman and Kurt Schütte.... |
Predicative reductionism (Friedman, Simpson) | Conservative over Feferman's system IR for sentences |
| Π-CA0 | Π comprehension axiom | Ψ0(Ωω) Psi0(Omega omega) In mathematics, Ψ0 is a large countable ordinal that is used to measure the proof-theoretic strength of some mathematical systems. In particular, it is the proof theoretic ordinal of the subsystem \Pi_1^1-CA0 of second-order arithmetic; this is one of the "big five" subsystems studied in reverse... |
Impredicativism |
The subscript 0 in these names means that the induction scheme has been restricted from the full second-order induction scheme . For example, ACA0 includes the induction axiom (0∈X ∧ ∀n(n∈X → n+1∈X)) → ∀n n∈X. This together with the full comprehension axiom of second order arithmetic implies the full second-order induction scheme given by the universal closure of (φ(0) ∧ ∀n(φ(n) → φ(n+1))) → ∀n φ(n) for any second order formula φ. However ACA0 does not have the full comprehension axiom, and the subscript 0 is a reminder that it does not have the full second-order induction scheme either. This restriction is important: systems with restricted induction have significantly lower proof-theoretical ordinals than systems with the full second-order induction scheme.
The base system RCA0
RCA0 is the fragment of second-order arithmetic whose axioms are the axioms of Robinson arithmeticRobinson arithmetic
In mathematics, Robinson arithmetic, or Q, is a finitely axiomatized fragment of Peano arithmetic , first set out in R. M. Robinson . Q is essentially PA without the axiom schema of induction. Since Q is weaker than PA, it is incomplete...
, induction for Σ formulas, and comprehension for Δ formulas.
The subsystem RCA0 is the one most commonly used as a base system for reverse mathematics. The initials "RCA" stand for "recursive comprehension axiom", where "recursive" means "computable", as in recursive function
Computable function
Computable functions are the basic objects of study in computability theory. Computable functions are the formalized analogue of the intuitive notion of algorithm. They are used to discuss computability without referring to any concrete model of computation such as Turing machines or register...
. This name is used because RCA0 corresponds informally to "computable mathematics". In particular, any set of natural numbers that can be proven to exist in RCA0 is computable, and thus any theorem which implies that noncomputable sets exist is not provable in RCA0. To this extent, RCA0 is a constructive system, although it does not meet the requirements of the program of constructivism
Constructivism (mathematics)
In the philosophy of mathematics, constructivism asserts that it is necessary to find a mathematical object to prove that it exists. When one assumes that an object does not exist and derives a contradiction from that assumption, one still has not found the object and therefore not proved its...
because it is a theory in classical logic including the excluded middle.
Despite its seeming weakness (of not proving any noncomputable sets exist), RCA0 is sufficient to prove a number of classical theorems which, therefore, require only minimal logical strength. These theorems are, in a sense, below the reach of the reverse mathematics enterprise because they are already provable in the base system. The classical theorems provable in RCA0 include:
- Basic properties of the natural numbers, integers, and rational numbers (for example, that the latter form an ordered fieldOrdered fieldIn mathematics, an ordered field is a field together with a total ordering of its elements that is compatible with the field operations. Historically, the axiomatization of an ordered field was abstracted gradually from the real numbers, by mathematicians including David Hilbert, Otto Hölder and...
). - Basic properties of the real numbers (the real numbers are an ArchimedeanArchimedean propertyIn abstract algebra and analysis, the Archimedean property, named after the ancient Greek mathematician Archimedes of Syracuse, is a property held by some ordered or normed groups, fields, and other algebraic structures. Roughly speaking, it is the property of having no infinitely large or...
ordered field; any nested sequence of closed intervals whose lengths tend to zero has a single point in its intersection; the real numbers are not countable). - The Baire category theoremBaire category theoremThe Baire category theorem is an important tool in general topology and functional analysis. The theorem has two forms, each of which gives sufficient conditions for a topological space to be a Baire space....
for a complete separable metric spaceMetric spaceIn mathematics, a metric space is a set where a notion of distance between elements of the set is defined.The metric space which most closely corresponds to our intuitive understanding of space is the 3-dimensional Euclidean space...
(the separability condition is necessary to even state the theorem in the language of second-order arithmetic). - The intermediate value theoremIntermediate value theoremIn mathematical analysis, the intermediate value theorem states that for each value between the least upper bound and greatest lower bound of the image of a continuous function there is at least one point in its domain that the function maps to that value....
on continuous real functions. - The Banach–Steinhaus theorem for a sequence of continuous linear operators on separable Banach spaces.
- A weak version of Gödel's completeness theoremGödel's completeness theoremGödel's completeness theorem is a fundamental theorem in mathematical logic that establishes a correspondence between semantic truth and syntactic provability in first-order logic. It was first proved by Kurt Gödel in 1929....
(for a set of sentences, in a countable language, that is already closed under consequence). - The existence of an algebraic closureAlgebraic closureIn mathematics, particularly abstract algebra, an algebraic closure of a field K is an algebraic extension of K that is algebraically closed. It is one of many closures in mathematics....
for a countable field (but not its uniqueness). - The existence and uniqueness of the real closureReal closed fieldIn mathematics, a real closed field is a field F that has the same first-order properties as the field of real numbers. Some examples are the field of real numbers, the field of real algebraic numbers, and the field of hyperreal numbers.-Definitions:...
of a countable ordered field.
The first-order part of RCA0 (the theorems of the system that do not involve any set variables) is the set of theorems of first-order Peano arithmetic with induction limited to Σ01 formulas. It is provably consistent, as is RCA0, in full first-order Peano arithmetic.
Weak König's lemma WKL0
The subsystem WKL0 consists of RCA0 plus a weak form of König's lemmaKönig's lemma
König's lemma or König's infinity lemma is a theorem in graph theory due to Dénes Kőnig . It gives a sufficient condition for an infinite graph to have an infinitely long path. The computability aspects of this theorem have been thoroughly investigated by researchers in mathematical logic,...
, namely the statement that every infinite subtree of the full binary tree (the tree of all finite sequences of 0's and 1's) has an infinite path. This proposition, which is known as weak König's lemma, is easy to state in the language of second-order arithmetic. WKL0 can also be defined as the principle of Σ01 separation (given two Σ01 formulas of a free variable n which are exclusive, there is a class containing all n satisfying the one and no n satisfying the other).
The following remark on terminology is in order. The term “weak König's lemma” refers to the sentence which says that any infinite subtree of the binary tree has an infinite path. When this axiom is added to RCA0, the resulting subsystem is called WKL0. A similar distinction between particular axioms, on the one hand, and subsystems including the basic axioms and induction, on the other hand, is made for the stronger subsystems described below.
In a sense, weak König's lemma is a form of the axiom of choice (although, as stated, it can be proven in classical Zermelo–Fraenkel set theory without the axiom of choice). It is not constructively valid in some senses of the word constructive.
To show that WKL0 is actually stronger than (not provable in) RCA0, it is sufficient to exhibit a theorem of WKL0 which implies that noncomputable sets exist. This is not difficult; WKL0 implies the existence of separating sets for effectively inseparable recursively enumerable sets.
It turns out that RCA0 and WKL0 have the same first-order part, meaning that they prove the same first-order sentences. WKL0 can prove a good number of classical mathematical results which do not follow from RCA0, however. These results are not expressible as first order statements but can be expressed as second-order statements.
The following results are equivalent to weak König's lemma and thus to WKL0 over RCA0:
- The Heine–Borel theoremHeine–Borel theoremIn the topology of metric spaces the Heine–Borel theorem, named after Eduard Heine and Émile Borel, states:For a subset S of Euclidean space Rn, the following two statements are equivalent:*S is closed and bounded...
for the closed unit real interval, in the following sense: every covering by a sequence of open intervals has a finite subcovering. - The Heine–Borel theorem for complete totally bounded separable metric spaces (where covering is by a sequence of open balls).
- A continuous real function on the closed unit interval (or on any compact separable metric space, as above) is bounded (or: bounded and reaches its bounds).
- A continuous real function on the closed unit interval can be uniformly approximated by polynomials (with rational coefficients).
- A continuous real function on the closed unit interval is uniformly continuous.
- A continuous real function on the closed unit interval is RiemannRiemann integralIn the branch of mathematics known as real analysis, the Riemann integral, created by Bernhard Riemann, was the first rigorous definition of the integral of a function on an interval. The Riemann integral is unsuitable for many theoretical purposes...
integrable. - The Brouwer fixed point theoremBrouwer fixed point theoremBrouwer's fixed-point theorem is a fixed-point theorem in topology, named after Luitzen Brouwer. It states that for any continuous function f with certain properties there is a point x0 such that f = x0. The simplest form of Brouwer's theorem is for continuous functions f from a disk D to...
(for continuous functions on a finite product of copies of the closed unit interval). - The separable Hahn–Banach theoremHahn–Banach theoremIn mathematics, the Hahn–Banach theorem is a central tool in functional analysis. It allows the extension of bounded linear functionals defined on a subspace of some vector space to the whole space, and it also shows that there are "enough" continuous linear functionals defined on every normed...
in the form: a bounded linear form on a subspace of a separable Banach space extends to a bounded linear form on the whole space. - The Jordan curve theoremJordan curve theoremIn topology, a Jordan curve is a non-self-intersecting continuous loop in the plane, and another name for a Jordan curve is a "simple closed curve"...
- Gödel's completeness theorem (for a countable language).
- Every countable commutative ringCommutative ringIn ring theory, a branch of abstract algebra, a commutative ring is a ring in which the multiplication operation is commutative. The study of commutative rings is called commutative algebra....
has a prime idealPrime idealIn algebra , a prime ideal is a subset of a ring which shares many important properties of a prime number in the ring of integers...
. - Every countable formally real field is orderable.
- Uniqueness of algebraic closure (for a countable field).
Arithmetical comprehension ACA0
ACA0 is RCA0 plus the comprehension scheme for arithmetical formulas (which is sometimes called the "arithmetical comprehension axiom"). That is, ACA0 allows us to form the set of natural numbers satisfying an arbitrary arithmetical formula (one with no bound set variables, although possibly containing set parameters). Actually, it suffices to add to RCA0 the comprehension scheme for Σ1 formulas in order to obtain full arithmetical comprehension.The first-order part of ACA0 is exactly first-order Peano arithmetic; ACA0 is a conservative extension of first-order Peano arithmetic. The two systems are provably (in a weak system) equiconsistent. ACA0 can be thought of as a framework of predicative mathematics, although there are predicatively provable theorems that are not provable in ACA0. Most of the fundamental results about the natural numbers, and many other mathematical theorems, can be proven in this system.
One way of seeing that ACA0 is stronger than WKL0 is to exhibit a model of WKL0 that doesn't contain all arithmetical sets. In fact, it is possible to build a model of WKL0 consisting entirely of low sets
Low (computability)
In computability theory, a Turing degree [X] is low if the Turing jump [X′] is 0′, which is the least possible degree in terms of Turing reducibility for the jump of a set. Since every set is computable from its jump, any low set is computable in 0′...
using the low basis theorem
Low basis theorem
The low basis theorem in computability theory states that every nonempty \Pi^0_1 class of 2^\omega contains a set of low degree. It was first proved by Carl Jockusch and Robert I. Soare in 1972.- References :...
, since low sets relative to low sets are low.
The following assertions are equivalent to ACA0
over RCA0:
- The sequential completeness of the real numbers (every bounded increasing sequence of real numbers has a limit).
- The Bolzano–Weierstrass theoremBolzano–Weierstrass theoremIn real analysis, the Bolzano–Weierstrass theorem is a fundamental result about convergence in a finite-dimensional Euclidean space Rn. The theorem states thateach bounded sequence in Rn has a convergent subsequence...
. - Ascoli's theorem: every bounded equicontinuous sequence of real functions on the unit interval has a uniformly convergent subsequence.
- Every countable commutative ring has a maximal idealMaximal idealIn mathematics, more specifically in ring theory, a maximal ideal is an ideal which is maximal amongst all proper ideals. In other words, I is a maximal ideal of a ring R if I is an ideal of R, I ≠ R, and whenever J is another ideal containing I as a subset, then either J = I or J = R...
. - Every countable vector space over the rationals (or over any countable field) has a basis.
- Every countable field has a transcendence basis.
- König's lemma (for arbitrary finitely branching trees, as opposed to the weak version described above).
- Various theorems in combinatorics, such as certain forms of Ramsey's theorem.
Arithmetical Transfinite Recursion ATR0
The system ATR0 adds to ACA0 an axiom which states, informally, that any arithmetical functional (meaning any arithmetical formula with a free number variable n and a free class variable X, seen as the operator taking X to the set of n satisfying the formula) can be iterated transfinitely along any countable well ordering starting with any set. ATR0 is equivalent over ACA0 to the principle of Σ11 separation. ATR0 is impredicative, and has the proof-theoretic ordinal, the supremum of that of predicative systems.ATR0 proves the consistency of ACA0, and thus by Gödel's theorem
Gödel's incompleteness theorems
Gödel's incompleteness theorems are two theorems of mathematical logic that establish inherent limitations of all but the most trivial axiomatic systems capable of doing arithmetic. The theorems, proven by Kurt Gödel in 1931, are important both in mathematical logic and in the philosophy of...
it is strictly stronger.
The following assertions are equivalent to
ATR0 over RCA0:
- Any two countable well orderings are comparable. That is, they are isomorphic or one is isomorphic to a proper initial segment of the other.
- Ulm's theorem for countable reduced Abelian groups.
- The perfect set theoremPerfect set propertyIn descriptive set theory, a subset of a Polish space has the perfect set property if it is either countable or has a nonempty perfect subset...
, which states that every uncountable closed subset of a complete separable metric space contains a perfect closed set. - Lusin's separation theoremLusin's separation theoremIn descriptive set theory and mathematical logic, Lusin's separation theorem states that if A and B are disjoint analytic subsets of Polish space, then there is a Borel set C in the space such that A ⊆ C and B ∩ C = ∅ . It is named after Nicolas Lusin,...
(essentially Σ11 separation). - DeterminacyDeterminacyIn set theory, a branch of mathematics, determinacy is the study of under what circumstances one or the other player of a game must have a winning strategy, and the consequences of the existence of such strategies.-Games:...
for open setOpen setThe concept of an open set is fundamental to many areas of mathematics, especially point-set topology and metric topology. Intuitively speaking, a set U is open if any point x in U can be "moved" a small amount in any direction and still be in the set U...
s in the Baire spaceBaire spaceIn mathematics, a Baire space is a topological space which, intuitively speaking, is very large and has "enough" points for certain limit processes. It is named in honor of René-Louis Baire who introduced the concept.- Motivation :...
.
Π11 comprehension Π11-CA0
Π11-CA0 is stronger than arithmetical transfinite recursion and is fully impredicative. It consists of RCA0 plus the comprehension scheme for Π11 formulas.In a sense, Π11-CA0 comprehension is to arithmetical transfinite recursion (Σ11 separation) as ACA0 is to weak König's lemma (Σ01 separation). It is equivalent to several statements of descriptive set theory whose proofs make use of strongly impredicative arguments; this equivalence shows that these impredicative arguments cannot be removed.
The following theorems are equivalent to Π11-CA0 over RCA0:
- The Cantor–Bendixson theorem (every closed set of reals is the union of a perfect set and a countable set).
- Every countable abelian group is the direct sum of a divisible group and a reduced group.
Additional systems
- Weaker systems than recursive comprehension can be defined. The weak system RCA consists of elementary function arithmetic EFA (the basic axioms plus Δ00 induction in the enriched language with an exponential operation) plus Δ01 comprehension. Over RCA, recursive comprehension as defined earlier (that is, with Σ01 induction) is equivalent to the statement that a polynomial (over a countable field) has only finitely many roots and to the classification theorem for finitely generated Abelian groups. The system RCA has the same proof theoretic ordinal ω3 as EFA and is conservative over EFA for Π sentences.
- Weak Weak König's Lemma is the statement that a subtree of the infinite binary tree having no infinite paths has an asymptotically vanishing proportion of the leaves at length n (with a uniform estimate as to how many leaves of length n exist). An equivalent formulation is that any subset of Cantor space that has positive measure is nonempty (this is not provable in RCA0). WWKL0 is obtained by adjoining this axiom to RCA0. It is equivalent to the statement that if the unit real interval is covered by a sequence of intervals then the sum of their lengths is at least one. The model theory of WWKL0 is closely connected to the theory of algorithmically random sequenceAlgorithmically random sequenceIntuitively, an algorithmically random sequence is an infinite sequence ofbinary digits that appears random to any algorithm...
s. In particular, an ω-model of RCA0 satisfies weak weak König's lemma if and only if for every set X there is a set Y which is 1-random relative to X.
- DNR (short for "diagonally non-recursive") adds to RCA0 an axiom asserting the existence of a diagonally non-recursive function relative to every set. That is, DNR states that, for any set A, there exists a total function f such that for all e the eth partial recursive function with oracle A is not equal to f. DNR is strictly weaker than WWKL (Lempp et al., 2004).
- Δ11-comprehension is in certain ways analogous to arithmetical transfinite recursion as recursive comprehension is to weak König's lemma. It has the hyperarithmetical sets as minimal ω-model. Arithmetical transfinite recursion proves Δ11-comprehension but not the other way around.
- Σ11-choice is the statement that if η(n,X) is a Σ11 formula such that for each n there exists an X satisfying η then there is a sequence of sets Xn such that η(n,Xn) holds for each n. Σ11-choice also has the hyperarithmetical sets as minimal ω-model. Arithmetical transfinite recursion proves Σ11-choice but not the other way around.
ω-models and β-models
The ω in ω-model stands for the set of non-negative integers (or finite ordinals). An ω-model is a model for a fragment of second-order arithmetic whose first-order part is the standard model of Peano arithmetic, but whose second-order part may be non-standard. More precisely, an ω-model is given by a choice S⊆2ω of subsets of ω. The first order variables are interpreted in the usual way as elements of ω, and +, × have their usual meanings, while second order variables are interpreted as elements of S. There is a standard ω model where one just takes S to consist of all subsets of the integers. However there are also other ω-models; for example, RCA0 has a minimal ω-model where S consists of the recursive subsets of ω.A β model is an ω model that is equivalent to the standard ω-model for Π and Σ sentences (with parameters).
Non-ω models are also useful, especially in the proofs of conservation theorems.