Читать книгу Lógos and Máthma 2 - Roman Murawski - Страница 14

Another consequence of incompleteness results (besides those described above) is so-called relativized Hilbert’s program. If the entire infinitistic mathematics cannot be reduced to and justified by finitistic mathematics then one can ask for which part of it is that possible? In other words:Howmuch of infinitistic mathematics can ←15 | 16→be developed within formal systems which are conservative over finitistic mathematics with respect to real sentences? This constitutes the relativized version of Hilbert’s program. In what follows, we would like to show how the so-called reverse 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),

–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. Friedman 1976),

–every bounded increasing sequence of real numbers is convergent (cf. Friedman 1976),

–the Arzela–Ascoli lemma (any bounded equicontinuous sequence of functions on [0,1] has a uniformly convergent subsequence) (cf. Simpson 1998),

–every countable vector space has a basis (cf. Friedman, Simpson, Smith 1983),

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

–every countable Abelian group has a unique divisible closure (cf. Friedman, Simpson, Smith 1983).

And again, if S is any of those theorems then RCA0 + S is equivalent to ACA0.

What is the meaning of those results? First of all they indicate how much of we need in fact to prove various particular theorems of classical mathematics. And it is interesting from the philosophical point of view that certain particular fragments of (described above) turn out to be adequate with respect to ordinary mathematical practice. But note that proofs (in the formalized subsystems of the second order arithmetic) of uniqueness are usually more difficult and more complicated than proofs of the existence (in mathematical practice the former are usually simple consequences of the latter). There is also no direct connection between the complexity of a classical proof of a theorem and the level in the hierarchy of subsystems of in which a formalized version of it can be proved (as an example can serve here the theorem that every Abelian group has a torsion subgroup which is trivial in classical algebra but RCA0 + this theorem is equivalent to ACA0 hence is not a theorem of, say, WKL0).

In mathematical practice, we encounter often the following situation: Assume that certain theorem τ can be proved in set theory. The natural question is now: Can τ be proved in an elementary way? Observe that if τ can be classified in the hierarchy of subsystems of Aat a level higher than RCA0 then the answer is negative, i.e., an abstract, infinitistic proof of τ is indispensable and necessary.

Results of reverse mathematics have also interesting mathematical, and not only logical, applications. As an example can serve here Cauchy–Peano theorem on the existence of solutions of ordinary differential equations. Since it is equivalent to WKL0 over RCA0 and since the structure (No,Rec,∈) is not a model of WKL0,←19 | 20→we get that there exists a differential equation y ′ = f (x, y), where f is a recursive continuous function, such that it has no recursive solution.

Observe that not every mathematical theorem can be classified in Friedman’s hierarchy of subsystems of As an example one can give here Hilbert’s basis theorem (cf. Simpson 1988) which states that for any field K and any natural number n all ideals in the ring K [x1, . . . , xn] can be finitely generated. This theorem is provable in ACA0 but RCA0 + “Hilbert’s basis theorem” is not equivalent to any of the considered systems.12

Add also that there are sentences which are unprovable in the full system of second order arithmetic but can be proved in Zermelo-Fraenkel set theory (cf. Friedman 1981).

To indicate the connections of reverse mathematics with Hilbert’s program we must recall some results. In the early 1980s, L.Harrington and Z.Ratajczyk proved a theorem on conservativeness of WKL0 (none of the mpublished it; the proof can be found in Simpson 1998).

Theorem 1 If (X ,M,∈) is a countable model of RCA0 and A ∈X then there exists a family Y ⊆P(M) such that A∈Y and (Y,M,∈) is a model of WKL0.

Corollary 2 The theory WKL0 is conservative over RCA0 with respect to sentences, i.e., every sentence provable in WKL0 can be proved in RCA0.

What more, Friedman proved in 1977 (this result was not published; it can be found also in Kirby, Paris 1977) that WKL0 is a conservative extension of Skolem arithmetic PRA with respect to sentences. His proof used model-theoretical methods. W. Sieg improved this result, giving an alternative proof which uses Gentzen-style methods and exhibiting a primitive recursive proof tranformation. Hence the reducibility of WKL0 to PRA is itself provable in PRA.

Combining those results together with the fact that WKL0 is a fairly strong theory (what was indicated above) one comes to the conclusion that a large and significant part of classical mathematics is finitistically reducible. This means in fact that Hilbert’s program can be partially realized!

Add that all this has also some “practical” consequences. First observe that the class of sentences is rather broad – many theorems of number theory can be formulated as sentences belonging to that class. Since one can formalize within ←20 | 21→WKL0 the technique of contour integration, hence any number–theoretic theorem which is provable with the help of it can also be proved “elementarily”, i.e., within PRA and, even more, one can effectively (at least theoretically) find such an “elementary” proof. To give one more example, consider Artin’s theorem (being a solution to Hilbert’s 17th problem13). It can be written as a sentence. Since all results of the theory of real closed fields needed in the proof of Artin’s theorem are provable in WKL0, it follows by Friedman’s and Sieg’s theorems that Artin’s theorem can be proved in PRA, i.e., in an elementary way.

It seems that Hilbert would be satisfied by such results!

←21 | 22→

1 Detlefsen (1990, p. 374) writes that “Hilbert did want to preserve classical mathematics, but this was not for him an end in itself. What he valued in classical mathematics was its efficiency (including its psychological naturalness) as a means of locating the truth of real or finitary mathematics. Hence, any alternative to classical mathematics having the same benefits would presumably have been equally welcome to Hilbert”.

2 ,,Schon Kant hat gelehrt – und zwar bildet dies einen integrierenden Bestandteil seiner Lehre –, dass die Mathematik über einen unabhängig von aller Logik gesicherten Inhalt verfügt und daher nie und nimmer allein durch Logik begründet werden kann, weshalb auch die Bestrebungen von Frege und Dedekind scheitern mußten. Vielmehr ist als Vorbedingung für die Anwendung logischer Schlüsse und für die Betätigung logischer Operationen schon etwas in der Vorstellung gegeben: gewisse, außer-logische konkrete Objekte, die anschaulich als unmittelbares Erlebnis vor allem Denken da sind. Soll das logische Schließen sicher sein, so müssen sich diese Objekte vollkommen in allen Teilen überblicken lassen und ihre Aufweisung, ihre Unterscheidung, ihr Aufeinanderfolgen oder Nebeneinandergereihtsein ist mit den Objekten zugleich unmittelbar anschaulich gegeben als etwas, das sich nicht noch auf etwas anderes reduzieren läßt oder einer Reduktion bedarf. Dies ist die philosophische Grundeinstellung, die ich für die Mathematik wie überhaupt zu allem wissenschaftlichen Denken, Verstehen und Mitteilen für erforderlich halte. Und insbesondere in der Mathematik sind Gegenstand unserer Betrachtung die konkreten Zeichen selbst, deren Gestalt unserer Einstellung zufolge unmittelbar deutlich und wiedererkennbar ist”.

3 In some of Hilbert’s publications (cf., e.g. Hilbert 1926, 1927) both aspects are stressed but usually (cf. Hilbert and Bernays 1934–1939) the one-sided emphasis is put on the consistency problem.

4 Both those aspects are interconnected – as was indicated by G. Kreisel. He showed that if φ is a sentence and T ⊢ φ (where T is an infinitistic theory) then S + ConT ⊢ φ (where S is a finitistic theory and ConT is a sentence stating that T is consistent) (cf., e. g. Smoryński 1977). Hence, identifying real sentences with Πsentences we see that a solution to the consistency problem yields a solution to the conservation problem.

5 Hilbert rejected the opinion that Gödel’s results showed the non-executability of his programme. He claimed that they have shown “only that for more advanced consistency proofs one must use the finitistic standpoint in a deeper way than is necessary for the consideration of elementary formalisms” (cf. Hilbert and Bernays 1934–1939, vol. I). Gödel wrote in (1931) that “Theorem XI [i.e. Gödel’s second theorem for arithmetic P where P denotes the arithmetic of Peano extended by simple type theory – my remark, R.M.] (and the corresponding results for M and A) [where M is the set theory and A is the analysis – my remark, R.M.] do not contradict Hilbert’s formalistic viewpoint. For this viewpoint presupposes only the existence of a consistency proof in which nothing but finitary means of proof is used, and it is conceivable that there exist finitary proofs that cannot be expressed in the formalism of P (or Mor A)”.

6 It seems that Bernays was among the first who recognized this need. He wrote: “It thus became apparent that the ‘finite Standpunkt’ is not the only alternative to classical ways of reasoning and is not necessary implied by the idea of proof theory. An enlarging of the methods of proof theory was therefore suggested: instead of a restriction to finitist methods of reasoning, it was required only that the arguments be of a constructive character, allowing us to deal with more general forms of inference” (cf. Bernays 1967, p. 502).

7 For the description of PRA see, e.g. Smoryński (1977).

8 This was first observed by Hilbert and Bernays. Weyl (1918) had shown that a substantial part of ordinary mathematics can be developed within a certain “predicative” subsystem of Z2 (allowing ω-iterated arithmetical definability).

9 Recall that H. Poincaré saw the source of antinomies in mathematics just in impredicativity and therefore demanded a restriction to predicative methods only.

10 Drake claims even that the implications of the results of reverse mathematics “make much of what was written in the past on the philosophy of mathematics, obsolete” (cf. Drake 1989).

11 For the definition of and basic information on the arithmetical and analytical hierarchies of formulas and relations see, e.g. Shoenfield (1967).

12 Denote by WO(α) the sentence stating that the ordinal α is a well-ordered set. One can prove in RCA0 that WO(ωω) is equivalent to Hilbert’s basis theorem. But the sentence WO (ωω) is incomparable with WKL0.On the other hand, for any given natural number n one can prove in RCA0 that WO(ωn) is equivalent to Hilbert’s basis theorem for n. What more, WO(ωn) is provable in RCA0. So we have here certain analogy with the ω–incompleteness of Peano arithmetic (cf. Gödel 1931, see also Mendelson 1970).

13 Hilbert asked in his 17th problem “whether every definite form [of any number of variables with real coefficients – my remark, R.M.] may not be expressed as a quotient of sums of squares of forms” (cf. Hilbert 1901, see also Browder 1976). Recall that a form is called “definite” if it becomes negative for no real values of the variables. In 1926, Artin answered this question positively.