Lógos and Máthma 2. Roman Murawski

axiom)

      4 (axiom scheme of comprehension) where φ(x, . . .) is any formula of the language (possiblywith free number-or set-variables) in which X does not occur free.

      Possible models of are structures of the form (X ,M,∈) where Mis a model of PA and X is a family of subsets of the universe of the model M. (More information on and its models can be found in Apt, Marek (1974), and Murawski (1976–1977, 1984a).)

Second order arithmetic is a nice system because one avoids here troubles connected with set theory (in which mathematics is usually formalized), and on the other hand it is strong enough to provemany important theorems of classical mathematics. There is only a problem of impredicativity9 of (connected with the axiom scheme of comprehension, where φ may be any formula of the language of ←16 | 17→hence in particular φ may be of the form ∀Yψ(Y, x, . . .)). But it turns out that in many cases certain fragments of suffice, i.e., only particular special forms of the comprehension axiom are needed.

At the Congress of Mathematicians in Vancouver in 1974 H.Friedman formulated a program of foundations of mathematics called today “reversemathematics” (cf. Friedman 1975). Its aim is to study the role of set existence axioms, i.e., comprehension axioms in ordinary mathematics. The main problem is: Given a specific theorem τ of ordinary mathematics, which set existence axioms are needed in order to prove τ? This research program turned out to be very fruitful and led to many interesting results.10

      The procedure used in the reverse mathematics (it reveals the inspiration for its name) is the following: Assume we know that a given theorem τ can be proved in a particular fragment S(τ) of Is S(τ) the weakest fragment with this property? To answer this question positively, one shows that the principal set existence axiom of S(τ) is equivalent to τ, the equivalence being provable in some weaker system in which τ itself is not provable. Thus reverse mathematics is, from the point of view of the philosophy of mathematics, an example of a reductionist program with a firm mathematical basis.

      Some specific systems – fragments of – arose in this context; the most important are: RCA0,WKL0, ACA0, ATRo and −CA.We shall describe only the first three of them.

The system RCA0 is a theory in the language of based on the following axioms: (i) PA− (i.e., axioms of Peano arithmetic PA without the axiom scheme of induction), (ii) scheme of induction for formulas,11 i.e.:

      where φ is a formula, (iii) (recursive comprehension axiom)

      where φ is and ψ is [Axiom (iii) explains the name RCA0 of the theory.] It can be shown that (Rec,N,∈), where No is the standard model of Peano arithmetic PA and Rec is the family of all recursive sets, is a model of RCA0.

      The theory WKL0 consists of RCA0 plus a further axiom known as weak König’s lemma (therefore the name WKL0) which states that every infinite binary tree has an infinite path (this can be formulated in the language of using coding). It is ←17 | 18→stronger than RCA0 what follows, e.g. from the fact that (Rec,N,∈) is not a model of WKL0 (this is a consequence of Gödel’s theorem on essential undecidability of Peano arithmetic).

      The theory ACA0 is PA− plus induction axiom plus arithmetical comprehension, i.e., comprehension scheme for any arithmetical formula (possibly containing set parameters). This theory is not weaker than WKL0 because it proves weak König’s lemma. It is in fact stronger than WKL0 what follows from the fact that there are models of WKL0 consisting of sets definable in No by formulas of a given class (e.g. the family of definable sets), whereas for any model (X ,N,∈) of ACA0 the family X must be closed with respect to arithmetical definability.

      The specified subsystems of are appropriate for particular parts of classical mathematics. In RCA0 one can construct reals, define notions of the convergence of a sequence, of a continuous function, of Riemann’s integrability, etc. and prove positive results of recursive analysis and recursive algebra. For example one can prove in RCA0 that every countable field has an algebraic closure, that every countable ordered field has an extension to a real closed field as well as the intermediate value theorem for continuous functions (cf. Simpson 1998).

      The theory WKL0 turns out to be a quite strong theory, in particular one can prove in it the following theorems:

      –the Heine–Borel covering theorem (every covering of [0,1] by a countable sequence of open intervals has a finite subcovering) (cf. Friedman 1976),

      –every continuous function on [0,1] is uniformly continuous (cf. Simpson 1998),

      –every continuous function on [0,1] is bounded (cf. Simpson 1998),

      –every continuous function on [0,1] has a supremum (cf. Simpson 1998),

      –every uniformly continuous function on [0,1], which has a supremum, attains it (cf. Simpson 1998),

      –every continuous function on [0,1] attains a maximum value (cf. Simpson 1998),

      –the Hahn–Banach theorem (cf. Brown, Simpson 1986 and Brown 1987),

      –the Cauchy–Peano theorem on the existence of solutions of ordinary differential equations (cf. Simpson 1984),

      –every countable commutative ring has a prime ideal (cf. Friedman, Simpson, Smith 1983),

      –every countable formally real field can be ordered (cf. Friedman, Simpson, Smith 1983),

      –every countable formally real field has a real closure (cf. Friedman, Simpson, Smith 1983),

      –Gödel’s completeness theorem for the predicate calculus (cf. Friedman 1976 and Simpson 1998).

      ←18 | 19→

      Even more: if S is one of the above stated theorems then RCA0 + S is equivalent to WKL0.

      To indicate the strength of ACA0 let us mention that the following theorems can be proved in it:

      –the Bolzano–Weierstrass theorem(every bounded sequence of real numbers has a convergent subsequence) (cf. Friedman 1976),

      –every Cauchy sequence of reals is convergent (cf. Simpson 1998),

      –every bounded sequence of reals has a supremum (cf.