Reverse mathematics is a program in
mathematical logic
Mathematical logic is the study of logic, formal logic within mathematics. Major subareas include model theory, proof theory, set theory, and recursion theory. Research in mathematical logic commonly addresses the mathematical properties of for ...
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
In mathematics, a theorem is a statement that has been proved, or can be proved. The ''proof'' of a theorem is a logical argument that uses the inference rules of a deductive system to establish that the theorem is a logical consequence of th ...
s to the
axiom
An axiom, postulate, or assumption is a statement that is taken to be true, to serve as a premise or starting point for further reasoning and arguments. The word comes from the Ancient Greek word (), meaning 'that which is thought worthy or f ...
s", in contrast to the ordinary mathematical practice of deriving theorems from axioms. It can be conceptualized as sculpting out
necessary conditions from
sufficient
In logic and mathematics, necessity and sufficiency are terms used to describe a conditional or implicational relationship between two statements. For example, in the conditional statement: "If then ", is necessary for , because the truth of ...
ones.
The reverse mathematics program was foreshadowed by results in
set theory
Set theory is the branch of mathematical logic that studies sets, which can be informally described as collections of objects. Although objects of any kind can be collected into a set, set theory, as a branch of mathematics, is mostly conce ...
such as the classical theorem that the
axiom of choice
In mathematics, the axiom of choice, or AC, is an axiom of set theory equivalent to the statement that ''a Cartesian product of a collection of non-empty sets is non-empty''. Informally put, the axiom of choice says that given any collectio ...
and
Zorn's lemma are equivalent over
ZF set theory ZF, Z-F, or Zf may refer to:
Businesses and organizations
* ZF Friedrichshafen, a German supplier of automobile transmissions
* Zionist Federation of Great Britain and Ireland, an organization established to campaign for a permanent homeland for th ...
. The goal of reverse mathematics, however, is to study possible axioms of ordinary theorems of mathematics rather than possible axioms for set theory.
Reverse mathematics is usually carried out using subsystems of
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.
A precurs ...
,
[Simpson, Stephen G. (2009), Subsystems of second-order arithmetic, Perspectives in Logic (2nd ed.), Cambridge University Press, doi:10.1017/CBO9780511581007, ISBN 978-0-521-88439-6, MR 2517689] where many of its definitions and methods are inspired by previous work in
constructive analysis
In mathematics, constructive analysis is mathematical analysis done according to some principles of constructive mathematics.
This contrasts with ''classical analysis'', which (in this context) simply means analysis done according to the (more comm ...
and
proof theory
Proof theory is a major branchAccording to Wang (1981), pp. 3–4, proof theory is one of four domains mathematical logic, together with model theory, axiomatic set theory, and recursion theory. Jon Barwise, Barwise (1978) consists of four correspo ...
. The use of second-order arithmetic also allows many techniques from
recursion theory
Computability theory, also known as recursion theory, is a branch of mathematical logic, computer science, and the theory of computation that originated in the 1930s with the study of computable functions and Turing degrees. The field has since e ...
to be employed; many results in reverse mathematics have corresponding results in
computable analysis
In mathematics and computer science, computable analysis is the study of mathematical analysis from the perspective of computability theory. It is concerned with the parts of real analysis and functional analysis that can be carried out in a co ...
. In ''higher-order'' reverse mathematics, the focus is on subsystems of
higher-order arithmetic, and the associated richer language.
The program was founded by and brought forward by
Steve Simpson. A standard reference for the subject is , while an introduction for non-specialists is . An introduction to higher-order reverse mathematics, and also the founding paper, 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
In mathematics, a sequence is an enumerated collection of objects in which repetitions are allowed and order matters. Like a set, it contains members (also called ''elements'', or ''terms''). The number of elements (possibly infinite) is calle ...
of
real number
In mathematics, a real number is a number that can be used to measure a ''continuous'' one-dimensional quantity such as a distance, duration or temperature. Here, ''continuous'' means that values can have arbitrarily small variations. Every real ...
s has a
supremum
In mathematics, the infimum (abbreviated inf; plural infima) of a subset S of a partially ordered set P is a greatest element in P that is less than or equal to each element of S, if such an element exists. Consequently, the term ''greatest l ...
” it is necessary to use a base system that 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 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.
A precurs ...
. 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 can be represented as either
natural number
In mathematics, the natural numbers are those numbers used for counting (as in "there are ''six'' coins on the table") and ordering (as in "this is the ''third'' largest city in the country").
Numbers used for counting are called ''Cardinal n ...
s or sets of natural numbers. For example, in order to prove theorems about real numbers, the real numbers can be represented as
Cauchy sequence
In mathematics
Mathematics is an area of knowledge that includes the topics of numbers, formulas and related structures, shapes and the spaces in which they are contained, and quantities and their changes. These topics are represented in m ...
s of
rational number
In mathematics, a rational number is a number that can be expressed as the quotient or fraction of two integers, a numerator and a non-zero denominator . For example, is a rational number, as is every integer (e.g. ). The set of all ration ...
s, each of which sequence can be represented as a set of natural numbers.
The axiom systems most often considered in reverse mathematics are defined using
axiom scheme In mathematical logic, an axiom schema (plural: axiom schemata or axiom schemas) generalizes the notion of axiom.
Formal definition
An axiom schema is a formula in the metalanguage of an axiomatic system, in which one or more schematic variables a ...
s 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
In mathematical logic, the arithmetical hierarchy, arithmetic hierarchy or Kleene–Mostowski hierarchy (after mathematicians Stephen Cole Kleene and Andrzej Mostowski) classifies certain sets based on the complexity of formulas that define th ...
and
analytical hierarchy
In mathematical logic and descriptive set theory, the analytical hierarchy is an extension of the arithmetical hierarchy. The analytical hierarchy of formulas includes formulas in the language of second-order arithmetic, which can have quantifiers ...
.
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 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 re ...
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
In mathematics and physics, a vector space (also called a linear space) is a set whose elements, often called ''vectors'', may be added together and multiplied ("scaled") by numbers called '' scalars''. Scalars are often real numbers, but can ...
has a basis" but it cannot express the principle "Every vector space has a basis". In practical terms, this means that theorems of
algebra
Algebra () is one of the broad areas of mathematics. Roughly speaking, algebra is the study of mathematical symbols and the rules for manipulating these symbols in formulas; it is a unifying thread of almost all of mathematics.
Elementary a ...
and
combinatorics
Combinatorics is an area of mathematics primarily concerned with counting, both as a means and an end in obtaining results, and certain properties of finite structures. It is closely related to many other areas of mathematics and has many appl ...
are restricted to countable structures, while theorems of
analysis
Analysis ( : analyses) is the process of breaking a complex topic or substance into smaller parts in order to gain a better understanding of it. The technique has been applied in the study of mathematics and logic since before Aristotle (38 ...
and
topology
In mathematics, topology (from the Greek language, Greek words , and ) is concerned with the properties of a mathematical object, geometric object that are preserved under Continuous function, continuous Deformation theory, deformations, such ...
are restricted to
separable space
In mathematics, a topological space is called separable if it contains a countable, dense subset; that is, there exists a sequence \_^ of elements of the space such that every nonempty open subset of the space contains at least one element of the ...
s. Many principles that imply the
axiom of choice
In mathematics, the axiom of choice, or AC, is an axiom of set theory equivalent to the statement that ''a Cartesian product of a collection of non-empty sets is non-empty''. Informally put, the axiom of choice says that given any collectio ...
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 RCA
0, the weakest system typically employed in reverse mathematics.
Use of higher-order arithmetic
A recent strand of ''higher-order'' reverse mathematics research, initiated by
Ulrich Kohlenbach
Ulrich Wilhelm Kohlenbach (born 27 July 1962 in Frankfurt am Main) is a German mathematician and professor of algebra and Mathematical logic, logic at the Technische Universität Darmstadt. His research interests lie in the field of proof mining ...
in 2005, focuses on subsystems of
higher-order arithmetic.
Due to the richer language of higher-order arithmetic, the use of representations (aka 'codes') common in second-order arithmetic, is greatly reduced.
For example, a continuous function on the
Cantor space In mathematics, a Cantor space, named for Georg Cantor, is a topological abstraction of the classical Cantor set: a topological space is a Cantor space if it is homeomorphic to the Cantor set. In set theory, the topological space 2ω is called "the ...
is just a function that maps binary sequences to binary sequences, and that also satisfies the usual 'epsilon-delta'-definition of continuity.
Higher-order reverse mathematics includes higher-order versions of (second-order) comprehension schemes. Such a higher-order axiom states the existence of a functional that decides the truth or falsity of formulas of a given complexity. In this context, the complexity of formulas is also measured using the
arithmetical hierarchy
In mathematical logic, the arithmetical hierarchy, arithmetic hierarchy or Kleene–Mostowski hierarchy (after mathematicians Stephen Cole Kleene and Andrzej Mostowski) classifies certain sets based on the complexity of formulas that define th ...
and
analytical hierarchy
In mathematical logic and descriptive set theory, the analytical hierarchy is an extension of the arithmetical hierarchy. The analytical hierarchy of formulas includes formulas in the language of second-order arithmetic, which can have quantifiers ...
. The higher-order counterparts of the major subsystems of second-order arithmetic generally prove the same second-order sentences (or a large subset) as the original second-order systems.
[See and .] For instance, the base theory of higher-order reverse mathematics, called , proves the same sentences as RCA
0, up to language.
As noted in the previous paragraph, second-order comprehension axioms easily generalize to the higher-order framework. However, theorems expressing the ''
compactness'' of basic spaces behave quite differently in second- and higher-order arithmetic: on one hand, when restricted to countable covers/the language of second-order arithmetic, the compactness of the unit interval is provable in WKL
0 from the next section. On the other hand, given uncountable covers/the language of higher-order arithmetic, the compactness of the unit interval is only provable from (full) second-order arithmetic. Other covering lemmas (e.g. due to
Lindelöf,
Vitali Vitali, Vitalii, Vitaly, Vitaliy and may refer to:
People Given name
* Vitaly Borker (born 1975 or 1976), Ukrainian American Internet fraudster and cyberbully
* Vitaly Churkin (1952–2017), Russian politician
* Vitaly Ginzburg (1916–2009), Russ ...
,
Besicovitch
Abram Samoilovitch Besicovitch (or Besikovitch) (russian: link=no, Абра́м Само́йлович Безико́вич; 23 January 1891 – 2 November 1970) was a Russian mathematician, who worked mainly in England. He was born in Berdyansk ...
, etc.) exhibit the same behavior, and many basic properties of the
gauge integral are equivalent to the compactness of the underlying space.
The big five 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.
A precurs ...
is a formal theory of the natural numbers and sets of natural numbers. Many mathematical objects, such as
countable
In mathematics, a set is countable if either it is finite or it can be made in one to one correspondence with the set of natural numbers. Equivalently, a set is ''countable'' if there exists an injective function from it into the natural numbers; ...
rings
Ring may refer to:
* Ring (jewellery), a round band, usually made of metal, worn as ornamental jewelry
* To make a sound with a bell, and the sound made by a bell
:(hence) to initiate a telephone connection
Arts, entertainment and media Film and ...
,
groups
A group is a number of persons or things that are located, gathered, or classed together.
Groups of people
* Cultural group, a group whose members share the same cultural identity
* Ethnic group, a group whose members share the same ethnic ide ...
, and
fields
Fields may refer to:
Music
* Fields (band), an indie rock band formed in 2006
* Fields (progressive rock band), a progressive rock band formed in 1971
* ''Fields'' (album), an LP by Swedish-based indie rock band Junip (2010)
* "Fields", a song b ...
, as well as points in
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. In particular, standard examples ...
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 RCA
0, WKL
0, ACA
0, ATR
0, and Π-CA
0.
The following table summarizes the "big five" systems and lists the counterpart systems in higher-order arithmetic.
[
The latter generally prove the same second-order sentences (or a large subset) as the original second-order 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 . This together with the full comprehension axiom of second-order arithmetic implies the full second-order induction scheme given by the universal closure of 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 arithmetic
In mathematics, Robinson arithmetic is a finitely axiomatized fragment of first-order Peano arithmetic (PA), first set out by R. M. Robinson in 1950. It is usually denoted Q. Q is almost PA without the axiom schema of mathematical induction. Q is ...
, 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 that 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 may refer to:
Art and architecture
* Constructivism (art), an early 20th-century artistic movement that extols art as a practice for social purposes
* Constructivist architecture, an architectural movement in Russia in the 1920s a ...
because it is a theory in classical logic including the law of excluded middle
In logic, the law of excluded middle (or the principle of excluded middle) states that for every proposition, either this proposition or its negation is true. It is one of the so-called three laws of thought, along with the law of noncontradic ...
.
Despite its seeming weakness (of not proving any non-computable 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 field
In mathematics, an ordered field is a field together with a total ordering of its elements that is compatible with the field operations. The basic example of an ordered field is the field of real numbers, and every Dedekind-complete ordered field ...
).
* Basic properties of the real numbers (the real numbers are an Archimedean 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 theorem
The Baire category theorem (BCT) is an important result 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 (a topological space such that the ...
for a complete
Complete may refer to:
Logic
* Completeness (logic)
* Completeness of a theory, the property of a theory that every formula in the theory's language or its negation is provable
Mathematics
* The completeness of the real numbers, which implies t ...
separable metric space
In mathematics, a metric space is a set together with a notion of ''distance'' between its elements, usually called points. The distance is measured by a function called a metric or distance function. Metric spaces are the most general settin ...
(the separability condition is necessary to even state the theorem in the language of second-order arithmetic).
* The intermediate value theorem on continuous real functions.
* The Banach–Steinhaus theorem
In mathematics, the uniform boundedness principle or Banach–Steinhaus theorem is one of the fundamental results in functional analysis.
Together with the Hahn–Banach theorem and the open mapping theorem, it is considered one of the cornerst ...
for a sequence of continuous linear operators on separable Banach spaces.
* A weak version of Gödel's completeness theorem
Gö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.
The completeness theorem applies to any first-order theory: I ...
(for a set of sentences, in a countable language, that is already closed under consequence).
* The existence of an algebraic closure
In 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.
Using Zorn's lemmaMcCarthy (1991) p.21Kaplansky (1 ...
for a countable field (but not its uniqueness).
* The existence and uniqueness of the real closure 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
Induction, Inducible or Inductive may refer to:
Biology and medicine
* Labor induction (birth/pregnancy)
* Induction chemotherapy, in medicine
* Induced stem cells, stem cells derived from somatic, reproductive, pluripotent or other cell t ...
limited to Σ 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 lemma
Kőnig's lemma or Kőnig's infinity lemma is a theorem in graph theory due to the Hungarian mathematician Dénes Kőnig who published it in 1927. It gives a sufficient condition for an infinite graph to have an infinitely long path. The computab ...
, 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 Σ separation (given two Σ formulas of a free variable ''n'' that 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 that 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
In mathematics, the axiom of choice, or AC, is an axiom of set theory equivalent to the statement that ''a Cartesian product of a collection of non-empty sets is non-empty''. Informally put, the axiom of choice says that given any collectio ...
(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 that 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 that 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 theorem 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 Riemann
Georg Friedrich Bernhard Riemann (; 17 September 1826 – 20 July 1866) was a German mathematician who made contributions to analysis, number theory, and differential geometry. In the field of real analysis, he is mostly known for the first rig ...
integrable.
* The Brouwer fixed point theorem
Brouwer's fixed-point theorem is a fixed-point theorem in topology, named after L. E. J. (Bertus) Brouwer. It states that for any continuous function f mapping a compact convex set to itself there is a point x_0 such that f(x_0)=x_0. The simplest ...
(for continuous functions on a finite product of copies of the closed unit interval).
* The separable Hahn–Banach theorem
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 f ...
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 theorem
In topology, the Jordan curve theorem asserts that every ''Jordan curve'' (a plane simple closed curve) divides the plane into an " interior" region bounded by the curve and an "exterior" region containing all of the nearby and far away exterior ...
* Gödel's completeness theorem (for a countable language).
* Determinacy for open (or even clopen) games on of length ω.
* Every countable commutative ring
In mathematics, a commutative ring is a ring in which the multiplication operation is commutative. The study of commutative rings is called commutative algebra. Complementarily, noncommutative algebra is the study of ring properties that are not sp ...
has a prime ideal
In algebra, a prime ideal is a subset of a ring that shares many important properties of a prime number in the ring of integers. The prime ideals for the integers are the sets that contain all the multiples of a given prime number, together with ...
.
* 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 using the low basis theorem The low basis theorem is one of several basis theorems in computability theory, each of which showing that, given an infinite subtree of the binary tree 2^, it is possible to find an infinite path through the tree with particular computability prop ...
, 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 theorem
In mathematics, specifically in real analysis, the Bolzano–Weierstrass theorem, named after Bernard Bolzano and Karl Weierstrass, is a fundamental result about convergence in a finite-dimensional Euclidean space \R^n. The theorem states that each ...
.
* 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 ideal
In mathematics, more specifically in ring theory, a maximal ideal is an ideal that is maximal (with respect to set inclusion) amongst all ''proper'' ideals. In other words, ''I'' is a maximal ideal of a ring ''R'' if there are no other ideals cont ...
.
* Every countable vector space over the rationals (or over any countable field) has a basis.
* Every countable field has a transcendence basis
In abstract algebra, the transcendence degree of a field extension ''L'' / ''K'' is a certain rather coarse measure of the "size" of the extension. Specifically, it is defined as the largest cardinality of an algebraically independent subset ...
.
* 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
In combinatorics, Ramsey's theorem, in one of its graph-theoretic forms, states that one will find monochromatic cliques in any edge labelling (with colours) of a sufficiently large complete graph. To demonstrate the theorem for two colours (say ...
.
Arithmetical transfinite recursion ATR0
The system ATR0 adds to ACA0 an axiom that 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
In mathematics, a well-order (or well-ordering or well-order relation) on a set ''S'' is a total order on ''S'' with the property that every non-empty subset of ''S'' has a least element in this ordering. The set ''S'' together with the well-o ...
starting with any set. ATR0 is equivalent over ACA0 to the principle of Σ separation. ATR0 is impredicative, and has the proof-theoretic ordinal
In proof theory, ordinal analysis assigns ordinals (often large countable 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 ...
, 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:
* 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 In mathematics, the height of an element ''g'' of an abelian group ''A'' is an invariant that captures its divisibility properties: it is the largest natural number ''N'' such that the equation ''Nx'' = ''g'' has a solution ''x'' ∈ ''A' ...
for countable reduced Abelian groups.
* The perfect set theorem, which states that every uncountable closed subset of a complete separable metric space contains a perfect closed set.
* Lusin's separation theorem
In 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
In mathematics, a Borel set is any set in a topological space ...
(essentially Σ separation).
* Determinacy
Determinacy is a subfield of set theory, a branch of mathematics, that examines the conditions under which one or the other player of a game has a winning strategy, and the consequences of the existence of such strategies. Alternatively and sim ...
for open set
In mathematics, open sets are a generalization of open intervals in the real line.
In a metric space (a set along with a distance defined between any two points), open sets are the sets that, with every point , contain all points that are suf ...
s in the Baire space
In mathematics, a topological space X is said to be a Baire space if countable unions of closed sets with empty interior also have empty interior.
According to the Baire category theorem, compact Hausdorff spaces and complete metric spaces are ...
.
Π comprehension Π-CA0
Π-CA0 is stronger than arithmetical transfinite recursion and is fully impredicative. It consists of RCA0 plus the comprehension scheme for Π formulas.
In a sense, Π-CA0 comprehension is to arithmetical transfinite recursion (Σ separation) as ACA0 is to weak Kőnig's lemma (Σ 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 Π-CA0 over RCA0:
* The Cantor–Bendixson theorem In 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 (Kechris 1995, p. 150). Note that having the perfect set property is not the same as being a p ...
(every closed set of reals is the union of a perfect set and a countable set).
* Silver's dichotomy (every coanalytic equivalence relation has either countably many equivalence classes or a perfect set of incomparables)
* 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
In proof theory, a branch of mathematical logic, elementary function arithmetic (EFA), also called elementary arithmetic and exponential function arithmetic,C. Smoryński, "Nonstandard Models and Related Developments" (p. 217). From ''Harvey Frie ...
EFA (the basic axioms plus Δ induction in the enriched language with an exponential operation) plus Δ comprehension. Over RCA, recursive comprehension as defined earlier (that is, with Σ 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
In proof theory, ordinal analysis assigns ordinals (often large countable 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 ...
ω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 sequence
Intuitively, an algorithmically random sequence (or random sequence) is a Sequence#Infinite sequences in theoretical computer science, sequence of binary digits that appears random to any algorithm running on a (prefix-free or not) universal Turi ...
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'' that 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 ''e''th partial recursive function with oracle ''A'' is not equal to ''f''. DNR is strictly weaker than WWKL (Lempp ''et al.'', 2004).
* Δ-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 Δ-comprehension but not the other way around.
* Σ-choice is the statement that if ''η''(''n'',''X'') is a Σ 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''. Σ-choice also has the hyperarithmetical sets as minimal ω-model. Arithmetical transfinite recursion proves Σ-choice but not the other way around.
* HBU (short for "uncountable Heine-Borel") expresses the (open-cover) compactness of the unit interval, involving ''uncountable covers''. The latter aspect of HBU makes it only expressible in the language of ''third-order'' arithmetic. Cousin's theorem (1895) implies HBU, and these theorems use the same notion of cover due to Cousin
Most generally, in the lineal kinship system used in the English-speaking world, a cousin is a type of familial relationship in which two relatives are two or more familial generations away from their most recent common ancestor. Commonly, " ...
and Lindelöf. HBU is ''hard'' to prove: in terms of the usual hierarchy of comprehension axioms, a proof of HBU requires full second-order arithmetic.
* Ramsey's theorem
In combinatorics, Ramsey's theorem, in one of its graph-theoretic forms, states that one will find monochromatic cliques in any edge labelling (with colours) of a sufficiently large complete graph. To demonstrate the theorem for two colours (say ...
for infinite graphs does not fall into one of the big five subsystems, and there are many other weaker variants with varying proof strengths.
Stronger Systems
Over RCA0, Π transfinite recursion, ∆ determinacy, and the ∆ Ramsey theorem are all equivalent to each other.
Over RCA0, Σ monotonic induction, Σ determinacy, and the Σ Ramsey theorem are all equivalent to each other.
The following are equivalent:
* (schema) Π consequences of Π-CA0
* RCA0 + (schema over finite ''n'') determinacy in the ''n''th level of the difference hierarchy of Σ sets
* RCA0 +
The set of Π consequences of second-order arithmetic Z2 has the same theory as RCA0 + (schema over finite ''n'') determinacy in the ''n''th level of the difference hierarchy of Σ sets.
ω-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 agrees with the standard ω-model on truth of Π and Σ sentences (with parameters).
Non-ω models are also useful, especially in the proofs of conservation theorems.
See also
* Closed-form expression § Conversion from numerical forms
* Induction, bounding and least number principles
* Ordinal analysis
In proof theory, ordinal analysis assigns ordinals (often large countable 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 ...
Notes
References
*
*
*
*
*
*
*
*
*
*
External links
Harvey Friedman's home page
Stephen G. Simpson's home page
Reverse Mathematics Zoo
{{Mathematical logic
Computability theory
Mathematical logic
Proof theory