Lógos and Máthma 2. Roman Murawski

Скачать книгу

mathematics of Friedman and Simpson contributes to it, providing us with a partial realization of Hilbert’s original program.

To be able to consider the issue we should first specify what is exactly meant by finitistic mathematics and by real sentences. We shall follow Tait (1981) where it is claimed that Hilbert’s finitism is captured by the formal system of primitive recursive arithmetic7 (PRA, also called Skolem arithmetic). By real sentences we shall mean Πsentences of the language of Peano arithmetic PA.

It turns out that one can formalize classical mathematics not only in set theory, but most of its parts (such as geometry, number theory, analysis, differential equations, complex analysis, etc.) can be formalized in a weaker system called second order arithmetic (denoted also sometimes by Z2).8 This is a system formalized in a language with two sorts of variables: number variables x, y, z, . . . and set variables X,Y,Z, . . . Its nonlogical constants are those of Peano arithmetic PA, i.e., o,S,+,⋅ and the membership relation ∈. Nonlogical axioms of are the following:

      1 axioms of PA without the axiom scheme of induction,

      2 (extensionality)

      3 (induction 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),

Скачать книгу