Reverse mathematics

From Wikipedia, the free encyclopedia

Reverse mathematics is a program in mathematical logic that seeks to determine which axioms are required to prove theorems of mathematics. The method can briefly be described as “going backwards from the theorems to the axioms” rather than the usual direction (from the axioms to the theorems).

This 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.

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 reseachers in mathematical logic. Stephen Simpson [1999] wrote the primary reference book on the subject.

1 General principles
2 Subsystems of second order arithmetic
3 The base system
4 Weak König's lemma
5 Arithmetical comprehension
6 Arithmetical Transfinite Recursion
7 Π11 comprehension
8 Additional systems
9 An example of a reverse mathematics proof
10 References
11 External links

[edit] 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 numbers has a supremum” 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 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 the axiom system; this proof is carried out in the base system. The reversal shows that no weaker axiom system can prove the theorem, because any second axiom system which implies the theorem must already imply the first axiom system.

Reverse mathematics uses the framework of subsystems of second order arithmetic, rather than set theory, to formalize ordinary mathematics. This is because the language of set theory is so expressive that extremely complex sets of natural numbers can be defined by simple formulas. The arithmetical hierarchy and analytical hierarchy show that the complexity of a set definable in the language of second order arithmetic is closely related to the complexity of the defining formula.

[edit] 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 spaces, 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 arithemtic 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.

Simpson [1999] describes five particular subsystems of second order arithmetic, which he calls the Big Five, which occur frequently in reverse mathematics. In order of increasing strength, these systems are named by the acronyms $\mathsf{RCA}_0$ , $\mathsf{WKL}_0$ , $\mathsf{ACA}_0$ , $\mathsf{ATR}_0$ , and $\Pi^1_1\mathsf{-CA}_0$ ; they are defined in detail in the article on second order arithmetic.

[edit] The base system

$\mathsf{RCA}_0$ is the base system. The overall goal of reverse mathematics is to take specific theorems of classical mathematics and show that these theorems are either provable in $\mathsf{RCA}_0$ or equivalent to one of the other systems.

$\mathsf{RCA}_0$ corresponds informally to "computable mathematics". In particular, any set of natural numbers which can be proven to exist in $\mathsf{RCA}_0$ is computable, and thus any theorem which implies that noncomputable sets exist is not provable in $\mathsf{RCA}_0$ . To this extent, $\mathsf{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, $\mathsf{RCA}_0$ is sufficient to prove a number of classical theorems which are, 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 $\mathsf{RCA}_0$ include:

Basic properties of the natural numbers, integers, and rational numbers (for example, that the latter form an 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 for a complete separable metric space (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 for a sequence of continuous linear operators on separable Banach spaces.
A weak version of Gödel's completeness theorem (for a set of sentences, in a countable language, that is already closed under consequence).
The existence of an algebraic 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 $\mathsf{RCA}_0$ (in other words, theorems of the system which do not involve any set variables) is the set of theorems of first-order Peano arithmetic with induction limited to Σ⁰₁ formulas. It is provably consistent, as is $\mathsf{RCA}_0$ , in full first-order Peano arithmetic.

[edit] Weak König's lemma

The subsystem $\mathsf{WKL}_0$ consists of $\mathsf{RCA}_0$ plus a weak form of Kö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. $\mathsf{WKL}_0$ can also be defined as the principle of Σ⁰₁ separation (given two Σ⁰₁ 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 $\mathsf{RCA}_0$ , the resulting subsystem is called $\mathsf{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 see that $\mathsf{WKL}_0$ is actually stronger than (not provable in) $\mathsf{RCA}_0$ , it is sufficient to exhibit a theorem of $\mathsf{WKL}_0$ which implies that noncomputable sets exist. This is not difficult; $\mathsf{WKL}_0$ implies the existence of separating sets for effectively inseparable recursively enumerable sets.

It turns out that $\mathsf{RCA}_0$ and $\mathsf{WKL}_0$ have the same first-order part. Weak König's lemma can prove a good number of classical mathematical results which do not follow from $\mathsf{RCA}_0$ .

The following results are equivalent to weak König's lemma and thus to $\mathsf{WKL}_0$ over $\mathsf{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.
The Brouwer fixed point theorem (for continuous functions on a finite product of copies of the closed unit interval).
The separable Hahn-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 countable commutative ring has a prime ideal.
Every countable formally real field is orderable.
Uniqueness of algebraic closure (for a countable field).

[edit] Arithmetical comprehension

$\mathsf{ACA}_0$ is $\mathsf{RCA}_0$ plus the comprehension scheme for arithmetical formulas. That is, it 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 $\mathsf{RCA}_0$ the comprehension scheme for Σ₁ formulas in order to obtain full arithmetical comprehension.

The first-order part of $\mathsf{ACA}_0$ turns out to be exactly first-order Peano arithmetic; $\mathsf{ACA}_0$ is a conservative extension of first-order Peano arithmetic. The two systems are provably (in a weak system) equiconsistent. $\mathsf{ACA}_0$ can be thought of as a framework of predicative mathematics, although there are predicatively provable theorems that are not provable in $\mathsf{ACA}_0$ . Seemingly every natural arithmetical result, and many other mathematical theorems, can be proven in this system.

The following assertions are equivalent to $\mathsf{ACA}_0$ over $\mathsf{RCA}_0$ :

The sequential completeness of the real numbers (every bounded increasing sequence of real numbers has a limit).
The Bolzano-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 a maximal ideal.
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.

[edit] Arithmetical Transfinite Recursion

The system $\mathsf{ATR}_0$ adds to $\mathsf{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 countable well ordering (a total countable order with no infinite decreasing sequence) starting with any set. $\mathsf{ATR}_0$ is equivalent over $\mathsf{ACA}_0$ to the principle of Σ¹₁ separation. Although $A T R 0$ is impredicative, it has the same proof-theretic ordinal $Γ 0$ as predicative systems.

$\mathsf{ATR}_0$ proves the consistency of arithmetical comprehension, so by Gödel's theorem it is strictly stronger.

The following assertions are equivalent to $\mathsf{ATR}_0$ over $\mathsf{RCA}_0$ :

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 theorem: every uncountable closed subset of a complete separable metric space contains a perfect closed set.
Lusin's separation theorem (essentially Σ¹₁ separation).
Open determinacy in the Baire space.

[edit] Π¹₁ comprehension

$\Pi^1_1\mathsf{-CA}_0$ is stronger than arithmetical transfinite recursion and is fully impredicative. It consists of $\mathsf{RCA}_0$ plus the comprehension scheme for Π¹₁ formulas.

In a sense, $\Pi^1_1\mathsf{-CA}_0$ comprehension is to arithmetical transfinite recursion (Σ¹₁ separation) as $\mathsf{ACA}_0$ 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 $\Pi^1_1\mathsf{-CA}_0$ over $\mathsf{RCA}_0$ :

The Cantor-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.

[edit] Additional systems

Weaker systems than recursive comprehension can be defined. Over such a weak system as elementary function arithmetic (the basic axioms plus Δ⁰₀ induction in the enriched language with an exponential operation) plus Δ⁰₁ comprehension, 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.

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 unifoirm 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< math>\mathsf{RCA}_0</math>). $\mathsf{WWKL}_0$ is obtained by adjoining this axiom to $\mathsf{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 $\mathsf{WWKL}_0$ is closely connected to the theory of algorithmically random sequences. In particular, an ω-model of $\mathsf{RCA}_0$ satisfies weak weak Konig's lemma if and only if for every set X there is a set Y which is 1-random relative to X.

Δ¹₁-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 X_n such that η(n,X_n) holds for each n. Σ¹₁-choice also has the hyperarithmetical sets as minimal ω-model. Arithmetical transfinite recursion proves Σ¹₁-choice but not the other way around.

[edit] An example of a reverse mathematics proof

As an example of the theory, we sketch the proof that the Bolzano-Weierstraß theorem (in the form: every bounded sequence of real numbers has a least upper bound) is equivalent to arithmetical comprehension over $\mathsf{RCA}_0$ . We define a “real number” to be a sequence of rationals such that the difference between the nth and (n + 1)th terms is always less than 2⁻ⁿ.

For the forward direction (proving Bolzano-Weierstraß from arithmetical comprehension), we proceed by dichotomy as usual. For definiteness, assume the sequence is bounded between 0 and 1. For each n, divide the interval in 2⁻ⁿ subintervals of equal lengths, and consider the first of these for which infinitely many terms of the sequence lie in the subinterval: defining this requires arithmetical comprehension (because of the “for infinitely many terms”). Then take the subsequence formed by the first element from each the selected nested subintervals.

It may appear at first sight that weak König's lemma should suffice, because the nested intervals form a binary tree like in the hypothesis of weak König's lemma and we are taking a finite branch. This is not true because the tree consisting of those binary intervals containing an element of the sequence requires arithmetical comprehension to define.

For the reversal, the idea is as follows: to prove arithmetical comprehension it is actually sufficient to prove Σ⁰₁ comprehension, because that implies arithmetical comprehension. Now this means, essentially, that given a Σ⁰₀ formula θ(m,n) we must prove the comprehension axiom for the formula ∃m(θ(m,n)). To do so, we construct a sequence of real numbers whose least upper bound gives us enough information to construct the same set using Δ⁰₁ comprehension relative to the least upper bound.

To do this, we use the predicate ∃m<k(θ(m,n)) which is Σ⁰₀. For each $k$ let $x_k = \sum_{i \in A_k} 2^{-i}$ , where $A_k = \{ i \mid \exists m < k \theta(m,i)\}$ . The sequence $\langle x_k \rangle$ can be formed in $\mathsf{RCA}_0$ , is nondecreasing, and is bounded above by 1. By Bolzano-Weierstraß, there is a least upper bound for the sequence. Under the assumption that the set $A = \{i \mid \exists m \theta(m,i)\}$ exists, $\mathsf{RCA}_0$ is able to prove that the least upper bound is equal to $\sum_{i \in A} 2^{-i}$ . Our goal is to show that the set $A$ actually exists. $\mathsf{RCA}_0$ proves that the least upper bound has a binary expansion. If the least upper bound has a nonunique binary expansion, this means that $A$ is either finite or cofinite, in which case it is trivial to prove that $A$ exists. We may thus assume that the binary expansion is unique (it cannot end with infinitely many 1's). It follows that we can use Δ⁰₁ comprehension relative to the binary expansion of the least upper bound to form the set $A$ , completes the proof.

[edit] References

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.
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 [1]).
Reed Solomon. "Ordered Groups: A Case Study in Reverse Mathematics". The Bulletin of Symbolic Logic, v. 5 n. 1 (Mar., 1999), pp. 45-58.

[edit] External links

Retrieved from "http://en.wikipedia.org../../../r/e/v/Reverse_mathematics.html"

Categories: Mathematical logic | Recursion theory | Proof theory

Reverse mathematics

From Wikipedia, the free encyclopedia

Contents

[edit] General principles

[edit] Subsystems of second order arithmetic

[edit] The base system

[edit] Weak König's lemma

[edit] Arithmetical comprehension

[edit] Arithmetical Transfinite Recursion

[edit] Π¹₁ comprehension

[edit] Additional systems

[edit] An example of a reverse mathematics proof

[edit] References

[edit] External links

Views

Navigation

Search

In other languages

Reverse mathematics

From Wikipedia, the free encyclopedia

Contents

[edit] General principles

[edit] Subsystems of second order arithmetic

[edit] The base system

[edit] Weak König's lemma

[edit] Arithmetical comprehension

[edit] Arithmetical Transfinite Recursion

[edit] Π11 comprehension

[edit] Additional systems

[edit] An example of a reverse mathematics proof

[edit] References

[edit] External links

Views

Navigation

Search

In other languages

[edit] Π¹₁ comprehension