Lógos and Máthma 2. Roman Murawski

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