- Reverse mathematics
**Reverse mathematics**is a program inmathematical logic that seeks to determine which axioms are required to prove theorems of mathematics. The method can briefly be described as "going backwards from thetheorem s to theaxiom s." This contrasts with the ordinary mathematical practice of deriving theorems from axioms.This program was foreshadowed by results in set theory such as the classical theorem that the

axiom of choice andZorn's lemma are equivalent overZF 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 carried out using subsystems of

second-order arithmetic . Many of its definitions and methods were inspired by work inconstructive analysis . The use of second-order arithmetic also allows many techniques fromrecursion theory to be employed; many results in reverse mathematics have corresponding results incomputable analysis .The program was founded by

Harvey Friedman in his article "Some systems of second order arithmetic and their use" and abstracts "Systems of second order arithmetic with restricted induction" (I and II). The program was pursued by many researchers in mathematical logic. The primary reference for the subject is by Simpson [1999] .**General principles**The principle of reverse mathematics is the following: 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 the theorem. For example, in order to study the theorem “Every bounded sequence of

real number s has asupremum ” it is necessary to use a base system which can speak of real numbers and sequences of real numbers.The goal is to determine the particular axiom system stronger than the base system that is "necessary" to prove the theorem. This requires two proofs. The first proof shows that the axiom system "S" implies the theorem; this is an ordinary mathematical proof along with a justification that it can be carried out in the axiom system at hand. The second proof, known as a

**reversal**, shows that the theorem implies "S"; this proof is carried out in the base system. The reversal shows that no weaker axiom system than "S" can prove the theorem, because any second axiom system which implies the theorem must already imply "S".In most results of reverse mathematics, both the axiom system "T" and the base system are taken to be subsystems of

second-order arithmetic ; the large body of research in reverse mathematics has established weak subsystems of second-order arithmetic suffice to formalize almost all undergraduate-level mathematics. In second-order arithmetic, all objects must be represented as eithernatural number s or sets of natural numbers. For example, in order to prove theorems about real numbers, the real numbers must be represented asCauchy sequence s ofrational 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 scheme 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 thearithmetical hierarchy andanalytical 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.**Subsystems of second order arithmetic**::"Main article:

Second-order arithmetic ".Second order arithmetic is a formal theory of the natural numbers and sets of natural numbers. Many mathematical objects, such as countable 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 havemeaning, this system must not itself be able to prove the mathematical theorem "T".Simpson [1999] 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Π^{1}_{1}-CA_{0}; they are defined indetail in the article onsecond order arithmetic .**The base system**The subsystem RCA

_{0}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 RCA_{0}corresponds informally to "computable mathematics". In particular, any set of natural numbers that can be proven to exist in RCA_{0}is computable, and thus any theorem which implies that noncomputable sets exist is not provable in RCA_{0}To this extent, RCA_{0}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), RCA

_{0}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 RCA_{0}include:

* Basic properties of the natural numbers, integers, and rational numbers (for example, that the latter form anordered field ).

* Basic properties of the real numbers (the real numbers are an Archimedean ordered field; anynested sequence of closed intervals whose lengths tend to zero has a single point in its intersection; the real numbers are not countable).

* TheBaire category theorem for a complete separablemetric space (the separability condition is necessary to even state the theorem in the language of second-order arithmetic).

* Theintermediate value theorem on continuous real functions.

* The Banach-Steinhaus theorem for a sequence of continuous linear operators on separable Banach spaces.

* A weak version ofGödel's completeness theorem (for a set of sentences, in a countable language, that is already closed under consequence).

* The existence of analgebraic closure 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 RCA

_{0}(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 Σ^{0}_{1}formulas. It is provably consistent, as is RCA_{0}, in full first-order Peano arithmetic.**Weak König's lemma**The subsystem WKL

_{0}consists of RCA_{0}plus a weak form ofKönig's lemma , 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. WKL_{0}can also be defined as the principle of Σ^{0}_{1}separation (given two Σ^{0}_{1}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 the sentence which says that any infinite subtree of the binary tree has an infinite path. When this axiom is added to RCA

_{0}, the resulting subsystem is called WKL_{0}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 WKL

_{0}is actually stronger than (not provable in) RCA_{0}, it is sufficient to exhibit a theorem of WKL_{0}which implies that noncomputable sets exist. This is not difficult; WKL_{0}implies the existence of separating sets for effectively inseparable recursively enumerable sets.It turns out that RCA

_{0}and WKL_{0}have the same first-order part, meaning that they prove the same first-order sentences. WKL_{0}can prove a good number of classical mathematical results which do not follow from RCA_{0}, 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 WKL

_{0}over RCA_{0}:* 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 integrable.

* TheBrouwer fixed point theorem (for continuous functions on a finite product of copies of the closed unit interval).

* The separableHahn-Banach theorem 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.

* Gödel's completeness theorem (for a countable language).

* Every countablecommutative ring has aprime ideal .

* Every countable formally real field is orderable.

* Uniqueness of algebraic closure (for a countable field).**Arithmetical comprehension**ACA

_{0}is RCA_{0}plus the comprehension scheme for arithmetical formulas (which is sometimes called the "arithmetical comprehension axiom"). That is, ACA_{0}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 RCA_{0}the comprehension scheme for Σ_{1}formulas in order to obtain full arithmetical comprehension.The first-order part of ACA

_{0}is exactly first-order Peano arithmetic; ACA_{0}is a "conservative" extension of first-order Peano arithmetic. The two systems are provably (in a weak system) equiconsistent. ACA_{0}can be thought of as a framework of predicative mathematics, although there are predicatively provable theorems that are not provable in ACA_{0}. 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 ACA

_{0}is stronger than WKL_{0}is to exhibit a model of WKL_{0}that doesn't contain all arithmetical sets. In fact, it is possible to build a model of WKL_{0}consisting entirely of low sets using thelow basis theorem , since low sets relative to low sets are low.The following assertions are equivalent to ACA

_{0}over RCA_{0}:

* The sequential completeness of the real numbers (every bounded increasing sequence of real numbers has a limit).

* TheBolzano-Weierstrass theorem .

*Ascoli's theorem : every bounded equicontinuous sequence of real functions on the unit interval has a uniformly convergent subsequence.

* Every countable commutative ring has amaximal ideal .

* Every countable vector space over the rationals (or over any countable field) has a basis.

* Every countable field has atranscendence 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**The system ATR

_{0}adds to ACA_{0}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 countablewell ordering starting with any set. ATR_{0}is equivalent over ACA_{0}to the principle of Σ^{1}_{1}separation. ATR_{0}is impredicative, and has the proof-theoretic ordinal $Gamma\_0$, the supremum of that of predicative systems.ATR

_{0}proves the consistency of ACA_{0}, and thus by Gödel's theorem it is strictly stronger.The following assertions are equivalent to ATR

_{0}over RCA_{0}:

* Any two countablewell ordering s 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 theorem, which states that every uncountable closed subset of a complete separable metric space contains a perfect closed set.

*Lusin's separation theorem (essentially Σ^{1}_{1}separation).

*Determinacy foropen set s in theBaire space .**Π**^{1}_{1}comprehensionΠ

^{1}_{1}-CA_{0}is stronger than arithmetical transfinite recursion and is fully impredicative. It consists of RCA_{0}plus the comprehension scheme for Π^{1}_{1}formulas.In a sense, Π

^{1}_{1}-CA_{0}comprehension is to arithmetical transfinite recursion (Σ^{1}_{1}separation) as ACA_{0}is to weak König's lemma (Σ^{0}_{1}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 Π

^{1}_{1}-CA_{0}over RCA_{0}:

* TheCantor-Bendixson theorem (every closed set of reals is the union of a perfect set and a countable set).

* Every Abelian group is the direct sum of a divisible group and a reduced group.**Additional systems*** Weaker systems than recursive comprehension can be defined. Over such a weak system as elementary function arithmetic (the basic axioms plus Δ

^{0}_{0}induction in the enriched language with an exponential operation) plus Δ^{0}_{1}comprehension, recursive comprehension as defined earlier (that is, with Σ^{0}_{1}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.* 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 RCA

_{0}). WWKL_{0}is obtained by adjoining this axiom to RCA_{0}. 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 WWKL_{0}is closely connected to the theory ofalgorithmically random sequence s. In particular, an ω-model of RCA_{0}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 RCA

_{0}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).* Δ

^{1}_{1}-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 Δ^{1}_{1}-comprehension but not the other way around.* Σ

^{1}_{1}-choice is the statement that if η("n","X") is a Σ^{1}_{1}formula such that for each "n" there exists an "X" satisfying η then there is a sequence of sets "X_{n}" such that η("n","X_{n}") holds for each "n". Σ^{1}_{1}-choice also has the hyperarithmetical sets as minimal ω-model. Arithmetical transfinite recursion proves Σ^{1}_{1}-choice but not the other way around.**References*** cite journal

author = Ambos-Spies, K.

coauthors = Kjos-Hanssen, B.; Lempp, S.; Slaman, T.A.

year = 2004

title = Comparing DNR and WWKL

journal = Journal of Symbolic Logic

volume = 69

issue = 4* Harvey Friedman. "Some systems of second order arithmetic and their use". "Proceedings of the International Congress of Mathematicians (Vancouver, B.C., 1974), Vol. 1", pp. 235–242. "Canad. Math. Congress, Montreal, Que.", 1975.

* Harvey Friedman. "Systems of second order arithmetic with restricted induction," I, II (Abstracts). "Journal of Symbolic Logic", v.41, pp. 557-- 559, 1976. [

*http://www.jstor.org/stable/2272259 JStor*]* Stephen G. Simpson. "Subsystems of Second Order Arithmetic". Perspectives in Mathematical Logic, Springer-Verlag, Berlin, 1999. ISBN 3-540-64882-8 (first chapter available online [

*http://www.math.psu.edu/simpson/sosoa*] ).* Reed Solomon. "Ordered Groups: A Case Study in Reverse Mathematics". "The Bulletin of Symbolic Logic", v. 5 n. 1 (Mar., 1999), pp. 45-58.

**External links*** [

*http://www.math.ohio-state.edu/~friedman/ Harvey Friedman's home page*]

* [*http://www.math.psu.edu/simpson/ Stephen G. Simpson's home page*]

*Wikimedia Foundation.
2010.*

### Look at other dictionaries:

**Reverse Mathematik**— Die reverse Mathematik, ein Teilgebiet der mathematischen Logik, versucht zu bestimmen, welche Axiome notwendig sind, um bestimmte Theoreme zu beweisen. Reverse Mathematik ist damit gewissermaßen die Umkehrung der gewöhnlichen Mathematik, die… … Deutsch Wikipedia**Reverse Monte Carlo**— (RMC) is a variation of the standard Metropolis Hastings algorithm to solve an inverse problem probing the configuration space though a random walk in search for set of parameters that is consistent with experimental data. An inverse problem is… … Wikipedia**Mathematics and Physical Sciences**— ▪ 2003 Introduction Mathematics Mathematics in 2002 was marked by two discoveries in number theory. The first may have practical implications; the second satisfied a 150 year old curiosity. Computer scientist Manindra Agrawal of the… … Universalium**Mathematics of radio engineering**— A complex valued function. The mathematics of radio engineering is a pleasant and very useful subject. This article is an attempt to provide a reasonably comprehensive summary of this almost limitless topic. While the ideas have historically… … Wikipedia**Reverse auction**— A reverse auction (also called procurement auction, e auction, sourcing event, e sourcing or eRA) is a tool used in industrial business to business procurement. It is a type of auction in which the role of the buyer and seller are reversed, with… … Wikipedia**mathematics**— /math euh mat iks/, n. 1. (used with a sing. v.) the systematic treatment of magnitude, relationships between figures and forms, and relations between quantities expressed symbolically. 2. (used with a sing. or pl. v.) mathematical procedures,… … Universalium**Mathematics of CRC**— Cyclic Redundancy Check (CRC) is based on division in the ring of polynomials over the finite field GF(2) (the integers modulo 2), that is, the set of polynomials where each coefficient is either zero or one, and arithmetic operations wrap around … Wikipedia**List of mathematics articles (R)**— NOTOC R R. A. Fisher Lectureship Rabdology Rabin automaton Rabin signature algorithm Rabinovich Fabrikant equations Rabinowitsch trick Racah polynomials Racah W coefficient Racetrack (game) Racks and quandles Radar chart Rademacher complexity… … Wikipedia**Foundations of mathematics**— is a term sometimes used for certain fields of mathematics, such as mathematical logic, axiomatic set theory, proof theory, model theory, and recursion theory. The search for foundations of mathematics is also a central question of the philosophy … Wikipedia**Milman's reverse Brunn–Minkowski inequality**— In mathematics, Milman s reverse Brunn Minkowski inequality is a result due to Vitali Milman that provides a reverse inequality to the famous Brunn Minkowski inequality for convex bodies in n dimensional Euclidean space Rn. At first sight, such a … Wikipedia