M Schrin Finitist point of view

Extensions of the Finitist Point of View

ATTHIAS

CHIRN

and K

ARL

-G

EORG

IEBERGALL

UniversitaÈt MuÈnchen, Seminar fuÈr Philosophie, Logik und Wissenschaftstheorie, Ludwigstr. 31, 80539

MuÈnchen, Germany

Revised 5 April 2002

Hilbert developed his famous ®nitist point of view in several essays in the 1920s. In this paper, we discuss
various extensions of it, with particular emphasis on those suggested by Hilbert and Bernays in
Grundlagen der Mathematik (vol. I 1934, vol. II 1939). The paper is in three sections. The ®rst deals with
Hilbert’s introduction of a restricted

o-rule in his 1931 paper `Die Grundlegung der elementaren

Zahlenlehre’. The main question we discuss here is whether the ®nitist (meta-)mathematician would be
entitled to accept this rule as a ®nitary rule of inference. In the second section, we assess the strength of
®nitist metamathematics in Hilbert and Bernays 1934. The third and ®nal section is devoted to the second
volume of Grundlage n der Mathematik. For preparatory reasons, we ®rst discuss Gentzen’s proposal of
expanding the range of what can be admitted as ®nitary in his esssay `Die Widerspruchsfreiheit der reinen
Zahlentheorie’ (1936). As to Hilbert and Bernays 1939, we end on a `critical’ note: however considerable
the impact of this work may have been on subsequent developments in metamathematics, there can be no
doubt that in it the ideals of Hilbert’s original ®nitism have fallen victim to sheer proof-theoretic pragmatism.

In the 1920s, David Hilbert developed his ®nitist metamathematics qua contentual

theory of formalized proofs to defend all of classical mathematics. On the one hand,
Russell’s and Zermelo’s discovery of the set-theoretic paradoxes shook the logical
foundations of number theory and analysis. On the other hand, Brouwer and Weyl
had mounted a serious attack on classical analysis, especially on the (alleged) validity
of the law of excluded middle. Hilbert felt that he had to meet this twofold challenge
by establishing metamathematicall y and in a purely ®nitist fashion the consistency of
classical mathematics. The central idea underlying metamathematical consistency
proofs was to show the consistency of formalized mathematical theories T by means
of `weaker’ and more reliable methods than those that could be formalized in T.

It was in the light of GoÈdel’s Incompleteness Theorems that ®nitist

metamathematic s turned out to be too weak to lay the foundations for a signi®cant
portion of classical mathematics. Hilbert and his collaborators , notably Bernays,
responded by extending the original ®nitist point of view. The envisaged extension
was guided by two central, though possibly con¯icting ideas: ®rst, to make sure
that it preserved the essentials of ®nitist metamathematics ; second, to conduct
indeed, within the extended proof-theoretic bounds, a consistency proof for a large
part of mathematics, in particular for second-order arithmetic (Z

We may characterize the nature of Hilbert’s ®nitist metamathematics of the 1920s

(henceforth referred to as `M’) in a few words as follows:

(1) M is a non-formalized and non-axiomatized `theory’ with a non-mathematica l

vocabulary.

*With the exception of Hilbert (1928a) and (1928b) the translations of Hilbert’s writings are our own. For
the most part, we have slightly modi®ed the existing translations. As to the translation of the word
`inhaltlich’, we have adopted the neologism `contentual’, coined by the translator of Hilbert 1926, Stefan
Bauer-Mengelberg. The references to the English translations of Hilbert (1926) and (1928a) appear in
square brackets.

HISTORY AND PHILOSOPHY OF LOGIC, 22 (2001), 135±161

History & Philosophy of Logic ISSN 0144-5340 print/ISSN 1464-5149 online # 2002 Taylor & Francis Ltd

http://www/tandf/co/uk/journals/tf/01445340.html

DOI: 10.1080/01445340210154295

(2) Both M and its formal version MM contain only true sentences.

(3) Neither M nor MM need be recursively enumerable.
(4) Unbounded universal quanti®cations cannot be formulated in the language L

M, nor can genuine

-sentences or

-formulae be formulated in the language

of MM.

(5) MM is possibly much weaker than Primitive Recursive Arithmetic (PRA).

To avoid misunderstandings , a few remarks are in order here. We are aware that

some if not most people working on Hilbert’s programme and related topics will
probably not agree with our way of characterizing his pre-GoÈdelian conception of
metamathematics . To be sure, all but one of our ®ve theses are denials of standard
assumptions made by researchers in this ®eld. However, our non-standard
approach is by no means due to mania for innovation, cost what it may. On the
contrary, in our paper `Hilbert’s ®nitism and the notion of in®nity’ (see Niebergall
and Schirn 1998) we attempt to argue in some detail for the plausibility of the
theses (1)±(5) by paying close attention to Hilbert’s texts. We wish to make one
proviso, though. On the one hand, Hilbert’s classical papers on proof theory
between 1922 and 1928 are not free from ambiguity and vagueness. On the other
hand, it goes without saying that they were not written from the point of view of
modern metalogical considerations . We therefore concede that the theses (1)±(5)
cannot be attributed to Hilbert with absolute certainty.

In any case, it seems to us that some of our fellow researchers still tend to regard

Hilbert’s early proof theory from the point of view of later developments in
metamathematics , beginning in the 1930s. However, to the best of our knowledge, so
far no one has furnished conclusive textual evidence that in the 1920s Hilbert held
the denial of any of the theses (1), (3), (4) and (5), let alone the denials of all of them.
And we believe that such evidence is not forthcoming. The question whether the
conception of metamathematic s characterized above is a coherent and an intelligible
one, is another matter. To ®nd it incoherent or unintelligible is certainly no
compelling reason to claim that it cannot have been in the spirit of Hilbert.

The core of this paper is a critical discussion of the extensions of the ®nitist point

of view that Hilbert and Bernays suggest in Grundlagen der Mathematik (Vol. I 1934,
Vol. II 1939). This monumental work has largely been ignored in discussions of
Hilbert’s ®nitist standpoint. To gain a complete picture of the facets of Hilbert’s
®nitism, this gap needs to be ®lled. We venture to do this in

}2 and 3 of this paper.

}1, we canvass Hilbert’s introduction of a restricted o-rule in his 1931 paper

`Die Grundlegung der elementaren Zahlenlehre’. Hilbert uses this rule to achieve an
extension of PA and quali®es it expressly as ®nitary. The main question we focus
on here is whether the ®nitist (meta-)mathematicia n would be justi®ed in accepting
this rule as a ®nitary mode of inference. In the second section, we are especially
interested in ®guring out to what extent Hilbert’s ®nitist perspective of 1934 tallies
with or deviates from his approach in the 1920s. We argue that ®nitist
metamathematic s in Hilbert and Bernays 1934 is at least as strong as PRA, and
may include even PRA+Con

pra

. The third and ®nal section provides ®rst a brief

account of Gentzen’s consistency proof for Peano Arithmetic (PA) in his 1936

MM results from couching M in a formal language.

We argue for this claim in Niebergall and Schirn (1998) and in `Finitism=PRA? On a thesis of W.W.

Tait’ (forthcoming). For a detailed description of the nature of M see Niebergall and Schirn 1998.

136

Matthias Schirn and Karl-Georg Niebergall

paper `Die Widerspruchsfreiheit der reinen Zahlentheorie’, followed by a few
comments on his suggestion of extending the scope of permissible ®nitary (or
constructive) methods in metamathematics . Gentzen’s approach proves to be
important when we come to consider more closely the post-GoÈdelian fate of
®nitism in Hilbert and Bernays 1939.

One essential point argued for is that in

Hilbert and Bernays 1939 the canons of M, such as its informal character, its
intuitive evidence, and its unquestionable soundness, are thrown overboard.

Hilbert (1931) and the

o-rule

Restricted versions of the

o-rule have been suggested both as a means of

explicating certain forms of ®nitary arguments or proofs and as a way of correctly
extending a theory already accepted. In this section, we want to deal with the
question as to whether weak versions of the

o-rule can be regarded as ®nitary. For

if they can, they may prove useful for the construction of metamathematica l
theories that clash neither with Hilbert’s programme nor with GoÈdel’s
Incompleteness Theorems. In pursuing our aim, we align ourselves with most
authors who discuss the

o-rule in connection with Hilbert’s programme.

contrast, in his 1931 essay Hilbert himself introduces a restricted

o-rule as a means

of extending PA, though he does so in a way which admits different interpretations.

Rule

o*: When it is shown that the formula A(~z) is a correct numerical formula for

each particular numeral ~z, then the formula 8xA(x) can be taken as a premise.

Hilbert quali®es this rule expressly as ®nitary and goes on to remind us that

8xA(x) has a much wider scope than A(~n), where ~n is an arbitrarily given numeral.
Indeed, in the text that follows he shows that one can prove every (arithmetically)
true

-sentence

in the theory that results from adjoining rule

o* to PA. It is

worth bringing

o* into sharp focus. We shall do this by discussing two questions

we consider to be crucial. Let PA

¡
2

be the deductive closure of PA and

f8xj…x†j 8n …j…n† 2 P

^ PA ` j…n††g. The ®rst question is then this: does

Hilbert in his 1931 paper really intend to extend PA in the sense of PA

¡
2

or in

another? The question forces itself upon us, because the de®nition of the extension
of PA suggested by Hilbert (let us refer to it as Z*) is affected by indeterminacy.
The second question is: Can rule

o* be construed as ®nitary? Let us turn to the ®rst.

(a) Hilbert fails to de®ne the term `numerical formula’. We, for our part, accept the

standard view, according to which the numerical formulae are the quanti®er-free
formulae (cf. Feferman 1986) or the

-formulae.

(b) We de®ned PA

¡
2

in such a way that it by no means emerged as the closure of PA

under a restricted

o-rule, but only as the extension obtained by adjoining one

GoÈdel’s 1958 proposal to liberalize Hilbert’s original ®nitist point of view is less important for our

concern and will be left for another occasion.

Especially Detlefsen 1979, 310 comes close to our view when he denies that MM need be recursively enumerable.

Hilbert 1931, 491. In fact, it is unclear to us whether Hilbert extended his base system by an

o-rule or just

by one application of an

o-rule.

Hilbert does not, of course, use the terminology of the arithmetical hierarchy. We assume familiarity

with the arithmetical hierarchy; cf. Smorynski 1977 and Kaye 1991.

It is worth noting that in Ackermann 1925, 4. Numerical formulae are already de®ned as quanti®er-free

formulae.

Extensions of the Finitist Point of View

137

application of this rule. The closure of PA under rule

o* may be de®ned as

PA[

o]:=\{TjPA³T^T is a theory ^8c[8n(c(n) 2 P

^ T ` c(n)) ) T `

8xc]}. It seems, therefore, that Z* is not de®ned as PA

¡
2

, but rather as PA[

o].

Since one can prove `PA+Tr

0
1

=PA[

o] ’, this explication accords well with the

0
1

-completeness of Z* which Hilbert claims to have established.

It can also

be shown, however, that PA

¡
2

=PA[

o]. For this reason, we have taken the

liberty to present Z* as PA

¡
2

o* is this. As soon as we have proved in PA that

for each z, A(z) is correct, we are entitled to use 8xA(x) as a premise. Since we
assume that A(z) is

0
0

, we can de®ne a correctness-predicat e in PA as a partial

truth-predicate. Another possibility is to explicate `correct’ as `Pr

’ for a

representation

t of a suitable theory T. o* is then turned into the following

re¯ection-rule: If PA ` 8xPr

(A(x)), then 8xA(x).

Aleksandar IgnjatovicÂ (1994) rejected the standard interpretation of

o* (i.e.

version (b) above)

in the sense just speci®ed. From his point of view (330), Z* is

rendered precisely through S, where S := (QF-IA)+{8x

j(x) j j 2 P

0
0

^ (QF-IA) `

8xPr

qf-ia

… j…x† †}.

However, S is by no means

-complete. Since PA proves the

uniform re¯ection principle for (QF-IA), S is an axiomatizabl e subtheory of PA.
Even if we strengthen S considerably either by replacing, in the de®niens, (QF-IA)
by stronger axiomatizable theories or by abandoning the restriction imposed on

the resulting theories are still axiomatizable and, therefore, far from

0
1

-complete.

Now, IgnjatovicÂ himself observes that Hilbert claims to have shown the

completeness of Z*. In the light of this, we fail to see why IgnjatovicÂ considers S to
be a more precise version of Z*.

We now tackle the second question: Can rule

o* be construed as ®nitary?

When versions of the

o-rule are discussed in connection with Hilbert’s

programme, it is fairly common to adjoin one or the other of these to the ®nitary
metamathematical assumptions already accepted rather than to the formalized
mathematical theory under consideration (cf. Detlefsen 1979, p. 310). Those who
cast only a cursory glance at Hilbert’s 1931 paper may succumb to the temptation
of interpreting his characterization of

o* as ®nitary along these lines. The objective

of adjoining

o* in the sense just mentioned would appear straightforward: to pave

the way for consistency proofs for larger fragments of classical mathematics by
strengthening the ®nitary proof-theoretic repertoire. Closer examination of
Hilbert’s text, however, reveals that he adds

o* to the formalized theory PA, that

is, to a theory stated in the formalized object-languag e and already containing

By Tr

we understand the set of true

0
n

-sentences, by `Tr

(x)’ a formula representing this set in

a `natural’ way.

If we understand by a `numerical formula’ an arbitrary formula in the language of PA, then PA adjoined

by one application of the resulting

o-rule differs signi®cantly from the closure of PA under this o-rule.

The ®rst theory coincides with PA+Tr

0
3

+RFN[pa] (where RFN[pa] is the uniform re¯ection principle

for PA), the second is equal to Th (N ), i.e. the set of all arithmetically true sentences of L

10 See also Isaacson 1992 for the `standard’ view.
11 IgnjatovicÂ endorses the identi®cation of (formalized) ®nitist metamathematics with PRA or (QF-IA).

(QF-IA) is the conservative extension of PRA obtained by adding ®rst-order logic to PRA. Our
de®nition of S is a slight modi®cation of IgnjatovicÂ’s original de®nition (IgnjatovicÂ 1994, 330).

12 Perhaps we misrepresent IgnjatovicÂ by ascribing to him the view that S is a precise version of (QF-IA)

enlarged by one application of

o*. We do not, however, rule out that he regards S as a kind of `rational

reconstruction’ of Hilbert’s approach. At any rate, when IgnjatovicÂ criticizes Detlefsen’s interpretation
of Hilbert’s

o-rule, he seems to take version (c) as an explication of Z*; cf. especially 326.

138

Matthias Schirn and Karl-Georg Niebergall

trans®nite statements. For instance, he sketches a consistency proof for Z*.

It is

further noteworthy that around 1930 Hilbert’s programme did not centre
exclusively on consistency proofs for formalized mathematical theories. On the
contrary, Hilbert likewise attached great importance to issues concerning the
completeness of such theories. Accordingly, in his 1931 paper he shows that Z* is a
theory enjoying a higher degree of completeness (namely at least

0
1

-completeness)

than recursively enumerable theories.

He writes (1931, 491):

1. If a statement can be shown to be consistent, it is provable; and further
2. If for a sentence S one can prove the consistency with the axioms of number theory,
one cannot, at the same time, prove for S the consistency with those axioms.
I was able to prove these sentences at least for certain simple cases. This progress is
achieved by adjoining to the rules of inference already admitted (substitution and
inference ®gure [i.e. modus ponens]) the following likewise ®nitary rule of inference.

Hilbert goes on to state what we refer to as rule

o*. The use of the word `likewise’

clearly suggests that he intends to add

o* qua ®nitary rule of inference to the already

accepted ®nitary rules of inference. Yet to lay emphasis on the (allegedly) ®nitary
nature of

o* in the context he is considering is scarcely enlightening and may give

rise to confusion. What counts for Hilbert is the result that can be achieved by
adjoining

o* to PA; the question as to the ®nitary or non-®nitary status of o* is,

strictly speaking, irrelevant.

It comes as no surprise that Hilbert refrains from employing

o* in

metamathematical consistency proofs. M is void of any rules of inference in the
ordinary sense of the expression. And, according to Hilbert, ®nitist inferences are
either effected in the form of thought-experiment s on intuitively given objects (cf.
Hilbert and Bernays 1934, 32) or are carried out simply with concrete objects.
Hence, even if Hilbert were to succeed in justifying the purportedly ®nitary
character of

o*, any attempt at adjoining o* to the informal, contentual `modes of

inference’ available in M would clearly be at variance with the methodological
underpinnings of M. We are stressing here the informal character of M with the
proviso that by 1930 Hilbert may have undergone some change of mind as to the
nature of M. There is, however, no conclusive textual evidence for that.

We shall

therefore assume that in his 1931 article he is still subscribing to the essential ideas
concerning M as developed in his papers between 1923 and 1928.

13 Bernays 1935, 216 observes that by introducing the additional rule of inference

o* Hilbert relinquishes

the requirement of a complete formalization of the inferences in an arithmetical theory. Bernays speaks
in this connection of a deviation from Hilbert’s original proof-theoretic programme.

14 See also Bernays’s 1935, 214ff. comments.
15 Hilbert and Bernays 1934, 43 observe that the methodological standpoint of Brouwer’s intuitionism

incorporates a certain extension of the ®nitist point of view. The reason is claimed to be this:
Brouwer admits that an assumption is introduced about the presence of an inference or a proof,
without the inference or the proof being determined according to intuitive characteristics. From an
epistemological point of view, such an extension of the ®nitist attitude is said to amount to the
method of adjoining to the intuitive insights (gained in ®nitist reasoning) re¯ections of a generally
logical character. Hilbert and Bernays point out that the extension so conceived is requisite if by
means of ®nitist considerations one wishes to go beyond a certain elementary domain. Cf. also
Bernays 1930, 60. It is true that in his 1931 paper (486) Hilbert seems already to be hinting at this
kind of extension when he characterizes the insights a priori as those intuitive and logical insights
that we gain within the framework of the ®nitist attitude. But again, we are reluctant to regard this
isolated remark as furnishing conclusive evidence for the possible claim that by 1931 Hilbert’s
original conception of ®nitism had already undergone a signi®cant change.

Extensions of the Finitist Point of View

139

In spite of Hilbert’s use of

o* for the purpose of expanding a formalized

arithmetical theory, we now want to examine the question whether he would be
justi®ed in accepting

o* as a ®nitary rule of inference. Assuming, for the sake of

argument, that ®nitist (meta-)mathematic s is codi®ed by (QF-IA), three points
emerge

clearly.

First,

can

shown

that

(QF-IA)[

o]=(QF-IA)

(QF-IA)+Tr

0
2

Second, the closure of (QF-IA) under this

o-rule proves Con

(if

PA is consistent), even Con

(if ZF is consistent). Third, the closure of (QF-IA)

under

o* is not recursively enumerable. It is, therefore, hard to fathom what the

supposed ®nitist character of Hilbert’s extension of the ®nitist point of view might
consist in.

How can we dispense with the assumption of in®nity looming in proofs in PA

¡
2

, for

instance? Although proofs in PA

¡
2

are ®nite objects just as proofs in PA are, the

assumption in question is still contained in the postulates of PA

¡
2

. The claim `For

all natural numbers n (and consequently for in®nitely many objects)

j(n) must

already be provable in PA’ is expressed by the subformula `pa

(z)’ of the proof

predicate `Proof

¡
2

’, i.e. by 9u

5z (Fml(u)^z=8x.u^8y[P

0
0

(u[y])^Pr

(u[y])])’.

If we

retain the suggested mode of presentation of PA

¡
2

, we cannot avoid this assumption

of in®nity completely. We can, however, take advantage of the fact that
PA

¡
2

=PA+Tr

0
2

holds. It is true that this alternative mode of presenting PA

¡
2

does

not provide us with a decidable set of postulates. Yet it enables us to get rid of
in®nite rules of inference, and thus spares us the trouble of having to prove
in®nitely many premises.

Another reaction might be this. Since we can construe the in®nitely many premises of

one application and, hence, of ®nitely many applications of the

o-rule as ordered with

order type

o, the proof theorist who intends to employ the o-rule has to presuppose

only (the existence of)

o. By contrast, Gentzen’s consistency proof for pure number

theory in his 1936 article presupposes (the existence of)

Moreover, if a proof

theorist endorsing the basic tenets of Hilbert’s ®nitism were asked how he brings it
about to prove in®nitely many premises, he might respond as follows:

To accept one application of rule

o* is not more problematic than to make the

assumption that one can conclude from the PA-provability of `8x(0

4x)’ to the

PA-provability of `0

4n’ for every n. Both cases require that modus ponens be

applied in®nitely many times, where the sequence of the proo¯ines has order-
type

16 (QF-IA)[

o], (QF-IA)

and Tr

are de®ned in the same way as PA[

o], PA

¡
2

and Tr

17 It is worth noting that Hilbert 1926, 80 [370] expresses reserves towards proofs with in®nitely many

premises: `If we pay close attention, we ®nd that the literature of mathematics is replete with
absurdities and inanities which can usually be blamed on the in®nite. So, for instance, some stress
the stipulation, as a kind of restrictive condition, that, if mathematics is to be rigorous, only a ®nite
number of inferences is admissible in a proofÐas if anyone had ever succeeded in carrying out an
in®nite number of them.’ Admittedly, with these remarks Hilbert does not directly object to ®nitely
many inferences with in®nite rules of inference. Still, he does so indirectly, because in®nitely long
proofs with ®nite rules of inference can be converted, at least for the most part, into ®nite proofs
with in®nite rules of inference.

18 This notation should be self-explanatory. Here we do not pay closer attention to questions of coding.
19 Since PA

¡
2

is not axiomatizable, GoÈdel’s theorems prima facie do not apply to it (or to the closure of

(QF-IA) under rule

o*). Nevertheless, not only is this theory (trivially) incomplete, but it also

satis®es GoÈdel’s Second Incompleteness Theorem. Accordingly, extensions of axiomatizable theories
by rule

o* are affected by the same kind of incompleteness results as those familiar from

axiomatizable theories.

20 Of course, we say more about his consistency proof in

}3.

140

Matthias Schirn and Karl-Georg Niebergall

We venture to surmise that Hilbert qua metalogician relies on existence

assumptions of precisely this kind without being haunted by any ®nitist qualms.
And we do think that those assumptions of in®nity that are made by accepting one
application of rule

o* are not more far-reaching than those made by accepting

trans®nite induction up to

It should be evident that the

o-rule or even one application of it cannot be

accepted from Hilbert’s original ®nitist point of view. Yet both modern metalogic
and Hilbert’s metamathematic s of the 1920s rest on certain assumptions of in®nity
that clash anyway with his classical ®nitism (cf. Niebergall and Schirn 1998, section
4). Intuitively speaking, one may tend to believe that the metalogical assumptions
of in®nity just appealed to, or Hilbert’s assumption in his work on proof theory in
the 1920s that there are in®nitely many stroke-symbols, are slightly weaker than
those that we make when we apply an

o-rule. However this may be, we do not rule

out that Hilbert wants to commit himself only to the possible existence of in®nitely
many stroke-®gures or, alternatively, to the existence of in®nitely many possible
stroke-®gures.

Unless a satisfactory theory of the potential in®nite is to hand, it is

probably wise to postpone closer scrutiny of the question whether, from the point
of view of strength, applications of a given

o-rule and the assumptions of in®nity,

both made by Hilbert in the 1920s and common in contemporary metalogic, differ
essentially from each other.

Arriving at PRA: Hilbert and Bernays (1934)

In his short introduction `Zur EinfuÈhrung’ to Hilbert and Bernays (1934), Hilbert

denies that GoÈdel’s Incompleteness Theorems undermined his proof-theoreti c
programme. He claims that GoÈdel’s result shows merely that more far-reaching
consistency proofs require that the ®nitist point of view be utilized in a stricter
sense than is the case when elementary formalized systems are considered. And in
the ensuing Preface to the ®rst edition of Hilbert and Bernays (1934), Bernays
concedes that the work of Herbrand and GoÈdel evoked a change in the area of
proof theory, calling for new insights.

We know, of course, that the apparently

undiminished optimism displayed in Hilbert and Bernays (1934) regarding the
feasibility of a ®nitist consistency proof even for second-order arithmetic proved to
be unjusti®ed. It springs to mind that the method suggested by Hilbert and Bernays
in the face of GoÈdel’s theorems is, contrary to what Hilbert says in his
introduction, not a more rigorous utilization of the ®nitist standpoint, but just the
opposite: the ®nitist point of view is extended (Hilbert and Bernays 1934, 43, 1939,
VII) or its bounds are loosened (Hilbert and Bernays 1939, 362).

Let us stress at

this point that Hilbert’s ®nitist metamathematic s of 1934 is still an informal theory
which is not stated in precise terms.

Our subsequent considerations will primarily, but not exclusively, be of historical

interest. We take it that Hilbert was strongly in¯uenced by his collaborator Bernays
when he embarked on broadening the ®nitist point of view. In his short foreword

21 Even one application of

o* leads to a theory which, in the sense of recursion theory, is less `constructive’

than the addition of trans®nite induction up to

. This observation does not entail that the assumptions

of in®nity embodied in PA

¡
2

are stronger than those contained in PA enlarged by trans®nite induction

up to

. Questions concerning the strength of assumptions of in®nity ought not to be con¯ated with

questions concerning recursion-theoretic complexity.

22 See Niebergall and Schirn 1998.

Extensions of the Finitist Point of View

141

to the second volume of Grundlagen der Mathematik, Hilbert writes: `At my request,
P. Bernays has once again written the text. I thank him for the care and faithfulness
with which he has rendered my thoughts, and in whose development he has taken a
most active part for so many years of collaboration.’ Notice that Hilbert speaks
here of his thoughts. We think that the reader of the two volumes of Grundlagen
der Mathematik has to proceed from the assumption that they re¯ect faithfully
Hilbert’s position both around 1934 and around 1939 regarding the scope of ®nitist
methods in metamathematics . It is unlikely that in Grundlagen der Mathematik
Bernays would have taken the liberty to present a view about ®nitism which was
not in basic agreement with Hilbert’s own opinion at that time. And Hilbert surely
read the manuscripts before they went to press. The fact that even the ®rst volume
of Grundlagen der Mathematik was written not by Hilbert, but by Bernays should,
at any rate, be plain to anyone sensitive to author’s style. While in his principal
papers on proof theory of the 1920s Hilbert writes with power and vividness and
occasionally even with a touch of gracefulness, Bernays’s style in Grundlagen der
Mathematik strikes us as less appealing. We are, of course, aware that Grundlagen
der Mathematik was ®rst and foremost intended to be a mathematical work.

It is important to bear in mind that ®nitist metamathematics may be extended by

adding well-formed formulae or by adjoining further `principles’. It is the ®rst
possibility that is at issue in Hilbert’s proposed ®nitist interpretation of quanti®ed
statements about numerals (Hilbert and Bernays 1934, 32ff.). So, let us begin by
taking a closer look at this.

23 In his introduction to Herbrand’s 1931 article `Sur la non-contradiction de l’arithmeÂtique’, van

Heijenoort points out that it was intended to be a contribution to the realization of the programme
of the Hilbert school. He also observes that throughout his work `Herbrand applies the word
``intuitionistic’’ to the methods that he considers admissible in metamathematics, and, although there
may be some variations in the meaning that he gives to the term, this meaning is on the whole much
closer to that of Hilbert’s word ``®nitary’’ (`®nit’) than to ``intuitionistic’’ as applied to Brouwer’s
doctrine’ (van Heijenoort 1967, 618). For Herbrand’s speci®c use of the word `intuitionistic’ see
especially

}4 (entitled `Comparison with a theorem of GoÈdel’s’) of his article mentioned above. There

seems to have been a certain tendency among Hilbert’s young collaborators in the 1920s to consider
`intuitionistic’ and `®nitist’ (`®nitary’) to be synonymous or interchangeable terms. Thus, in his essay
`Zur Hilbertschen Beweistheorie’, von Neumann (1927) speaks at one place (p. 7) of the
`intuitionistic-®nitist’ character of his `contentual’ re¯ections. At another place (p. 21), he emphasizes
that in all inferences he has to proceed `intuitionistically (i.e. ®nitistically)’. Recall in this connection
Hilbert’s and Bernays’s remarks on the methodological point of view of Brouwer’s intuitionism to
which we referred in footnote 15. Now, it would probably be too hasty to conclude from these
remarks that in the early 1930s Hilbert in effect considered his ®nitism of the 1920s to be a restricted
form of intuitionism. And even if he did, it is by no means clear whether, on closer examination of
the epistemological underpinnings of the two doctrines, such a view could be sustained. It is true that
GoÈdel 1958 described both what he took to be the kinship and the difference between ®nitism and
intuitionism in a way which comes relatively close to Hilbert’s and Bernays’s brief characterization.
According to GoÈdel, the shared component of ®nitism and intuitionism is the idea that we are
entitled to speak of mathematical objects only to the extent that we can exhibit them. However,
Detlefsen 1998 argues convincingly that what separates intuitionism from ®nitism is not only the
nature of the objects exhibited, but the very nature of exhibition itself.

24 It seems that in the light of GoÈdel’s Incompleteness Theorems Bernays sympathized with the idea of

allowing

considerable extension

of Hilbert’s

original

®nitist

standpoint.

`Hilberts

Untersuchungen uÈber die Grundlagen der Arithmetik’ 1935, 216 he expresses the belief that the
method applied by Gentzen in his (®rst) consistency proof of PA meets the fundamental
requirements of the ®nitist point of view. See in this connection also the postscript to Bernays 1930
and Bernays 1967, 502. In the postscript, Bernays observes, by appeal to GoÈdel’s Theorems, that the
epistemological point of view underlying Hilbert’s original proof-theoretic programme has turned
out to be problematic. In particular, the sharp distinction between the intuitable and the non-
intuitable, as it is applied in connection with the problem of the in®nite, is, according to Bernays,
seemingly unfeasible.

142

Matthias Schirn and Karl-Georg Niebergall

(1) A general statement about numerals `8~n ~

A(~n)’ can be interpreted ®nitistically only

as a hypothetical statement, i.e. as a statement about every given numeral. A
general statement about numerals expresses a law that has to be veri®ed for
each individual case.

(2) An existential statement about numerals `9~n~

A(~n)’ must be construed, from the

®nitist point of view, as a `partial proposition’, i.e. `as an incomplete
communication of a more exactly determined statement, which consists either
in the direct speci®cation of a numeral with the property ~

A(~n) or in the

speci®cation of a procedure for gaining such a numeral’ (Hilbert and Bernays
1934, 32). The speci®cation of the procedure requires that for the sequence of
acts to be carried out a determinate limit be presented.

(3) In like manner we have to interpret ®nitistically statements in which a general

statement is combined with an existential statement such as `For every numeral

~k with the property ~

A(~k) there exists a numeral ~l for which ~

B(~k,~l) holds’, for

example. In the spirit of the ®nitist attitude, this statement must be regarded as
the incomplete communication of a procedure with the help of which we can
®nd for each given numeral ~k with the property ~

A(~k) a numeral ~l which stands

to ~k in the relation ~

B(~k,~l).

(4) Hilbert points out that negation is unproblematic when applied to what he calls

`elementary propositions’, i.e. to statements which can be decided by direct
intuitive observation. In the case of universally and existentially quanti®ed
statements about numerals, however, it is not immediately clear what ought to
be regarded as their negation in a ®nitist sense. The assertion that a numeral ~n
with the property ~

A(~n) does not exist has to be conceived of as the assertion

that it is impossible that a numeral ~n has the property ~

A(~n). Strengthened

negation of an existential statement, thus construed, is not (as in the case of
negation of an elementary statement) the contradictory of `9~n~

A(~n)’. From the

®nitist standpoint, we therefore cannot make use of the alternative according to
which there either exists a numeral ~n to which ~

A(~n) applies or the application of

A(~n) to a numeral ~n is excluded. Hilbert admits that, from the ®nitist
perspective, the law of excluded middle is invalid in so far as for quanti®ed
sentences we do not succeed in ®nding a negation of ®nitist content which
satis®es this law.

Now, when we compare (1)±(4) with Hilbert’s remarks on what can be formulated
®nitistically in, say, `UÈber das Unendliche’ (1926), we notice two things.
Explication (4) is very much akin to the points made in that paper about the
negation of quanti®ed statements. The matter stands differently with (1)±(3). On
plausible grounds, one should assume that a ®nitistically interpreted sentence is
capable of being formulated ®nitistically in the ®rst place. If that is correct, then (1)
to (3) ought to be understood in such a way that universally quanti®ed sentences,
even sentences whose formalizations are genuine

0
2

-sentences (cf. (3)), can be

formulated in the language of ®nitist metamathematics . Plainly, if around 1934
Hilbert really wished to maintain that quanti®ed sentences of types (1)±(3) have a
proper place in the language of ®nitist metamathematics , he would have departed

25 The proposed interpretation of universal quanti®cation is reminiscent of Gentzen’s and W.W. Tait’s

account (See Tait 1981) in that it likewise embodies a version of the

o-rule which rests on the

identi®cation of numerals with numbers. Tait’s additional idea is that the law in question is to be
construed as something given by a ®nitist function.

Extensions of the Finitist Point of View

143

signi®cantly from his conception of metamathematic s in the 1920s. It is quite true that
both in `UÈber das Unendliche’ and in Grundlagen der Mathematik (1934) Hilbert
spares himself the trouble of developing the language of ®nitist metamathematics in
a systematic way. There is one crucial difference, though. In his celebrated essay,
the distinction between real and ideal statements, although chie¯y designed to
streamline the formalism, provides at least a clue for assessing the scope and the
limits of the language of ®nitist metamathematics .

By contrast, the reader of

Hilbert and Bernays 1934 who is expecting to encounter this helpful distinction
again here will be disappointed. In this book, there is not even a trace of it framed
in familiar terms.

Admittedly, all this does not exclude that an alternative way of construing the

phrase `®nitistically interpretable’ can be contrived. Consider sentences of type (1).
In `UÈber das Unendliche’ `8x(x+1=1+x)’ is not a sentence of L

, and the same

applies to an expression like (*) `For every given ~a ``~a+1=1+~a’’ is true’. By
contrast, if a numeral ~a is given, the expression `~a+1=1+~a’ is a sentence of the
language of ®nitist metamathematics .

In Grundlagen der Mathematik (1934), the

question of which language (*) may belong to is passed over in silence. We are only
told that a ®nitist interpretation of (*) requires that it be construed as a
hypothetical judgement about every given numeral (cf. (1)) (we assume that (*)
should be considered a general statement about numerals). A similar formulation is
employed in `UÈber das Unendliche’ (91 [378]), with the minor difference that here
Hilbert talks about interpretation simpliciter.

And it is almost precisely at this

point that he introduces his conception of real and ideal statements, stressing that
the latter are, from the ®nitist point of view, devoid of meaning. This shows: the
fact that in `UÈber das Unendliche’ certain sentences of type (1), like (*), are
amenable to (a ®nitist) interpretation is compatible with the fact that the language
of ®nitist metamathematics does not comprise sentences of this type. The ®nitist
interpretation of (*) proceeds in such a way that for every given numeral ~a (*) is
replaced with `~a+1=1+~a’, and then each of the sentences `~a+1=1+~a’ is
interpreted ®nitistically. Seen from this angle, we should not take it for granted
that in Grundlagen der Mathematik (1934) ®nitist interpretability implies ®nitist
formulability. What we do take for granted is that if this implication holds for
sentences of one of these types, then it must also hold for the sentences of the
remaining types.

In order to ®nd out whether in Grundlagen der Mathematik (1934) quanti®ed

sentences of types (1)±(4) are indeed regarded to belong to the well-formed
sentences of the language of ®nitist metamathematics , it is useful to take a closer
look both at the number-theoretic formalisms presented there and at the
corresponding consistency proofs. In

}6 (Hilbert and Bernays 1934, 220ff.), Hilbert

carries out a consistency proof for a certain weak arithmetical axiom system (cf.
1934, 219) which we call H. The `proof’ is entirely informal, and it is not clear
whether Hilbert shows metamathematicall y `There is no proof in H for falsum’ or
only for every concretely given proof ®gure a that a is no proof for falsum in H.
The very beginning of the proof speaks in favour of the second option, that is, we
conjecture that Hilbert conducts what is in effect an informal version of what in

26 See Niebergall and Schirn 1998,

}}3 and 5.

27 See Niebergall and Schirn 1998,

}5.

28 It is reasonable to assume that here he likewise has a ®nitist interpretation in mind. Notice that non-

®nitary sentences, i.e. ideal sentences, are not interpreted at all.

144

Matthias Schirn and Karl-Georg Niebergall

our paper `Hilbert’s ®nitism and the notion of in®nity’ (1998) we call an approximative
consistency proof:

`We now imagine that we are given such a proof ®gure with the

end formula 06ˆ0. On this [proof ®gure] two processes can be effected one after
another which we call dissolution of the proof ®gure in ``proof-threads’’ and
elimination of the free variables’ (Hilbert and Bernays 1934, 220; cf. 298).

Hilbert and Bernays show, in the ®rst place, that every numerical formula that can

be derived from the axioms of H without the use of bound variables is true.

In a

second step, they demonstrate that every numerical formula provable in H is true
even if we drop the restriction concerning the bound variables. They generalize the
notion of a true formula in such a way that all formulae of a given proof ®gure are
taken into account, not only the numerical ones (cf. Hilbert and Bernays 1934,
232ff.). This is accomplished by introducing the term `veri®able’. Con®ning
themselves provisionally to formulae without universal quanti®ers, Hilbert and
Bernays explain the term as follows: (i) a numerical formula is veri®able, if it is
true; (ii) a formula containing one or more free individual variables, but no other
variables, is veri®able, if it can be shown that it is true for every replacement of the
variables with numerals; and (iii) a formula with bound variables, but without
formula variables and without universal quanti®ers is veri®able, if the application
of a certain reduction procedure leads to a veri®able formula in the sense of (i) or
(ii).

In a further step, Hilbert and Bernays show that the end formula of the given

proof (in H) is veri®able (cf. Hilbert and Bernays 1934, 244ff.). H is therefore
consistent.

As to (ii), it is plain that veri®ability is de®ned through an unbounded

quanti®cation over numerals, i.e. for all substitution instances. The phrase `can be
shown’ remains unexplained and is possibly meant to impart a `constructive’ or
®nitist air to unbounded universal quanti®cations over numerals.

These belong, in

the terminology of Hilbert (1926), to the class of ideal statements and are as such
unacceptable for the ®nitist of the 1920s. We further note that carrying out
consistency proofs along the lines of (i)±(iii) requires that the veri®ability predicate
can be formulated in the language of ®nitist metamathematics . Hence, this
language must contain sentences of type (1).

Let us now turn to Hilbert’s and Bernays’s introduction of `recursive number

theory’ (cf. Hilbert and Bernays 1934, 330ff.). In section 7, entitled `The recursive
de®nitions’, they introduce a formal theory T couched in a quanti®er-free language
L

. Besides some simple number-theoretic axioms, T contains the rule of induction

in L

. The crucial thing about L

is the circumstance that it includes only

5 and ’

as non-logical signs and, hence, only a rather weak version of quanti®er-free
induction. Due to this circumstance, T is considerably weaker than PRA (cf. Rose
1984, 137ff.; Kaye 1991; HaÂjek and Pudlak 1993). Recursive number-theory,
henceforth referred to as B*, arises from T by way of enlarging L

to include signs

29 In Niebergall and Schirn 1998,

}6 we de®ne this notion as follows (for axiomatizable theories S and T

with representation

t): S proves the approximative consistency of T:,8nS` :Proof

(n,?). We assume

here that the formalized proof predicate is the standard one. In our opinion, the notion of an
approximative consistency proof captures the core of the conception of ®nitary metamathematical
consistency proofs which Hilbert developed in his papers on proof theory in the 1920s.

30 Numerical formulae are characterized as quanti®er-free sentences; see Hilbert and Bernays 1934, 228.

Hilbert emphasizes that this is only a stricter version of the assertion that it is impossible to derive
06ˆ0 from the axioms of H without admitting bound variables (Hilbert and Bernays 1934, 230).

31 For Hilbert’s characterization of the reduction procedure see Hilbert and Bernays 1934, 233.
32 See also Parsons 1998.

Extensions of the Finitist Point of View

145

for primitive recursive functions and by adjoining to T the appropriate recursion
equations. Unfortunately, B* is not presented as a clear-cut theory. Depending on
whether the extension of T is applied to all or only to some primitive recursive
functions, we obtain as B* either the entire theory PRA or only a fragment of it.

On the one hand, several remarks in Hilbert and Bernays (1934) suggest that the

authors equate recursive number theory with the whole of PRA. Consider the
following passage:

The ef®ciency of the recursive functions shows itself yet much more clearly in
terms of the systematic development of the formalism which we obtain through
the general application of the recursive de®nitions, including the explicit
de®nitions and the schema of induction, by taking as a basis the elementary
calculus with free variables, the axioms of identity and the formula 0

’6ˆ0. [ . . .]

This way of treating number theory has been set forth by SKOLEM (Hilbert
and Bernays 1934, 309)

Here both the phrase `general application of the recursive de®nitions’

and the

reference to Skolem suggest that `this way of treating number theory’ is meant to
refer to what we nowadays call `PRA’. Hilbert and Bernays illustrate the
introduction of primitive recursive functions (function terms) with some examples
and observe that these `may suf®ce for providing an idea of the method according
to which number theory can be developed formally, both by means of the
recursions and the induction schema and by avoiding bound variables’ (Hilbert and
Bernays 1934, 330). They go on `We shall call this way of treating number theory
the recursive treatment of number theory or, in short, ``recursive number theory’’’
(Hilbert and Bernays 1934, 330). Here we seem to have some evidence for the claim
that B* is equal to PRA.

On the other hand, one might wish to argue, by drawing attention to the

consistency `proofs’ sketched by Hilbert and Bernays, that they construe B* as a
proper subtheory of PRA. They demonstrate (cf. Hilbert and Bernays 1934,
295ff.) that every extension E of the theory T by ®nitely many recursion
equations can be proved ®nitistically as consistent by establishing, with ®nitist
means, the veri®ability of the E-theorems.

Hilbert and Bernays write: `This

recursive number theory is closely related to intuitive number theory, considered
in

}2, in so far as all its formulae can be endowed with a ®nitist contentual

interpretation. This contentual interpretability results from the veri®ability,
already ascertained, of all derivable formulae of recursive number theory’
(Hilbert and Bernays 1934, 330). Thus it seems that Hilbert and Bernays are
justi®ed in claiming ®nitist contentual interpretability for a theory S only on
condition that S is such a ®nite extension of T. If in the quotation above they
want to maintain only that every single B*-theorem can be interpreted
®nitistically, we may still construe B* as PRA. By contrast, if Hilbert and
Bernays wish to convey that the entire theory B* can be interpreted ®nitistically,
then B* can only be a ®nite extension of T. Yet if the latter is the case, B*
cannot coincide with PRA (cf. Rose 1984, 137ff.; Sieg 1985, 47).

33 `Recursive’ means here `primitive recursive’, 286ff.
34 Notice that E also comprises theorems with free variables, so that for Hilbert and Bernays truth does not

suf®ce, but must give way to the allegedly more general notion of veri®ability.

146

Matthias Schirn and Karl-Georg Niebergall

At any rate, B* is a subtheory of PRA, which is formulated in a quanti®er-free

language. It is also plain that B* contains at least the recursion equations for
addition and multiplication. Since we may further assume that B* is recursively
enumerable, we can regard B* as a

-complete theory.

You will remember that we aim at ®guring out what ®nitist metamathematics in

Hilbert and Bernays (1934) is supposed to be. In the foregoing, we analyzed the
status of B*, because ®nitist metamathematics is used to establish the consistency
of B*. Although it is hard to determine the relationship between B* and ®nitist
metamathematic s in precise terms, we think that the interpretations we shall now
suggest broadly square with the relevant passages in Hilbert and Bernays (1934).
First, Hilbert and Bernays show in ®nitist metamathematics that B* is consistent or
that B* is veri®able or (*) that each B*-theorem is veri®able. Second, Hilbert and
Bernays show for a given B*-proof a in ®nitist metamathematics that a does not
end with falsum or (+) that the last proof-line of a is veri®able. Options (*) and
(+) can be rendered more precisely thus:

(**) In metamathematics it is shown `8

c (c quanti®er-free ^ B* ` c ) c is

veri®able)’
(++) 8

c (c quanti®er-free ^ B* ` c ) in metamathematic s it is shown `c is

veri®able’).

Recalling how Hilbert’s and Bernays’s consistency proofs actually get started,

even two further options can be contrived. The ®rst is: (+*1) Let a be given as a
code of a possible proof. It is then shown with ®nitist metamathematical means: if
a is a proof in B* for a quanti®er-free statement

c of L

, then

c is true. To be

sure, we have only mentioned the case that ®nitist metamathematics proves the
truth of every closed B*-theorem with a given proof. So, what are we to make of
the veri®ability of the open formulae with a given B*-proof to which Hilbert and
Bernays attach such importance? This leads us to (+*2): Let a be given as a code
of a possible proof. It is then shown with ®nitist metamathematica l means: if a is a
proof in B* for a quanti®er-free formula

c of L

, then

c is veri®able.

Since we do not know which subtheory of PRA B* really is, we have several

options as to how ®nitist metamathematics in Hilbert and Bernays (1934) could be
characterized. Before we deal with the question of how strong it is, two points
deserve attention.

First: in order to be able to compare, in a reasonable way, Hilbert’s and Bernays’s

informal ®nitist metamathematics of 1934 with B*, we replace the former with a
formalized version, called `FMM’. This means that the principles (**), (++),
(+*1) and (+*2) must be formalized as well. We assume for this purpose that B*
is represented by a

-formula b*(x). A plausible candidate for a formalization of

(**) is, for example:

…F**

† 8c ‰c is quantifier-free ) FMM ` 8x…Pr

… c…x† † ! Ver… c…x† ††Š

Here `Ver(x)’ ought to be construed as an arithmetical formalization of the
metatheoretic veri®ability predicate; the latter is a generalized truth predicate for
arithmetical sentences. Since the truth predicate for arithmetical sentences is not
arithmetically de®nable, it could seem, on the face of it, that the constraint imposed
on `Ver(x)’ may entangle us in dif®culties. However,

c(x) is taken to be a

Extensions of the Finitist Point of View

147

quanti®er-free formula. We therefore need to de®ne here only a `partial veri®ability
predicate’, and as such a satisfaction predicate for

-formulae suf®ces. The latter

can be de®ned arithmetically as a

-formula; it is already in the context of rather

weak subtheories of (QF-IA) that this predicate has the feature characteristic of a
partial truth predicate, namely the provability of the restricted T-schema.

In what

follows, we prefer to formalize (**), (++), (+*1) and (+*2) in such a way that
the use of partial veri®ability or satisfaction predicates is dispensed with.

…F**†

8c ‰c is quantifier-free ) FMM ` 8x…Pr

… c…x† † ! c…x††Š

…F ‡ ‡† 8c ‰c is quantifier-free ^ B* ` c ) FMM ` c†Š

…F ‡ *1† 8c8n ‰c is quantifier-free ) FMM ` Proof

…n; c † ! cŠ

…F ‡ *2† 8c8n ‰c is quantifier-free ) FMM ` 8x…Proof

…n; c…x† † ! c…x††Š

It should be emphasized here that (F**) and (F+*2) can be considered to be well-

formed only if the language of FMM contains at least

-sentences. We assume now

that FMM proves every true

0
0

-sentence. This assumption appears natural; we may

already regard MM as

0
0

-complete. The crucial point is that FMM proves every true

-sentence of L

FMM

, bearing in mind that FMM is closed under logical consequence

at least in the domain of

-sentences.

Second, reading through the ®rst volume of Grundlagen der Mathematik, we learn

at best how strong at least FMM is. If we suppose, for example, that Hilbert and
Bernays accepted B*=PRA, and if we understand the metamathematica l
veri®ability assertion for B*-theorems in the sense of (F**), then it should be clear
that FMM proves Con

pra

. This by no means rules out that in FMM we could

prove even much more than Con

pra

. Nonetheless, although we cannot specify an

upper bound for the strength of Hilbert’s and Bernays’s ®nitist metamathematics of
1934, we have no reason to assume that it goes beyond the means that they actually
use when they sketch a consistency proof.

We now want to explore the question of how strong FMM is at the very least. We

shall do this by distinguishing several options. On the one hand, we have (F**) and
(F+*1) or (F+*2) respectively.

On the other hand, we consider the case that B*

is equal to PRA or a ®nite extension of T. Option (F++) is trivial: B* is a
subtheory of FMM.

(a) Suppose that (F**) holds. Since FMM is

-complete, we have: if B* `

c, then

… c † qua true S

-sentence is also FMM-provable:

(i) B* is PRA. In this case, PRA is a subtheory of FMM, and FMM proves the

uniform re¯ection principle for PRA, restricted to quanti®er-free formulae of
L

pra

, i.e. RFN

[b*]. This principle is equivalent to Con

pra

over PRA. Hence,

FMM need not be taken to be stronger than PRA+Con

pra

; yet FMM is at

least as strong as PRA+Con

pra

;

(ii) B* is a ®nite extension of T. Then PRA proves RFN

0
0

[b*] (cf. Girard 1987,

226ff.). If FMM is an extension of B* which is just strong enough to prove

35 See HaÂjek and Pudlak 1993 and Kaye 1991.
36 If an analogy is allowed, we could say that FMM proves the approximative soundness of B*.
37 We need not especially account for the fact that FMM proves the consistency or the approximative

consistency of B*. For FMM ` Con

follows from (F**), and it follows from (F+*1) and (F+*2)

that FMM proves the approximative consistency of B*.

38 The reason is that B* is formulated in a quanti®er-free language.

148

Matthias Schirn and Karl-Georg Niebergall

RFN

0
0

[b*], then we may assume that FMM=B*+Con

. FMM is then a

proper subtheory of PRA.

(b) Suppose that (F+*1) is in force and let B* `

c. There is then an n such that

FMM ` Proof

(n, …

c †; for FMM proves every true S

-sentence. With (F+*1)

it follows FMM `

c. B* is therefore a subtheory of FMM. Due to the fact that

B* is

0
1

-complete, it also holds: For every n 2

o B* ` Proof

(n, …

c † ! c.

The upshot is this: If FMM proves every true

-sentence, we may assume that

FMM coincides with B*. Thus FMM need not be an extension of PRA.

FMM=PRA+Con

pra

suf®ces to make (F+*2) true.

Here, then, is what we take to be the quintessence of Hilbert’s and Bernays’s

metamathematical approach in the ®rst volume of Grundlagen der Mathematik.
Compared to Hilbert’s standpoint in the 1920s, ®nitist metamathematics in 1934 is
likely to have been expanded in the ®rst of the two ways mentioned at the outset of
section 2; it has de®nitely been extended in the second way. (a) It seems clear that
quanti®ed sentences of type (1) can indeed be formulated in L

or that their

formalized counterparts, i.e.

-sentences, belong to the well-formed sentences of

the language of FMM. As far as sentences of types (2)±(4) are concerned, we
suggest that they can be formulated in L

, too. (b) FMM is at least as strong as

PRA, and may include even PRA+Con

pra

So much to metamathematics as it is developed in the ®rst volume of Grundlagen

der Mathematik. The formalization of metamathematics was left for the second, to
which we now turn.

The sellout of ®nitism: Hilbert and Bernays (1939)

In his introduction to the second volume of Grundlagen der Mathematik, Bernays

points out that the book pursues two main issues. The ®rst is to give a thorough
account of Hilbert’s proof-theoretic investigations which rest on methods linked
with the

e-symbol. The second main issue is a discussion of the circumstance which

has created the need of extending, vis-aÁ-vis the former delimitation of the `®nitist
point of view’, the framework of the contentual modes of inference admitted in
proof theory. The circumstance Bernays has in mind is, of course, GoÈdel’s
discovery of the incompleteness of Peano arithmetic.

We are further informed that the discussion of the extension of the ®nitist point of

view leads to a consideration of Gentzen’s consistency proof for number theory. In
this

context,

Bernays

also

refers

Ackermann’s

(1940)

article

`Zur

Widerspruchsfreiheit der Zahlentheorie’ (which, we assume, was then nearly
completed) and speaks of a rehabilitation of `that original Hilbertian approach’,
provided that Ackermann’s proof is successful. By `that original Hilbertian
approach’ Bernays means Hilbert’s proof-theoreti c methods resting on the
elimination of the

e-symbol (cf. Hilbert and Bernays 1939, 92±126). In his

dissertation `BegruÈndung des ``tertium non datur’’ mittels der Hilbertschen Theorie
der Widerspruchsfreiheit’ , Ackermann (1925) had already applied these methods.
He gives there a consistency proof for number theory exclusive of complete
induction (see also Hilbert and Bernays 1939,

}2.4). The fundamental idea of the

proof is to show that within the proof ®gure the

e’s can be replaced with numerical

signs in such a way that all formulae of the proof ®gure are turned into formulae

Extensions of the Finitist Point of View

149

which can be established as being `correct’ according to the methods of ®nitist
mathematics. In his 1940 article, Ackermann extends this metamathematica l
method to the case that complete induction, too, will be used in the proofs of
formalized number theory. The crucial step in his proof consists in carrying out a
proof of ®niteness. While Gentzen (1936) proposes to show the ®niteness of a
certain reduction procedure, Ackermann intends to establish the ®niteness of the
succession of what he calls `Gesamtersetzungen ’ (1940, 175ff).

Like Gentzen,

Ackermann must make use of trans®nite induction up to

However,

Ackermann does not pretend, at least not explicitly, that his consistency proof for
full ®rst-order arithmetic proceeds within the limits of ®nitist methods.

By contrast, Gentzen does claim that his consistency proof is ®nitary, despite the

use of trans®nite induction. Does he argue for his claim, and if so, does his argument
carry conviction? To answer this question, we must take a closer look at Gentzen’s
proof and the relevant remarks he makes about its alleged ®niteness. We shall do
this mainly for preparatory reasons. In the second volume of Grundlagen der
Mathematik, Hilbert and Bernays discuss in detail Gentzen’s ®rst consistency proof
and raise the question whether trans®nite induction up to

can be accepted as a

®nitary method of proof.

Gentzen (1936, 500 [138]) regards metamathematics as a formalized mathematical

theory whose consistency must already be presupposed. Absolute consistency proofs
are said to be impossible, because a consistency proof can only reduce the `correctness’
of certain modes of inference to the `correctness’ of other modes of inference.
Gentzen’s (1936) (relative) consistency proof for PA in his article rests on a
reduction procedure for sequents and derivations whose technical details need not
concern us here (cf. Gentzen 1936,

}}13f.). Gentzen introduces the concept of the

statability of a reduction rule for a sequent as the formal substitute of the
`contentual concept of correctness’.

The consistency of PA follows from the proof

that reduction rules can be stated for all sequents occurring in an arbitrarily given
derivation, once the derivation has been transformed according to a rule designed
to eliminate the operators ^, 9, and ¼ from a given derivation (cf. Gentzen 1936,
}12). In order to prove the ®niteness of the reduction procedure, i.e. in order to
prove that by successively carrying out a reduction step on a given derivation we
always arrive at the reduced form (of the endsequent) in ®nitely many steps,
Gentzen shows that each reduction step in a certain sense `simpli®es’ a derivation.
For this purpose, he correlates with each derivation an ordinal number,
representing a measure for the `complexity’ of the derivation. It is then shown that
in a reduction step the ordinal number of a derivation (usually) diminishes. The

39 An explication of Ackermann’s term `Gesamtersetzung’ requires a prior explanation of the term

`fundamental type’ (`Grundtyp’). If in the

e-term ex~

A(x) we replace the terms ~a

, ~a2, . . ., ~a

with the

free number variables a

, a

, . . ., a

, then

ex~

A(x) is turned into a term

ex ~

B(x, a

, . . ., a

), where ~

B(x,

, . . ., a

) contains no free variables except a

, a

, . . ., a

ex ~

B(x, a

, . . ., a

) is called the

fundamental type belonging to

ex~

A(x). Now, when we assign to each fundamental type a recursive

function with the same number of arguments, and to each fundamental type without arguments a
determinate numeral as replacement, then, according to Ackermann (1940, 168), every formula of the
proof ®gure can be uniquely transformed into a `correct’ or `false’ formula. Such a replacement for
the fundamental types is called Gesamtersetzung. In

}6 (178ff.) of his 1940 paper, Ackermann

presents a stricter version of his proof of ®niteness by establishing an upper bound for the number of
`Gesamtersetzungen’ which can be formed at all.

40 See the account of Ackermann’s 1940 proof in Hilbert and Bernays 1939, 535ff.
41 If we have checked correctly, then in his 1940 paper he nowhere uses the word `®nitist’ (`®nit’).
42 The German term used by Gentzen 1936, 536 is `inhaltlicher Richtigkeitsbegriff’.

150

Matthias Schirn and Karl-Georg Niebergall

crucial point resides in the idea that enables us to recognize a simpli®cation of the
derivation in a reduction step despite the apparent increase in complexity. Finally,
Gentzen proves the theorem of trans®nite induction (1936, 555 [192]):

All ordinal numbers are accessible in the following sense, by our running through
them in the order of their increasing magnitude: the ®rst number 0,1 is considered
accessible; if further all numbers smaller than a number

b have been recognized as

accessible, then

b is also considered accessible.

By virtue of that theorem, the ®niteness of the reduction procedure for arbitrary

derivations follows at once (cf. Gentzen 1936, 556 [193]). The property of the
®niteness of the reduction procedure carries over from the totality of the
derivations with the ordinal numbers smaller than

b to the derivations with the

ordinal number

b. According to the theorem of trans®nite induction, this property

therefore holds for all derivations with arbitrary ordinal numbers. Gentzen stresses
that the de®nition of the notion accessible is entirely `constructive’; for

b is

explained as accessible only when all numbers smaller than

b have previously been

recognized as accessible. We are asked, though, to construe the word `all’ occurring
here ®nitistically, on the grounds that `in each case, we are dealing with a totality
for which a constructive rule for generating all elements is given’ (Gentzen 1936,
558 [195]). Gentzen claims towards the end of his paper that the proof of the
®niteness of the reduction procedure can be regarded as having been conducted
within the bounds of indisputable methods of proof, so that his consistency proof
provides a real vindication of the disputable methods of PA (1936, 560 [197]).

Gentzen’s treatment of the word `all’ suggests that he considers his consistency

proof to be ®nitistically interpretable. He does not explain, however, what he
exactly has in mind when he uses the phrase `®nitist interpretation’. We think that
there are two possible ways of understanding it; to be sure, none of them supplies a
strong argument for Gentzen’s claim that his proof is ®nitary. Gentzen proposes a
`®nitist’ interpretation of universal quanti®cation, that is, ``8x

c(x)’’ has the same

sense as `For every (given) numeral n

c(n)’. If this is to imply that in a ®nitistically

acceptable theory S `8x

c(x)’ is provable if and only if for every numeral n we can

derive `

c(n)’ in S, then Gentzen faces several dif®culties. Either ` ``8xc(x)’’ is

provable in S’ undergoes reinterpretation and is de®ned as `8n S `

c(n)’ or S is

closed under the

o-rule, and hence is not even arithmetically de®nable, let alone

recursively enumerable.

When applied to the schema of trans®nite induction, the problem presents itself as

follows. Gentzen argues in favour of the ®nitist admissibility of TI[

] by appeal to its

allegedly constructive character.

We think that his line of argument depends

crucially on his `®nitist’ interpretation of universal quanti®cation and that it lacks
persuasive power precisely for this reason. Let

lx.o[x] be the fundamental sequence

converging to

de®ned by

o[0]:=1, o[n+1]:=o

o[n]

. It holds then that (a) for all n

PA ` TI[

o[n]], but not (b) PA ` 8xTI[o[x]], i.e. it does not hold that PA ` TI[e

There are now two options.

43 See the Gentzen-style consistency proof for PA in Takeuti 1975, 97ff.; cf. also Gentzen’s new version of

the consistency proof for PA in his 1938 paper.

44 In our paper `Finitism = PRA? On a thesis of W.W. Tait’ (forthcoming), we argue that even restricted

versions of the

o-rule lead to theories which can hardly be accepted from the point of view of ®nitism.

45 Under `TI[

]’ we understand here the schema of tran®nite induction up to

in the language L

of PA.

Extensions of the Finitist Point of View

151

First, `8xTI[

o[x]]’ is understood ®nitistically in the sense of the ®rst disjunct of the

alternative above. (b) is then reinterpreted as (a), and `PA+TI[

]’ is per de®nitionem

equivalent to PA+{

cj 9n PA+TI[o[n]] ` c}. In this case, a consistency proof in

`PA+TI[

]’ for PA is beyond reach, since `PA+TI[

]’ coincides with PA.

Second, Gentzen’s `®nitist’ interpretation of universal quanti®cation is regarded as

a new principle of proof, i.e. for formulae of restricted complexity, for instance, it is
assumed that we can conclude to 8x

c(x), if for every given numeral n we have already

proved that

c(n).

Such an extension of PA allows that we conclude from (a) to (b),

and the consistency proof for PA works. The proof works, though, only at the expense
of accepting a version of the

o-rule. In other words, the purportedly ®nitist nature of

TI[

] could at best be justi®ed by appeal to the supposed ®nitist character of an

rule. We think, however, that the supposed ®nitist character of an

o-rule would in

its turn resist conclusive justi®cation. Although Gentzen insists on a `®nitist’
interpretation of `all’, we fail to see that he has succeeded in justifying trans®nite
induction up to

as a ®nitistically indisputable method of proof. Later, it will

emerge that this applies mutatis mutandis to Hilbert and Bernays (1939) when the
authors come to consider Gentzen’s consistency proof.

While Gentzen fails to adduce a persuasive argument for his claim that trans®nite

induction up to

is a ®nitistically legitimate form of inference, Hilbert and Bernays,

in the second volume of Grundlagen der Mathematik, seem to take a wavering attitude
towards the issue whether trans®nite induction up to

is ®nitary or not. Recall in this

context that in his essay `Hilbert’s Untersuchungen uÈber die Grundlagen der
Arithmetik’ Bernays (1935) had expressed the belief that the method applied by
Gentzen in his (®rst) consistency proof of PA meets the fundamental requirements
of the ®nitist point of view. By contrast, in his introduction to the second volume
of Grundlagen der Mathematik, Bernays refrains from claiming that trans®nite
induction as used by Gentzen and Ackermann is a ®nitistically permissible means
of proof.

One example for the seeming indecision of Hilbert and Bernays (1939)

regarding trans®nite induction is this. In the course of discussing Gentzen’s ®rst
consistency proof at the end of

}5 (entitled `The reason for extending the

methodic framework of proof theory’), they make a remark on Ackermann’s
consistency proof in his 1940 paper which is not free from ambiguity (385,
footnote 2). It is pointed out that the proof method resting on Hilbert’s

symbol `does not yet provide the desired result with ®nitary methods [our
emphasis]’. Ackermann is said to have succeeded in extending this proof method

46 That it is this second option which Gentzen may have had in mind is supported by the following

quotation: `The in®nite totality of the numbers smaller than 0,2 is transcended by one single idea:
the proof can be extended arbitrarily far into this totality; hence, it may be considered to be
completed for the entire totality’ Gentzen (1936, 558[195]). To be sure, we have a non sequitur
here; we are, furthermore, left in the dark as to the precise meaning of the word `may’ in this
speci®c context.

47 He does, however, claim that (already) in the light of Gentzen’s consistency proof one may maintain

that the `temporary ®asco’ of proof theory was due only to an exaggeration of the methodic
requirements that were made on it. As to the `exaggeration’ of the methodic requirements that were
made on proof theory, we do not share Bernays’s opinion. If in Hilbert and Bernays 1939 the
`philosophical’ foundations of proof theory were re¯ected to an extent matching Hilbert’s seminal
articles between 1922 and 1928, it would emerge that it is only the `high demands’ made or
limitations imposed on metamathematical reasoning that might guarantee its security. And security
and reliability of metamathematical reasoning clearly formed a key idea of Hilbert’s original
programme.

152

Matthias Schirn and Karl-Georg Niebergall

to a consistency proof for PA by applying induction up to

. One may be inclined

to make this more explicit thus: by applying a non-®nitary method, namely
induction up to

. But do Hilbert and Bernays really want to suggest this?

they do, they might have some trouble reconciling this with the other remarks
they make in connection with trans®nite induction. We shall return to their
assessment of trans®nite induction in due course.

In Hilbert and Bernays 1939, there is in fact a shift of emphasis. The philosophical

background of metamathematics plays a comparatively minor role. The
considerations relating speci®cally to issues of ®nitism are less of a piece, and they
lack both the drive and the pioneer spirit so characteristic of Hilbert’s classical
papers on proof theory. The prevailing idea is now that consistency proofs are
actually carried out; it seems to be of secondary importance to re¯ect thoroughly
on their ®nitist admissibility. The word `®nitist’ is still there, and indeed used
frequently, but it seems to have lost much of its former genuine impact on
metamathematical reasoning. By contrast, the labels `®nitist point of view’ and
`®nitist attitude’ have almost disappeared, and this is perhaps no accident.

At any

rate, whenever the authors speak of `®nitist statement’, `®nitist interpretation’ ,
`®nitist consistency proof’, `®nitist methods’, etc. they do so without appeal to
Hilbert’s classical texts. We are thus left in the dark as to how the new `®nitist’
perspective relates to the old one. Or should we take this as a symptom indicating
that the old perspective has been completely abandoned or no longer plays any role?

Be this as it may, it is fair to say that the reader of Grundlagen der Mathematik

(1939) still encounters a number of scattered remarks which seem to square pretty
well with the characterization of the ®nitist point of view, say, in `UÈber das
Unendliche’. We are told, for example, that `the truth-value of a logical function
for a given system of arguments is, in general, nothing that is ®nitistically
determined, since in the de®nition of the logical function totalities and existential
speci®cations may go in’ (Hilbert and Bernays 1939, 197f.). As to the ®nitist
interpretation of the quanti®ers, we are referred to the account in Hilbert and
Bernays (1934, 32) which we discussed earlier. We learn, moreover, that a
realization in the ®nitist sense cannot be related to a merely supposed domain of
objects, but only to an intuitively determined class of objects (Hilbert and Bernays
1939, 198). Much later (cf. Hilbert and Bernays 1939, 358), it is said that a ®nitist
assumption always relates to an intuitively characterized situation and that the
truth of a general sentence cannot be thought to be such a situation. So much for
the remnants of Hilbert’s original approach or what seem to be such.

Perhaps most of what has been said so far suggests that proof theory or

metamathematic s in the sense of Hilbert and Bernays (1939) is by no means the
same as the original ®nitist metamathematics M. In what follows, we shall try to
®nd out what Hilbert and Bernays (1939) regard as the limits of the ®nitistically
admissible. It will emerge that they are prepared to abandon tacitly one or the
other rationale of Hilbert’s ®nitism of the 1920s, as long as this paves the way for
proving the consistency of more extensive parts of mathematics. The most
important remarks on the problem of neatly segregating the ®nitistically admissible
from the ®nitistically inadmissible and, in particular, on the language of ®nitist

48 In his Preface to the second edition of Grundlage n der Mathematik (1970), however, Bernays recognizes

explicitly that trans®nite induction is the only non-®nitary means applied in Ackermann’s proof.

49 See the use of `®nitist point of view’ on pages VII, 197f., 200.

Extensions of the Finitist Point of View

153

(meta-)mathematic s as well as on the range of ®nitistically permissible modes of
inference can be found in

}5.2 and in }5.3 (Hilbert and Bernays 1939, 302ff. and

353ff.). Let us consider the relevant details.

}5.2 of Hilbert and Bernays (1939), entitled `The formalized metamathematics

of the number-theoreti c formalism’ (cf. 302ff.), the authors introduce a notational
variant of PA which they call Z

. Its purported drawback for metamathematica l

purposes rests on the fact `that in the formalizations of ®nitist reasoning in the
system (Z

) the characteristic of the ®nitist argumentation is, for the most part,

lost’ (1939, 361). Nonetheless, Z

is regarded as setting a provisional upper limit for

a ®nitistically acceptable metatheory (cf. Hilbert and Bernays 1939, 353ff., 361ff.).

At the beginning of the section `Eliminability of the ``tertium non datur’’ for the

investigation of the consistency of the system (Z)’, Hilbert and Bernays observe
that the `proof-theoretic methods hitherto applied (by them), even though they
partially go beyond the domain of recursive number theory, apparently do not
transcend the domain of those concept formations and modes of inference that can
still be presented within the formalism Z

’ (Hilbert and Bernays 1939, 361).

the face of it, this passage suggests that Hilbert and Bernays are here operating
with a twofold notion of extending proof-theory or metamathematics : the extension
involves both the language of metamathematic s and the metamathematica l theory
itself. Unfortunately, they do not distinguish clearly betweeen these two methods of
extending metamathematics ; their respective remarks give rise to ambiguity.

Hilbert and Bernays sketch, in the ®rst place, an extension L

‡
PRA

of L

PRA

which is

supposed to contain only `®nitary’ statements. Taking L

PRA

as the starting point,

‡
PRA

is arrived at in two stages: ®rst, symbols for certain computable number-

theoretic functions are adjoined to L

PRA

(call the set of formulae thereby de®ned

PRA

). Second, L

PRA

is converted into L

‡
PRA

by way of adding to L

PRA

only those

statements that can be `interpreted in a strict sense’ by a statement of L

PRA

(cf.

Hilbert and Bernays 1939, 362). Hilbert and Bernays do not explain the phrase
`interpreted in a strict sense’, but their ensuing exposition suggests that it is at least
formulae of the type `8x9y

c(x,y)’ with quanti®er-free formula c that are capable

of being `interpreted in a strict sense’ in L

PRA

. The interpretation can be given by

choosing for such a `8x9y

c(x,y)’ the quanti®er free-formula `c(x,f(x))’ in L

PRA

where f is a function-sign for a recursive function which has already been
introduced in L

PRA

. That these two formulae are equivalent to one another in some

sense of `equivalent’ is suggested by the phrase `strict interpretation’, but the
authors do not argue for this `equivalence’.

We observe that in Hilbert and Bernays 1939 the authors pass easily from the

determination of what is ®nitistically formulable to a characterization of what is
®nitistically provable. We are told that for the formalization of certain general
results of proof theory it is desirable to obtain as metamathematica l theorems
conditionals containing a universally quanti®ed sentence as antecedent (Hilbert and
Bernays 1939, 358, 362). Such sentences are for example (formalizations of)
assertions concerning the unprovability or veri®ability of formulae or the
computability of functions. To illustrate the idea, Hilbert and Bernays sketch a

50 The authors also argue that the proof-theoretical methods have been extended from PRA to PA without

infringing the `methodic fundamental idea of ®nitist proof theory’ (1939, 362).

51 Obviously, the conception of the ®nitistically admissible presented in this example is akin to the position

Hilbert and Bernays advocate in 1934, but deviates from Hilbert’s ®nitism in the 1920s. The truly
original, austere notion of a ®nitary statement embodies less than what can be expressed in L

‡
PRA

154

Matthias Schirn and Karl-Georg Niebergall

formalization of the informal consistency proof for H in Grundlagen der Mathematik
(1934), to which we have already referred in

}2. The formalization is carried out in PA,

and it is shown by means of a complexity analysis that a fragment of PA, though
extending PRA, would actually suf®ce for the consistency proof. Proof-theoretic
means extending PRA, including a form of complete induction which cannot be
formalized by the induction schema of recursive number theory (Hilbert and
Bernays 1939, 358), are said to be useful or desirable for conducting certain formal
consistency proofs.

However this may be, the crucial question for Hilbert and Bernays is whether the

so-called ®nitary methods may go beyond the scope of the modes of inference
formalizable in Z

. The question is said to lack a precise formulation, on the

grounds that `®nitary’ has not been introduced as a sharply de®ned term, but only
as a label for a `methodic guideline’. It serves merely to recognize certain forms of
concept formation and of inference de®nitely as ®nitary and certain others
de®nitely as non-®nitary. It is not appropriate, though, for drawing an exact
dividing line between modes of inference which meet the requirements of the ®nitist
method and modes of inference which do not.

It is in this connection that Hilbert and Bernays mention a typical borderline-case; it

concerns the question whether conditionals with a universally quanti®ed sentence as
antecedent can be formulated ®nitistically. They claim to have removed this
indeterminacy by distinguishing between sentences and inference rules (Hilbert and
Bernays 1939, 358f., 361). Hilbert and Bernays admit, though, that in some cases this
distinction may strike us as forced, and all this is said to require that the bounds of the
®nitist framework hitherto established be somewhat loosened, that is, that we go
beyond what can be formulated in L

‡
PRA

and proved in recursive number theory.

Two comments on these and similar remarks and ideas in Hilbert and Bernays

(1939) are in order here. First, what the authors may make clear with them is at
best that, compared with Hilbert’s ®nitism of the 1920s, the language of ®nitist
metamathematic s must be extended; for instance, unbounded quanti®cations
should now be ®nitistically formulable. Yet Hilbert and Bernays do not even
address the issue why in that case all theorems of PA should be sound from a
®nitist point of view. Moreover, remarks to the extent that it is useful or desirable
that the language of metamathematics has a certain expressive power and that the
metamathematical theory itself includes a certain repertoire of proof-theoretic
means convey nothing about the assumed ®nitary character of both the
metamathematical language and the metamathematica l theory under consideration.

Second, Hilbert’s and Bernays’s remarks presented above suggest that the old

foundational view dominating the pre-GoÈdelian period of Hilbertian proof theory
has been replaced with a view like this: we are accustomed to certain informal
metamathematical considerations, and experience teaches us that they can be
formalized in PA. Hence, we are entitled to use them in metamathematica l
reasoning. Whether Hilbert and Bernays do not care any longer much about
questions of ®nitist justi®ability, or whether they leave their readers with a principle
of the following kind: what is not de®nitely in®nitistic may be regarded as ®nitist,
remains unclear. Deplorably, this is not the only place where Hilbert and Bernays

52 We think that in Hilbert’s classical papers the expression `®nitary’ is much less vague than in Grundlagen

der Mathematik (1939). In spite of its vagueness both during the pre-GoÈdelian and post-GoÈdelian period
of Hilbertian proof theory, it is reasonable to say that it had undergone a thorough shift of meaning by
1939.

Extensions of the Finitist Point of View

155

hedge instead of putting their cards on the table. Surely Hilbert, as the founder of the
®nitist point of view, should feel called upon to give a clear-cut explication of `®nitist’
allowing a fair assessment of his programme. So, it could seem that the appeal to the
alleged inde®nability of `®nitist’ is meant to serve as a safeguard against possible
objections. This may come out a little clearer in Hilbert’s and Bernays’s treatment
of trans®nite induction to which we now turn.

Possibly guided by some principle of the kind just mentioned and the desire to be

able to formalize metatheoretical considerations to as high a degree as possible,
Hilbert and Bernays arrive at PA (or Z

, respectively) as a provisional boundary

within which a ®nitist metatheory may be developed (1939, 354, 361). The crucial
question for Hilbert and Bernays is now whether the so-called ®nitary methods
may go beyond the scope of the modes of inference formalizable in Z

. (Remember

that, owing to the vagueness of the word `®nitary’, they do not consider this
question to be formulated in precise terms.) For, as they point out (1939, 353f.), a
(formal) metamathematica l consistency proof for PA cannot be carried out in PA
itself. Nevertheless, Hilbert and Bernays do not rest content with the idea that there
can be no ®nitary consistency proof for PA. Accordingly, they insist that `in any
case, it is possible [ . . .] to surpass the modes of inference formalizable in (Z

)

without using the typically non-®nitary inferences. And in this way we succeed in
giving a very simple consistency proof for the system (Z)’ (1939, 362). Hilbert and
Bernays refer in this connection to an arithmetical version of trans®nite
induction.

The line of thought which leads them eventually to considering

trans®nite induction, in particular up to

, as a possibly `legitimate’ method of

proof theory deserves close attention.

In a preliminary step, Hilbert and Bernays introduce a version of Heyting

arithmetic (HA) (1939, 362ff.; cf. Heyting 1930). They claim to have proved, in a
completely ®nitist fashion (1939, 371), that a contradiction in PA would entail one
in HA. This claim holds indeed, because what we are given is an argument for
PA ` Con

!Con

, and, as we already know, everything provable in PA is

considered to be ®nitistically provable by Hilbert and Bernays in Grundlagen der
Mathematik (1939).

In order to obtain a consistency proof for PA, the

consistency of HA must then, of course, be proved ®rst. Hilbert and Bernays
regard this as less dif®cult in the case of HA than in the case of PA, because unlike
PA, HA does not prove the law of excluded middle.

The ®rst consistency `proof’ for HA is carried out `contentually’ (Hilbert and

Bernays 1939, 373). Hilbert and Bernays observe that by using a contentual notion
of inference they abandon completely Hilbert’s `methodic idea of proof theory’
(1939, 372). Trans®nite induction up to

offers itself as a way out of this

predicament. It does so, because even if TI[

] is restricted to

-formulae and in

this version adjoined to PA or (QF-IA), it in fact proves the consistency of PA. The
pivotal question whether TI[

] can be accepted as a ®nitist form of inference is not

given a clear answer, however.

Although Hilbert and Bernays concede that they

are unable to provide a clear clue as to which extensions are still admissible, they

53 Therefore the remark just quoted seems to suggest that PA+TI[

] could be treated as a ®nitistically

admissible theory.

54 Since we assume that the formalization MM of Hilbert’s ®nitist metamathematics of the 1920s ought to

be a proper subtheory of PRA, it cannot be taken for granted that MM suf®ces for carrying out the
relative consistency proof mentioned above.

55 In fact, Hilbert and Bernays 1939 formulate TI[

] as a rule of inference.

156

Matthias Schirn and Karl-Georg Niebergall

suggest, in the same breath, that certain forms of trans®nite induction ought to be
construed as ®nitary. They even attempt to provide two `reasons’ for accepting
TI[

] as a ®nitistically admissible method of proof. The ®rst relates to the PA-

provability of arbitrarily good approximations of TI[

]. It is taken from Gentzen

(1936) and has already been discussed and rejected by us.

The second consideration is this. Hilbert and Bernays (1939, 376) call attention to

what they describe as a `deviation from the procedure of the ®nitist conduct of proof
hitherto adopted’: the mode of inference of trans®nite induction may contain
universally quanti®ed sentences as premises. Thus, the idea of strengthening the
proof-theoretic resources by including trans®nite induction seems to ®t the
framework hinted at in Hilbert’s and Bernays’s earlier re¯ections on the need of
extending the limits of ®nitist considerations (cf. 1939, 362). Should we, for this
reason, assume that the extension by trans®nite induction must be considered
®nitary? The answer is `no’. What Hilbert and Bernays (1939, 362) discuss here is
rather the language of metamathematics , which can be regarded as a de®nitional
extension of the language of PA. Such discussion does not, of course, settle the
question which theory formulated in this language encompasses only ®nitist means.
But this is precisely at issue in the case of trans®nite induction.

At the very end of the last chapter of Grundlagen der Mathematik (1939), Hilbert

and Bernays make a concluding (but convoluted) remark on Gentzen’s (1936)
consistency proof, which suggests that is was no longer their serious concern to
argue for the ®nitist nature of the proof-theoretic means applied in consistency
proofs for mathematical theories they consider important. We are told that it is a
consequence of GoÈdel’s Theorem that

the more comprehensive the formalism to be considered is, the higher are the order
types, i.e. forms of the generalized induction principle, that must be used. [ . . .] The
methodic requirements for the contentual proof of that higher induction principle
supply the standard for [determining] which kind of methodic assumptions must
be taken as a basis for the contentual attitude, if the consistency proof for the
formalism in question is to be successful. (Hilbert and Bernays 1939, 387)

Two possible interpretations come to mind. First, whenever in PA+TI[

a] the

consistency of an important mathematical theory S is provable, TI[

a] is a

®nitistically permissible technique. Second, in order to be able to carry out
consistency proofs for stronger theories (such as Z

), a higher form of trans®nite

induction is required. Whether the latter is ®nitistically admissible is of no concern.
We submit that according to each of the two interpretations Hilbert’s original
®nitist point of view has been relinquished. Moreover, in this particular case it is
far from clear what the phrases `methodic requirements’ and `methodic
assumptions’ are supposed to mean here and why we should attach special
importance to them.

However this may be, there is at least one place in Grundlagen der Mathematik

(1939) where Hilbert and Bernays expressly maintain that a considerable portion of
the theory of trans®nite ordinals can still de®nitely be treated with ®nitary methods
(1939, 373). For this reason, the term `trans®nite induction’ is said to be misleading
with respect to the `methodic distinctions’ made by the authors (1939, 373). It is
still used (cf. Hilbert and Bernays 1939, 376, 382), but for the most part replaced
with `generalized induction principle’. There is residual concern, however. What

Extensions of the Finitist Point of View

157

exact portion do the authors have in mind when they speak of a considerable portion?
Do they mean to appeal only to (notations of) ordinals below

? Or are they toying

with the idea that trans®nite induction up to

and higher ordinal numbers might still

be within the bounds of ®nitary methods?

These questions do not allow for simple answers, especially since Hilbert and

Bernays do not tackle them in a straightforward manner. We must rather rely here
on hints which we may assess from the viewpoint of modern proof theory. Let us
then do this.

Hilbert’s and Bernays’s view that consistency `proofs’ for HA (or PA) which rest

on a contentual notion of truth must be considered in®nitistic, might serve as a clue.
When suitably formalized, such a consistency proof will naturally involve the use of a
formalized truth or satisfaction predicate for the formulas of L[HA]. If that is granted,
then the view under discussion seems to suggest that theories in which we prove the
consistency of PA by employing a formalized truth de®nition are likewise to be
regarded as ®nitistically inadmissible.

Consider now the following thesis:
(*) If T is a theory in which the consistency of PA is provable by employing a
formalized truth-predicate, then T is ®nitistically inadmissible.
A suitable example of such a `truth-formalizing ’ theory is T:= (

-CA)+(

IA) (cf. Takeuti 1975, 158ff.). T is a weak fragment of Z

; its restriction to L

is a

subtheory of PA+TI[

]. Admittedly, it would be anachronisti c to grant that

Hilbert and Bernays (1939) knew this result. However, assuming (with good
reason) that they had a clear idea about the in®nitistic nature of `truth-formalizing ’
theories, it seems unlikely that they would have considered T to be a ®nitistically
admissible theory. Be this as it may, (*) does imply that T is ®nitistically
inadmissible. Returning to our question `What exact portion do Hilbert and
Bernays have in mind when they speak of a considerable portion?’, two possible
answers suggest themselves: (a) the restriction of T to L

is considered inessential,

that is, PA+TI[

] is considered in®nitistic, and

is, therefore, taken as a limit

for ®nitistically admissible ordinal numbers; and (b) T owes its in®nitistic character
essentially to the fact that it is stated in a second-order language, that is, that in L

we may quantify over in®nite objects. This leaves room for the possibility of
construing PA+TI[

] as a ®nitistically acceptable theory.

In Grundlagen der Mathematik (1939), adjoining the schema of trans®nite

induction to the ®nitistically accepted base theory PA is regarded as the most
important method of carrying out ®nitist consistency proofs for formalized
mathematical theories T. This means that Hilbert and Bernays would be well-
advised to jettison (a). Due to a suitable version of GoÈdel’s Second Incompleteness
Theorem, it follows from (a) that a ®nitist consistency proof for Z

(or weak

fragments thereof) in which we use trans®nite induction is bound to fail. At ®rst
glance, to accept option (b) instead of (a) might be a better choice for Hilbert and
Bernays. Still, in doing so, they would have to advance an argument designed to
convince us that the ®rst-order portion T

of the in®nitistic theory T is ®nitistically

admissible. It seems to us that such an argument is not forthcoming. It presupposes
that we are capable of grasping interpretations of T and T

. But how should we be

able to bring this about for T

in a ®nitist fashion, given that T is supposed to be

an in®nitistic theory?

One might object that the issue whether certain forms of trans®nite induction are

®nitistically admissible is after all of little importance, because a consistency proof for

158

Matthias Schirn and Karl-Georg Niebergall

the entire body of mathematics by applying trans®nite induction is doomed to failure
right from the start. And we know, of course, that the principal objective of Hilbert’s
programme in the 1920s was to establish the entire heritage of classical mathematics
by means of a metamathematical consistency proof meeting the requirements of
reliability and indisputability. It is worth noting in this context that in his
introduction to the second volume of Grundlagen der Mathematik, Bernays is
requiring less of proof theory than Hilbert in effect required of it in the 1920s.

There Bernays observes that the fate of proof theory will ultimately depend on the
viability or failure of a metamathematical consistency proof for analysis (i.e. Z

Although we cannot conduct a consistency proof for Z

in PA, for example, we

might succeed in carrying it out by using trans®nite induction. However, we cannot
do this in a ®nitistically admissible fashion if (*) and (a) obtain.

At the end of the day, what then is the range of the ®nitistically admissible in

Grundlagen der Mathematik (1939)? Speculations aside, we can only say that it
encompasses at least PA, but we also know by now that it could be wider, much
wider indeed.

Reading through Hilbert and Bernays 1939, one cannot help feeling that the former

ideals of ®nitism have fallen victim to sheer proof-theoretic pragmatism, whence comes
the heading of this section. Undoubtedly, some price had to be paid in the face of GoÈdel’s
theorems. But was it the right one for Hilbert? Non-axiomatized metamathematics has
been replaced with an axiomatized version, and the intuitive down-to-earth `modes of
inference’ of informal metamathematics have given way to the loftier ones of a
formalized metatheory. The virtues of the formerÐintuitive evidence and
unquestionable soundnessÐhave disappeared in the latter. This change of perspective
is in no way to be condemned, of course. There seems to be a trace of indecision in
Hilbert and Bernays (1939), however. The new `®nitist’ parameters are kept ¯exible
(too ¯exible, we think) to make allowances for special proof-theoretic needs which in

56 On the face of it, Hilbert 1934 seems to proclaim his original proof-theoretic objective in his introduction

to Grundlagen der Mathematik. There he writes that the ®nal goal of further investigations in proof
theory is to recognize the totality of our usual mathematical methods as consistent. The phrase `the
totality of our usual mathematical methods’ is presumably meant to refer to classical mathematics in
its entirety.

57 Hilbert and Bernays (1939, Supplement IV) show that Z

is perfectly adequate for the formal

development of classical analysis.

58 The method, applied by Hilbert and others, of extending or strengthening the metamathematical

resources suffers from a well-known weakness. According to GoÈdel’s Second Incompleteness
Theorem, the theory T in which we prove the consistency of the theory T

’ must be `stronger’ than T’,

at least if both T and T

’ are recursively enumerable mathematical theories interpreting rather weak

theories like PRA. (As regards the use of the word `stronger’ in a context like this, see the detailed
comments in Niebergall and Schirn, `Hilbert’s programme and GoÈdel’s theorems’ (forthcoming).)
Thus, we cannot give a consistency proof within metamathematics for mathematics in its entirety, if
the former is taken to be a fragment of the latter. If we regard a metamathematical theory T which
proves `Con

’, for example, as a part of mathematics proper, we are bound to prove the consistency

of T itself (assuming that T is consistent). Plainly, if T is recursively enumerable, we need a theory
that is stronger than T in order to get the consistency proof for T off the ground. Assuming that
such a theory is recursively enumerable, the same problem arises anew, and so it goes on. In short,
whether we wish to prove the consistency of all of mathematics in a subtheory of that global theory
or whether we wish to prove the consistency of those metamathematical theories in which we have
carried out consistency proofs, the dif®culty of ®nding or constructing a metamathematical theory in
which we could do this appears to be insuperable.

59 We must leave a discussion of GoÈdel’s approach in his article `UÈber eine bisher noch nicht benuÈtzte

Erweiterung des ®niten Standpunktes’ (1958) to another occasion. In our view, his use of primitive
recursive functionals of higher type cannot be regarded as a reliable and indisputable proof-theoretic
method in the sense of Hilbert’s original ®nitist point of view.

Extensions of the Finitist Point of View

159

their turn have nothing to do with any reasonable form of ®nitism. Obviously, the
authors cannot have it both ways, that is, they cannot make metamathematics at least
as strong as PA or even much stronger than PA and, in the same breath, advocate a
version of ®nitism deserving of its name. And we think that they should have left no
doubt about this. In Grundlagen der Mathematik (1939), philosophical re¯ections on
the nature of ®nitist metamathematica l reasoning more or less come to grief. In this
sense, then, it seems to us that the book hardly bears comparison with Hilbert’s
classical papers on proof theory, however ingenious its technical achievements and
however considerable its impact on subsequent developments in metamathematics
may have been.

References

Ackermann, W. 1925. `BegruÈndung des ``tertium non datur’’ mittels der Hilbertschen Theorie der Wider-

spruchsfreiheit’, Mathematische Annalen 93, 1±36.

Ackermann, W. 1940. `Zur Widerspruchsfreiheit der Zahlentheorie’, Mathematische Annalen 117, 162±194.
Bernays, P. 1930. `Die Philosophie der Mathematik und die Hilbertsche Beweistheorie’, BlaÈtter fuÈr

Deutsche Philosophie 4 (1930±1931), 326±267; with a postscript reprinted in Bernays 1976, 17±61.

Bernays, P. 1935. `Hilberts Untersuchungen uÈber die Grundlagen der Arithmetik’, in Hilbert 1935, 196±

216.

Bernays, P. 1967. `Hilbert, David’, in P. Edwards, ed. Encyclopedia of Philosophy, Vol. 3, New York: Mac-

Millan and Free Press, pp. 496±504.

Bernays, P. 1976. Abhandlunge n zur Philosophie der Mathematik, Darmstadt: Wissenschaftliche Buchge-

sellschaft.

Detlefsen, M. 1979. `On interpreting GoÈdel’s second theorem’, Journal of Philosophical Logic 8, 297±313.
Detlefsen, M. 1998. `Constructive existence claims’, in Schirn 1998, 307±335.
Feferman, S. 1960. `Arithmetization of metamathematics in a general setting’, Fundamenta Mathematicae

XLIX, 35±92.

Feferman, S. 1986. `Introductory note to 1931c’, in S. Feferman, ed., Kurt GoÈdel: Collected Works, vol. I,

Oxford: Oxford University Press.

Gentzen, G. 1936. `Die Widerspruchsfreiheit der reinen Zahlentheorie’, Mathematische Annalen 112,

493±565 [English translation `The consistency of elementary number theory’ in Gentzen 1969,
132±201].

Gentzen, G. 1938. `Neue Fassung des Widerspruchsfreiheitsbeweises fuÈr die reine Zahlentheorie’, For-

schungen zur Logik und zur Grundlegung der exakten Wissenschaften 4, 19±44 [English translation
`New version of the consistency of elementary number theory’ in Gentzen 1969, 252±286].

Gentzen, G. 1969. The Collected Papers of Gerhard Gentzen, M. E. Szabo ed., Amsterdam: North-Holland.
Girard, J.-Y. 1987. Proof Theory and Logical Complexity vol. 1, Naples: Bibliopolis.
GoÈdel, K. 1931. `UÈber formal unentscheidbare SaÈtze der Principia Mathematica und verwandter Systeme

I’, Monatshefte fuÈr Mathematik und Physik 38, 173±198.

GoÈdel, K. 1958. `UÈber eine bisher noch nicht benuÈtzte Erweiterung des ®niten Standpunktes’, Dialectica

12, 280±287; reprinted with english translation `On a hitherto unutilized extension of the ®nitary
standpoint’, in S. Feferman ed. Kurt GoÈdel: Collected Works, vol. I, Oxford: Oxford University Press,
pp. 240±251.

HaÂjek, P. and Pudlak, P. 1993. Metamathematics of First-Order Arithmetic, Berlin: Springer-Verlag.
Heijenoort, J. van (ed.) 1967. From Frege to GoÈdel, A Source Book in Mathematical Logic, 1879±1931,

Cambridge, MA: Harvard University Press.

Herbrand, J. 1931. `Sur la non-contradiction de l’arithmeÂtique’, Journal fuÈr die reine und angewandte Mathe-

matik 166, 1±8 [English translation `On the consistency of arithmetic’, in van Heijenoort 1967, 618±628].

Heyting, A. 1930. `Die formalen Regeln der intuitionistischen Logik’, Sitzungsberichte der preuûischen Aka-

demi der Wissenschaften, Phys.-Mathematische Klasse II, 42±56.

Hilbert, D. 1899. Grundlage n der Geometrie, Leipzig: Teubner, seventh revised and enlarged edition 1930.
Hilbert, D. 1922. `NeubegruÈndung der Mathematik’, Erste Mitteilung, Abhandlunge n aus dem Mathema-

tischen Seminar der Hamburger UniversitaÈt 1, 157±177; reprinted in Hilbert 1935, 157±177.

Hilbert, D. 1923. `Die logischen Grundlagen der Mathematik’, Mathematische Annalen 88, 151±165; rep-

rinted in Hilbert 1935, 178±191.

Hilbert, D. 1926. `UÈber das Unendliche’, Mathematische Annalen 95, 161±190; reprinted in Hilbert, D.

Hilbertiana, Wissenschaftliche Buchgesellschaft, Darmstadt, 1964, 79±108 [English translation `On
the in®nite’, in van Heijenoort 1967, 367±392].

160

Matthias Schirn and Karl-Georg Niebergall

Hilbert, D. 1928a. `Die Grundlagen der Mathematik’, Abhandlunge n aus dem Mathematischen Seminar der

Hamburger UniversitaÈt 6, 65±85; abbreviated version reprinted as appendix IX in the seventh edition of
Hilbert 1899, 289±312 [English translation `The foundations of mathematics’, in van Heijenoort 1967,
464±479].

Hilbert, D. 1928b. `Probleme der Grundlegung der Mathematik’, Atti del Congreso nazionale dei matema-

tici, Bologna 3±10 settembre 1928, 1, 135±141; with supplementations reprinted in Mathematische An-
nalen 102 (1929) 1±9, and as appendix X in the seventh edition of Hilbert 1899, 313±323.

Hilbert, D. 1931. `Die Grundlegung der elementaren Zahlenlehre’, Mathematische Annalen 104, 485±494.
Hilbert, D. 1935. Gesammelte Abhandlungen , III, Berlin: Springer-Verlag, second edition 1970.
Hilbert, D. and Bernays, P. 1934 Grundlagen der Mathematik I, Berlin: Springer-Verlag, second edition

with modi®cations and supplementations, 1968.

Hilbert, D. and Bernays, P. 1939. Grundlagen der Mathematik II, Berlin: Springer-Verlag, second edition

with modi®cations and supplementations, 1970.

IgnjatovicÂ, A. 1994. `Hilbert’s program and the omega-rule’, The Journal of Symbolic Logic 59, 322±343.
Isaacson, D. 1992. `Some considerations on arithmetical truth and the

o-rule’, in M. Detlefsen (ed.), Proof,

Logic and Formalization, London: Routledge & Kegan Paul, pp. 94±138.

Kaye, R. 1991. Models of Peano Arithmetic, Oxford: Oxford University Press.
Neumann, J. von. 1927. `Zur Hilbertschen Beweistheorie’, Mathematische Zeitschrift 26, 1±46.
Niebergall, K.G. and Schirn, M. 1998. `Hilbert’s ®nitism and the notion of in®nity’, in Schirn 1998, 271±

305.

Parsons, C. 1998. `Finitism and intuitive knowledge’, in Schirn 1998, 249±270.
Rose, H.E. 1984, Subrecursion, Oxford: Oxford University Press.
Schirn, M. (ed.). 1998. The Philosophy of Mathematics Today, Oxford: Oxford University Press.
Sieg, W. 1985. `Fragments of arithmetic’, Annals of Pure and Applied Logic 28, 33±72.
Smorynski, C. 1977. `The incompleteness theorems’, in J. Barwise (ed.), Handbook of Mathematical Logic,

Amsterdam: North-Holland, pp. 821±865.

Tait, W.W. 1981. `Finitism’, The Journal of Philosophy 78, 524±546.
Takeuti, G. 1975. Proof Theory, Amsterdam: North-Holland; second enlarged edition 1987.

Extensions of the Finitist Point of View

161

Wyszukiwarka

Podobne podstrony:
Evil from a theologians point of view
GONDA Ancient indian kingship from the religious point of view
Ilona Andrews [Kate Daniels] Curran s Point of View Volume 1 (rtf)
Anthony, Piers Xanth 13 Isle of View
Phantom Of The Opera The Point Of No Return
Point of Hopes Lisa A Barnett
Gene Wolfe At the Point of Capricorn
America At The Point Of No Return!
9 The Point Of No Return
Point of Ignition Erin Dutton
tekst piosenki The Point Of No Return
The Point Of No Return nuty
Piers Anthony Xanth 13 Isle of View
mapi com The Ayurvedic View of Marijuana
Freud View On The Nature Of Man
Candide Voltaire's Opposing View of Optimism in the World
The crime of bad Power Point and how to avoid it

więcej podobnych podstron