Lógos and Máthma 2. Roman Murawski

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

[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

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