Reverse mathematics

From Free net encyclopedia

Reverse mathematics is a program in mathematical logic which seeks to determine which axioms are required to prove theorems of classical mathematics. The method could 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. For example, it is well known that the axiom of choice and Zorn's lemma are equivalent over ZF set theory. The goal of reverse mathematics is to study theorems of classical mathematics, however, not 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 published abstracts Systems of second order arithmetic with restricted induction I and II. It was pursued, among other people, by Stephen G. Simpson and his students. Simpson wrote the primary reference book on the subject, Subsystems of Second Order Arithmetic. which was published in 1999. See references for details of these references.

Contents 1 Principles 1.1 Generalities 1.2 Choice of the language and base system 1.3 Second-order arithmetic 2 The main systems 2.1 The base system 2.2 Weak König's lemma 2.3 Arithmetical comprehension 2.4 Arithmetical Transfinite Recursion 2.5 Π11 comprehension 2.6 Some further systems 3 An example of a reverse mathematics proof 4 References

Principles

Generalities

The principle of reverse mathematics is the following: one starts with a framework language and a base theory—a core (axiom) system—which is too weak to prove most of the theorems one might be interested in, but still powerful enough to prove correct 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. To so this, one first proves the theorem from the axiom system — an ordinary mathematical proof — and then one proves in the base system that the theorem implies the axiom system. This shows that no weaker axiom system can prove the theorem, because any second axiom system which implies the theorem implies the first axiom system.

Choice of the language and base system

If the base system is chosen too strong (as an extreme case, take it to be full Zermelo-Fraenkel set theory with the axiom of choice), then reverse mathematics is uninformative: many theorems (of the full system, that is, usual mathematical theorems) will actually be theorems of this core system, so they are all equivalent and we learn nothing about their strength. If the base system is chosen too weak (as an extreme case, take it to be mere predicate calculus), then the equivalence relation between theorems is overfussy: nothing is ever equivalent to anything except when it is trivially so, and we also learn nothing. There is also the question of how to choose the framework language: it should be sufficient to express usual mathematical ideas without too much translation, yet it should not presuppose strong axioms otherwise we again run into the trouble of the core system being too strong.

For example, while usual (forward) mathematics is done in the language of set theory and in the system of Zermelo-Fraenkel set theory with the axiom of choice (which, unless the contrary is explicitly stated, is assumed to be the foundation system taken for granted by working mathematicians), this system is really much stronger than is necessary. Reverse mathematics uses subsystems of second-order arithmetic, which are much weaker than set theory. Experience shows that this choice produces interesting results. In particular, there is no well known theorem of the undergraduate analysis or algebra that is not equivalent to one of five particular subsystems of second-order arithmetic. This is remarkable because essentially the entire undergraduate curriculum in analysis and algebra has been studied.

Second-order arithmetic

This subsection gives a brief summary of the main article on second-order arithmetic.

In reverse mathematics, the framework language is taken to be that of second-order arithmetic and the core theory (or base system) is taken to be <math>\mathsf{RCA}_0</math>.

The language of second-order arithmetic has a constant 0, a unary function S (the successor function) the binary operations + and · (addition and multiplication), binary relations < and ∈ (membership), and has two types of variables, first-order ones corresponding to natural numbers, and second-order ones corresponding to subsets of natural numbers. Terms and formulas are formed in the usual way. The axioms are the basic axioms of Robinson arithmetic (giving the "usual" properties of +, × <), induction axioms, and comprehension axioms (saying roughly that for every formula there is a subset consisting of exactly numbers satisfying the formula).

The article on second-order arithmetic describes the following subsystems in more detail:

• Robinson arithmetic, or the basic axioms: "usual" rules for +, ×, no induction or comprehension.
• First-order Peano arithmetic: Robinson arithmetic plus induction for all first-order formulas.
• <math>\mathsf{RCA}_0</math>: the basic axioms, plus the Σ₁ induction scheme and Δ₁ comprehension.
• <math>\mathsf{ACA}_0</math>: the basic axioms, plus the arithmetical comprehension axiom scheme, in other words the comprehension axiom for every arithmetical formula φ, and the ordinary second-order induction axiom.
• <math>\Pi^1_1\mathrm{-CA}_0</math> is the system consisting of the basic axioms, plus the ordinary second-order induction axiom and the comprehension axiom for every Π₁¹ formula φ.

The main systems

We now attempt to describe in a nontechnical manner (and thus perhaps slightly imprecisely) the five main formal systems of reverse mathematics. In increasing order of strength, these systems are: <math>\mathsf{RCA}_0</math> (the base system), <math>\mathsf{WKL}_0</math>, <math>\mathsf{ACA}_0</math>, <math>\mathsf{ATR}_0</math>, and <math>\Pi^1_1\mathrm{-CA}_0</math>.

The base system

<math>\mathsf{RCA}_0</math> is our base system. Our goal is thus to take specific theorems of classical mathematics and show that these theorems are either provable in <math>\mathsf{RCA}_0</math> or equivalent to one of the other systems.

Intuitively, <math>\mathsf{RCA}_0</math> is a constructuve system, although it does not meet the requirements of the program of constructivism (see constructivist). In particular, any set which can be proven to exist in <math>\mathsf{RCA}_0</math> is computable. Thus any theorem which implies that noncomputable sets exist is not provable in <math>\mathsf{RCA}_0</math>.

Despite its seeming weakness, recursive comprehension is still sufficient to prove a number of classical results which are, therefore, “core mathematical statements” requiring only minimal logical strength (and, in a sense, below the reach of the reverse mathematics enterprise). Let us state:

• Basic properties of the natural numbers, integers, and rational numbers (for example, 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 have an intersection point, and consequently the real numbers are uncountable).
• The Baire category theorem in a complete separable metric space (the separability condition is necessary to even code 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 recursive comprehension (in other words, theorems of the system which do not involve any class variables) is the set of theorems of first-order Peano arithmetic with induction limited to Σ₁ formulae. It is provably consistent, and so is recursive comprehension, in the full first-order Peano arithmetic.

Weak König's lemma

To from the subsystem <math>\mathsf{WKL}_0</math>, we add to <math>\mathsf{RCA}_0</math> 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. <math>\mathsf{WKL}_0</math> can also be defined as the principle of Σ⁰₁ separation (given two Σ⁰₁ formulae of a free variable n which are exclusive, there is a class containing all n satisfying the one but none of the other).

The following remark on notation 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 <math>\mathsf{RCA}_0</math>, the resulting subsystem is called <math>\mathsf{WKL}_0</math>. 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). At any rate, it is not constructively valid in some senses of the word constructive.

To see that <math>\mathsf{WKL}_0</math> is actually stronger than (not provable in) <math>\mathsf{RCA}_0</math>, it is sufficient to exhibit a theorem of <math>\mathsf{WKL}_0</math> which implies that noncomputable sets exist. This is not difficult; c <math>\mathsf{WKL}_0</math> implies the existence of separating sets for effectively inseparable r.e. sets.

It turns out, however, that <math>\mathsf{RCA}_0</math> and <math>\mathsf{WKL}_0</math> have the same first-order part. But weak König's lemma is useful for proving a good number of classical mathematical results which do not follow from <math>\mathsf{RCA}_0</math>.

The following results are equivalent, over <math>\mathsf{RCA}_0</math>, to weak König's lemma and thus to <math>\mathsf{WKL}_0</math>:

• 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).

Arithmetical comprehension

<math>\mathsf{ACA}_0</math> is <math>\mathsf{RCA}_0</math> 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). Actually, it suffices to add to <math>\mathsf{RCA}_0</math> the comprehension scheme for Σ₁ formulas in order to obtain full arithmetical comprehension.

The first-order part of <math>\mathsf{ACA}_0</math> turns out to be exactly first-order Peano arithmetic: one says that arithmetical comprehension is a conservative extension of first-order Peano arithmetic. It is provably (in a weak system) equiconsistent with it. <math>\mathsf{ACA}_0</math> can be thought of as the framework of predicative mathematics, although there are predicatively provable theorems that are not provable in <math>\mathsf{ACA}_0</math>. Seemingly every natural arithmetical result, and many other mathematical theorems, can be proven in this system.

As for reverse mathematics, the following assertions are equivalent, over <math>\mathsf{RCA}_0</math>, to <math>\mathsf{RCA}_0</math>:

• 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.
• The full König's lemma (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 <math>\mathsf{ATR}_0</math> is, loosely speaking, the statement that an 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 decreasing sequence) starting with any set. It can also be defined as the principle of Σ¹₁ separation. Although <math>{ATR}_0</math> is impredicative, it has the same proof-theretic ordinal <math>\Gamma_0</math> as predicative systems.

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

The following assertions are equivalent, over <math>\mathsf{RCA}_0</math>, to <math>\mathsf{ATR}_0</math>:

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

Π¹₁ comprehension

<math>\Pi^1_1\mathsf{-CA}_0</math> is stronger than arithmetical transfinite recursion, and it is fully impredicative. It consists of <math>\mathsf{RCA}_0</math> plus the comprehension scheme for <math>\Pi^1_1</math> formulas.

In a sense, <math>\Pi^1_1\mathsf{-CA}_0</math> comprehension is to arithmetical transfinite recursion (Σ¹₁ separation) as <math>\mathsf{ACA}_0</math> is to weak König's lemma (Σ⁰₁ separation). It is essentially equivalent to statements of descriptive set theory that make use of strongly imprecative arguments.

Among the theorems of classical analysis equivalent, over recursive comprehension, to <math>\Pi^1_1\mathsf{-CA}_0</math>, let us mention:

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

Some further 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) can be shown to be equivalent to the statement that a polynomial (over a countable field) has only finitely many roots, or 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 tee 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). It is equivalent, for example, 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

<math>{RCA}_0</math> is closely connected to the theory of random real numbers. In particular, an ω-model of <math>\mathsf{RCA}_0</math> satisfies weak weak Konig's lemma if and only if for every set X there is a set Y which is one-random relative to X.

• Δ¹₁-comprehension is in certain ways 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 (over arithmetical comprehension) the statement that if η is a Σ¹₁ property of a natural number n and a class X (or real number, perhaps) such that for each n there exists X satisfying η then there is a sequence (of classes, or real numbers) satisfying the property. Σ¹₁-choice also has the hyperarithmetical sets as minimal ω-model. Arithmetical transfinite recursion proves Σ¹₁-choice but not the other way around.

An example of a reverse mathematics proof

As an example of the theory, let us sketch the proof of the fact that the Bolzano-Weierstraß theorem (in the form: every bounded sequence of real numbers has a convergent subsequence) is equivalent over recursive comprehension to arithmetical comprehension. We define a “real number” to be a sequence of rationals such that the difference between the n-th and (n + 1) -th terms is 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.

(Note: 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. But the tree consisting of those binary intervals containing an element of the sequence requires arithmetical comprehension to define.)

For the reverse, the idea is as follows: to prove arithmetical comprehension it is actually sufficient to prove Σ₁ comprehension (because that allows us to remove a quantifier, and we then use induction on the number of quantifiers since we can certainly pass to the complement). Now this means essentially that given a Δ₀ predicate θ(m,n) we need to prove comprehension for the predicate ∃m(θ(m,n)). But we can at least form the predicate ∃m<k(θ(m,n)) for all k. Considering this as the binary (or perhaps ternary, to avoid problems with non-uniqueness of binary expansions) expansion (letting n vary) for a real number x_k between 0 and 1 (our definition of real numbers is essentially by binary expansion), we get a nondecreasing bounded sequence which, by Bolzano-Weierstraß, converges to some real number x_∞ whose binary expansion is exactly the desired predicate ∃m(θ(m,n)). This suffices for what we want.

References

• Harvey Friedman's home page
• Proceedings of the International Congress of Mathematicians (Vancouver, B.C., 1974), Vol. 1, pp. 235–242. Canad. Math. Congress, Montreal, Que., 1975.
• Stephen G. Simpson's home page
• Subsystems of Second Order Arithmetic. Perspectives in Mathematical Logic, Springer-Verlag, Berlin, 1999. ISBN 3-540-64882-8 (out of print, first chapter available at http://www.math.psu.edu/simpson/).fr:Mathématiques à rebours

it:Matematica inversa tr:Tersine matematik zh:逆数学