What Finitism could not be.

SUMMARY: In his paper "Finitism" (1981), W.W. Tait maintains that the chief difficulty for everyone who wishes to understand Hilbert's conception of finitist mathematics is this: to specify the sense of the provability of general statements about the natural numbers without presupposing infinite totalities. Tait further argues that all finitist reasoning is essentially primitive recursive. In this paper, we attempt to show that his thesis "The finitist functions are precisely the primitive recursive functions" is disputable and that another, likewise defended by him, is untenable. The second thesis is that the finitist theorems are precisely the universal closures of the equations that can be proved in PRA.

KEY WORDS: finitist functions, primitive recursive functions, infinite totalities, finitist proof of the universal closure of an equation

1. Tait's Interpretation of Finitism

In his influential essay "Finitism" (1981), W.W. Tait sets himself the task (a) of explicating the notion of finitism by explaining a sense in which one can prove general statements about the natural numbers without assuming infinite totalities, and (b) of arguing for the thesis that all modes of finitist reasoning are essentially primitive recursive. Tait maintains that the significance of finitism is due to the fact that it is a minimal kind of reasoning presupposed by any nontrivial reasoning about the concept of number. In this sense, finitism is fundamental to mathematics, although Hilbert's attempt to found mathematics on finitism miscarries definitively, according to Tait (cf. Tait 1981, pp. 526, 540, 546).

In what follows, we try to show that one thesis advocated by Tait is questionable and another, likewise defended by him, indefensible. The thesis (Tait 1981, p. 533), "The finitist functions are precisely the primitive recursive functions" we call Tait's First Thesis. The thesis (Tait 1981, p. 537) "The finitist theorems are precisely the universal closures of the equations that can be proved in Primitive Recursive Arithmetic" (PRA) will be referred to as Tait's Second Thesis. (1)

At the outset of his paper, Tait attempts to pinpoint the main difficulty for everyone who wants to understand Hilbert's conception of finitist mathematics. He believes that this difficulty is embodied by the question as to how to specify the sense of the provability of general statements about the natural numbers without presupposing some infinite totality. Somewhat surprisingly, Tait does not distinguish explicitly between finitist mathematics and finitist metamathematics along the lines of Hilbert. When we talk of Hilbert's finitism, we ordinarily mean his finitist proof theory or metamathematics rather than what he takes to be the finitist portion of a formalized mathematical theory. As an example of a general statement, Tait chooses "[for all] xy(x + y = y + x)". This is a [[PI].sup.0.sub.1]-sentence (2) which appears to be a constituent of the language of formalized number theory rather than a sentence belonging to the (formalized or informal) language of metamathematics. We think that at this point Tait ought to have quoted a [[PI].sup.0.sub.1]-sentence whose formulability in the formalized language of metamathematics really counts for the proof theorist; "[Con.sub.pa]" would be an appropriate example. (3)

In any case, it seems to us that it would have been in Tait's own interest to set up the requirement that nontrivial finitist metamathematics be able to prove [[PI].sup.0.sub.1]-sentences (or [[PI].sup.0.sub.0]-formulae) without assuming some infinite totality. When he comes to describe a certain finitist framework for establishing some theses concerning finitist mathematics and PRA, he does so in terms of conditions which he himself regards as appropriate without being reasonably faithful to Hilbert. We thus face the question: Does Tait intend to present Hilbert's answer to his initial question concerning the finitist provability of general statements, or does he wish to give his own answer by endowing the term "finitism" with a sense which may be distinct from that one Hilbert attaches to it? To repeat: if we adopt Hilbert's finitist standpoint and if we wish to show [Con.sub.[tau]] for certain mathematical, axiomatizable theories T (with representation [tau]), we must clearly distinguish between finitist mathematics and (finitist) metamathematics. It is obvious that Tait, unlike Hilbert, considers metamathematics to be a formal mathematical theory. Thus, we ought to regard with reserve Tait's contention (1981, pp. 525f., 540, 546) that the only real divergence of his characterization of finitism from Hilbert's account concerns Hilbert's epistemological distinction between numbers and transfinite objects such as functions and sets in terms of representability in intuition. (4) For the present, we simply want to record that the only argument that Tait adduces in favour of the possibility of formulating finitistically [[PI].sup.0.sub.1]-sentences is this: it should be possible to establish the consistency of certain mathematical theories by finitist metamathematical means, and, thus, for Tait it should at least be possible to formulate consistency assertions [Con.sub.[tau]] metamathematically. (5)

Let us take a closer look at Tait's conception of finitism. He emphasizes that "finite" in "finitism" means precisely that all reference to infinite totalities should be rejected (Tait 1981, p. 524). It is not quite clear what the word "refer" is supposed to mean here. Two possible interpretations come to mind:

1. It is customarily held that the terms of Peano Arithmetic (PA) refer to natural numbers, and natural numbers are usually taken to be finite objects. This applies, of course, also to Robinson Arithmetic (Q) and likewise to theories like PA + TI[[alpha]], i.e. to the schema of transfinite induction in [L.sub.PA] up to [alpha] adjoined to PA. (6) In the sense considered here, these theories do not involve reference to infinite totalities.

2. PA is not satisfiable in any finite structure, just as PA + TI[[alpha]] or Q are not. Nevertheless, in a strict sense of "refer to", these theories do not refer to infinite totalities either. It seems more appropriate to say that they presuppose, assume or are committed to infinite totalities. In the context Tait is considering, he fails perhaps to distinguish terminologically between "to refer to" and "to presuppose". In one place (Tait 1981, p. 526), he says that he has analyzed a conception of reasoning about numbers which does not presuppose infinite totalities, not even the so-called potential infinities of intuitionistic mathematics. And he adds that his account well fits Hilbert's accounts of finitism.

In the end, it really does not matter whether we choose interpretation 1 or 2. Neither of them allows to distinguish between very weak subtheories and very strong extensions of PA and, thus, neither of them serves to distinguish neatly between finitist and non-finitist mathematics. Without providing suitable criteria, which enable us to fill this gap, the alleged affinity between Hilbert's and Tait's conception of finitism lacks a sound basis, however.

2. Finitist and Primitive Recursive Functions

In Section V of his 1981 paper, Tait argues that every primitive recursive function f : A [right arrow] B is finitist in the sense that the finitist can accept it as a construction of a B from an arbitrary A. (7) He then states what we referred to as Tait's First Thesis. Tait emphasizes that the thesis cannot be understood by the finitist since the notion of a function has no finitist meaning and, hence, the notion of a finitist function is not finitist either. Now, it is far from clear that from the fact that the finitist cannot understand the notion of a function qua transfinite object it follows that he cannot grasp the concept of a finitist function. If we strip Tait's mode of speaking of its epistemic implications, we may say that he concludes from the non-definability of a set X (in a certain context) to the non-definability of X [intersection] Y for any set Y (in the same context). We have doubts as to the correctness of this inference. (8)

In order to be able to tackle effectively the problem of whether it is legitimate, in the light of Hilbert's finitism of the 1920s, to identify the finitist functions with the primitive recursive functions, let us do some preparatory work and ask: Did Hilbert qua finitist mathematician believe in the existence of functions? To put it more explicitly: Did Hilbert qua finitist mathematician believe in the existence of entities which the classical mathematician, following by and large Tait's exposition of finitism, would call finitist functions? Various answers come to mind.

(i) No. For if functions existed, they would be transfinite objects, but, according to Hilbert, transfinite objects do not exist.

(ii) No. Yet we need not worry about their non-existence, because we are entitled to use function signs in theories which can be shown to be consistent with finitist means.

(iii) Yes, because like numbers functions are stroke-figures, and there can be no doubt about the existence of concrete, intuitable figures.

(iv) Yes, functions as abstract, transfinite objects do exist.

Although (i) may be correct, it strikes us as unsatisfactory. (i) certainly does not account for the fact that even the finitist as such is able to grasp contexts in which function signs occur. As to (iv), we feel inclined to reject it as incorrect. Several observations in Hilbert's texts speak in favour of the assumption that qua finitist he did not believe in the existence of functions as abstract, transfinite objects. (9)

Hilbert and Bernays (1934, p. 26) introduce "f: A [right arrow] B", in accordance with (ii), by means of a contextual definition. "f: A [right arrow] B" is just a shorthand expression for: "We are given a natural number (i.e. a numeral) [??]; then we determine f([??]) by computing f([??]-1), f([??]-1) by computing f([??]-2), etc. After [??]-1 steps we have determined f(1) and, in addition, shown how f([??]) is computed from f(1)." As to the finitist use of function signs, we could say that it is governed by a procedure given by some schema of computation. It seems clear that we cannot quantify metatheoretically over the procedure just characterized: function signs without argument-expressions do not even occur in the definiens. Thus, the proposed contextual definition does not presuppose the existence of f or of some other function. Rather, it bestows a meaning upon the entire context in which "f" occurs. (10) Surely, if a theory T designed to fix the use of a function sign "f" proves to be inconsistent, then we have not succeeded in bestowing a meaning upon "f". Hence, only when T is consistent should we assume that "f: A [right arrow] B" is defined in the way sketched above. So much to our comments on answer (ii).

Despite its appeal, (iii) might be deemed as a less plausible option than (ii). The reason is this. From the point of view of classical mathematics, there are uncountably many sets of natural numbers and uncountably many number-theoretic functions. Since the finitist (meta-)mathematician probably refuses to allow the postulation of uncountably many figures, he will not have enough figures at his disposal for "coding" all number-theoretic functions. We need not worry about this, however. The classical mathematician is likely to assume the existence of only countably many finitist functions or function signs. Due to Hilbert's identification of numbers with concrete figures (numerals), the introduction of the natural numbers already requires that there be countably many figures. Thus, countably many figures will suffice for coding or replacing the finitist functions.

So, it emerges that we can accept not only (ii), but also (iii) as a position that tallies closely with finitism concerning the existence of functions, in particular of finitist functions. Clearly, by accepting (iii) we make a concession to those who want to claim the existence of functions in a finitistically acceptable way, cost what it may. Still, from the point of view of a faithful interpretation of Hilbert's metamathematics we have a clear preference for (ii). While (ii) appears to be buttressed by the remarks of Hilbert and Bernays (1934) we referred to above, (iii) owes its plausibility to considerations by analogy.

How are we to assess Tait's First Thesis in the light of the preceding line of argument? The answer is simple: the primitive recursive functions cannot be the finitist ones. According to (ii), there are no finitist functions, and according to (iii), the primitive recursive and the finitist functions belong to distinct types of entities; the first are abstract mathematical objects, while the second are concrete figures. (11) There is even room for an additional argument. The primitive recursive functions, conceived of as sets of infinitely many tuples, are infinite objects in the ordinary set-theoretic sense. However, if the primitive recursive functions are transfinite objects, then, in the light of Tait's identification of the finitist functions with the primitive recursive ones, the former must be transfinite objects, too. Yet, on the face of it, to accept the finitist functions as transfinite objects appears incoherent.

If someone believes, in contrast to our own express opinion, that (iii) is to be preferred to (ii), he (or she) may still argue in favour of Tait's First Thesis. In a first step, he could code and then replace the primitive recursive functions with their indices, and in a second, identify these indices with stroke-symbols which coincide precisely with those figures that are the finitist functions in the sense of (iii). This procedure rests on the idea that the primitive recursive functions, even if they differ from the finitist ones, could still be reconstructed as finitist functions. Such a reconstruction would only require that both the finitist and the primitive recursive functions satisfy a set of certain characteristic conditions. Relative to the coding we just appealed to, it is possible, then, that primitive recursive and finitist functions are literally the same objects. It remains to be added that the primitive recursive functions qua stroke-figures are now conceived of as finite objects. The last objection raised to Tait's First Thesis therefore loses its force.

Nonetheless, we insist that even in this case it is mandatory to distinguish between finitist and primitive recursive functions. We want to argue for this claim by comparing the status of proofs in Hilbertian and in contemporary metamathematics and by drawing an analogy between the nature of proofs and the nature of functions considered from Hilbert's finitist standpoint. According to contemporary metamathematics, formalized proofs are sets and, hence, abstract mathematical objects over which we can quantify formally. For Hilbert, by contrast, formalized proofs are concrete and surveyable objects over which we cannot quantify formally. The Hilbertian metamathematician can only study and manipulate (e.g., shorten or lengthen) particular proofs qua figures; the finitistically acceptable codings must be given to our perceptual intuition. Analogously, from Hilbert's finitist point of view, we must have intuitive access to the finitistically acceptable codings of functions. If we are given a (finitist) function sign f, it is only for a previously given figure [??] that we can consider particular, concrete figures f([??]). And just as we cannot quantify formally over proofs qua figures, we cannot quantify formally over all arguments of a finitist function. We can, of course, do that for primitive recursive functions.

In the light of what has been said so far, Tait's First Thesis appears far from being well-founded. We are willing to concede that for those who are interested in a precise, purely mathematical definition of the notion of finitist function, it is not at all unfounded to reconstruct finitist functions as primitive recursive ones. It might even prove useful to do this. If we understand Tait's line of argument correctly, though, he does not have in mind any such reconstruction. It seems to us that his First Thesis is rather put forward as an explication of Hilbert's conception of a finitist function.

3. Finitist Theorems

We now turn more closely to what we take to be Tait's initial question: In what sense can one prove finitistically [[PI].sup.0.sub.1]-sentences without assuming infinite totalities? Tait (1981, p. 526) writes: "We wish to analyze the notion f : [for all] xF(x), that f is a finitist proof of [for all] xF(x), where x is a variable of some type A and F(x) is an equation between terms of some type B." It is important to be aware of the scope of the language in which these equations are formulated. We follow Tait in assuming that the language we call [L.sub.FIN] includes [L.sub.PRA]. In particular, equations may contain function symbols for arbitrary primitive recursive functions.

We observe that f is a function. This means that for Tait a finitist proof would be a function. In this respect, he clearly diverges from Hilbert's conception according to which formalized proofs are concrete figures. Furthermore, since Tait regards functions as transfinite objects, he ought to accept that certain proofs have to be transfinite objects, too. He confirms this expressly when he comes to discuss two difficulties to which the analysis of the notion "f : [for all] xF(x)" gives rise from the finitist viewpoint, when f is a recursive function (cf. Tait 1981, p. 527). At least those functions whose domain embraces the whole of N cannot be concrete, finite objects and, hence, cannot be proofs in Hilbert's sense.

Tait (1981, p. 526f.) continues:
```   It is clear that, no matter how the analysis goes, if f is such
a proof and a: A, then f should yield us a proof fa of F(a),
fa : F(a). [...] This requirement is in keeping with the finitist
idea of a proof of a general proposition as a schema for proving
its instances.
```

Notice that Tait does not provide any argument for his first claim; he rather seems to take the choice of the schema as evident. It is the other direction of the proposed explication that causes problems, though: "Conversely, it would seem reasonable that, if f associated with each a: A a proof of F(a), then f should count as a proof of [for all] xF(x)" (Tait 1981, p. 526). For the sake of simplicity, we confine ourselves to considering the case in which all objects are solely of type N. Thus, Tait's first proposal to fix the meaning of "f : [for all] x F(x)" (restricted to type N) amounts to this:

([for all] r) Let f be a recursive function, and F(n) be an equation in [L.sub.FIN]; then

f: [for all] x F(x) [??] for arbitrary n : N we have f(n) : F(n).

However, Tait draws attention to two difficulties that in his opinion render ([for all] r) inadequate from the finitist point of view (Tait 1981, p. 527).

First: Appealing to ([for all] r), Tait sketches a proof of [Con.sub.zf] (assuming that ZF is consistent) which he considers to be non-finitist.

Second: In his analysis, a proof f is a transfinite object, because it is defined for each of the infinitely many natural numbers.

Now, although Tait jettisons (for all] r), he does not, in our opinion, disavow the schema underlying ([for all] r):

([for all] G) Let f be a "good" function, and F(n) be an equation in [L.sub.FIN]; then

f: [for all] x F(x) [??] for arbitrary n : N we have f(n) : F(n).

In ([for all] r), "recursive" represents "good". Tait seems to take the schema ([for all] G) for granted (12) and sets about finding suitable candidates for the "good" functions. Plainly, according to Tait a class K of functions may be a suitable candidate for the class of "good" functions only if it does not involve either of the difficulties mentioned above. Otherwise, it would be hard to see why these difficulties should have led to the rejection of ([for all] r).

On the face of it, the "finitist" functions suggest themselves as candidates for the "good" functions. The second difficulty presumably does not arise by simple virtue of the attribute "finitist" itself, and the first difficulty should also be avoidable. If, for the moment, we accept Tait's First Thesis, schema ([for all] G) takes on the following form (cf. Tait 1981, pp. 534, 536):

([for all] pr) Let f be a primitive recursive function, and F(n) be an equation in [L.sub.FIN]; then

f : [for all] x F(x) [??] for arbitrary n : N we have f(n) : F(n).

In Tait's view, the principle ([for all] pr) serves for fixing the meaning of "f : [for all] x F(x)". However, he does not argue for its adequacy, nor does he examine the possibility of framing alternative stipulations. It is further clear that by choosing as "good" functions the primitive recursive ones, Tait does not avoid the second difficulty. Justas the recursive functions are defined on the whole of N, so are the primitive recursive ones; the latter are, therefore, transfinite objects, too.

Bearing ([for all] pr) in mind, we may now consider Tait's Second Thesis. To see whether it is sound, we must explain his conception of finitist mathematics in more precise terms. This in turn requires that we explain the role of the equivalence sign in ([for all] pr). We begin with a stipulation.

Let FI[N.sub.0] per definitionem be the first-order theory axiomatized by the set of the variable-free sentences which are proved via the "constructions" [f.sub.0] - [f.sub.7] (see Tait 1981, p. 535f.).

We think that there are two ways of interpreting the equivalence sign in ([for all] pr); we refer to them by means of ([alpha]) and ([beta]) respectively.

([alpha]) ([for all] pr) embodies a definition.

That is, for a primitive recursive function f and an equation F(n) in [L.sub.FIN], "f : [for all] x F(x)" is introduced as ah abbreviation for "for arbitrary n : N we have f(n) : F(n)". Notice that we have here a contextual definition defining neither "[for all] x" nor "[for all] xF(x)", but rather the entire formula "f : [for all] xF(x)". If we were to define

FIN- := FI[N.sub.0], supplemented by the definition ([for all] pr),

then "finitist mathematics" in Tait's sense would be precisely explained through FIN-. Basically, we have no objection to defining "f : [for all] xF(x)" in this way, but wish to emphasize that it is only apparent that FIN- should strengthen FI[N.sub.0]. For in the definition above we merely stipulate that we may write, e.g., "f : [for all] x(x + 1 = 1 + x)", if for every n f(n) is a finitistic proof of "n + 1 = 1 + n". The fact that "f : [for all] x(x + 1 = 1 + x)" contains "[for all] x(x + 1 = 1 + x)" by no means implies that in "f : [for all]x(x + 1 = 1 + x)" the symbol "[for all] x" occurs as a universal quantifier, as it is usually understood.

In this connection, we feel inclined to warn against the danger of falling prey to a confusion we shall spell out in a moment. Michael D. Resnik's account of formulae of PRA with free variables as part of his discussion of Hilbert's finitism in his book Frege and the Philosophy of Mathematics (1980) is a case in point. (13) It is worth canvassing some relevant passages of his account.

Resnik (1980, p. 82) is right in claiming that Hilbert probably recognized the meaningfulness of sentences, i.e. closed formulae, of variable-free primitive recursive arithmetic. The truth-value of such sentences can be ascertained effectively by finite, intuitive operations on the unary numerals (figures). We further agree with Resnik (1980, p. 83) that Hilbert countenanced bounded existential and universal quantifications (the bounds being numerals), because such sentences are taken to be equivalent to finite disjunctions and conjunctions, respectively (see Hilbert 1926, pp. 90f. [377f.]). Yet Resnik (1980, p. 83) writes also: "Hilbert found a place in his scheme for sentences of primitive recursive arithmetic with free variables. For these can be interpreted as schematic devices for asserting their instances. For example, the formula

(1) (x + y = y + x)

is meaningful as long as we interpret it as being a short form for

'x + y = y + x' yields a truth if any numerals are substituted for 'x' and 'y'."

So, formula (1) is meaningful, if we regard it as an abbreviation of

For all numerals k, l ("k + l = l + k" is true).

To put it in more general terms: a [[PI].sup.0.sub.0]-formula A(x, ...) is interpreted as a shorthand expression for "For all numerals k, ... 'A(k, ...)' is true".

Resnik's proposal, taken literally, cannot be correct, however. If it were, "PRA [??] x + y = y + x" would have to be an abbreviation for "PRA [??] for all numerals k, l ('k + l = l + k' is true)". Yet, the finitist wants to claim: "For all numerals k, l PRA [??] k + l = l + k." We take it that this is what Resnik has in mind.

Keeping the proposed emendation in mind, we turn to another passage in Resnik (1980). Let S be an axiomatizable theory. Following Resnik's proposal, the claim

(a) S [??] [logical not](x is a proof in S of "0 = 1")

(a') For all numerals k, S [??] [logical not](k is a proof in S of "0 = 1"),

since "[logical not](x is a proof in S of '0 = 1')" is a [[PI].sup.0.sub.0]-formula. (14)

Resnik contends (i) that (a) is false (i.e. that it is not the case that S [??] [logical not](x is a proof in S of "0 = 1")), and, in addition, (ii) that (a') is true (cf. Resnik 1980, p. 92). In fact, (a') is true, and if we construe (a) as usual, i.e. as a statement which would be equivalent to S [??] [for all] x[logical not](x is a proof in S of "0 = 1") (assuming that the language contains a universal quantifier), then (a) is false. However, if we rely on Resnik's proposal for interpreting schematic statements, (a) is defined as (a'); as a consequence, (i) clashes with (ii), and (a) is true. So, Resnik's exposition gives rise to the following confusion. The context "S [??] A(x)" (with the free variable x) is typographically preserved, though it undergoes reinterpretation. At a later stage, one may be liable not to account for the reinterpretation and read "S [??] A(x)" sometimes according to the usual and sometimes according to the reinterpreted version. Resnik himself seems prone to commit this error. The upshot of these considerations is, then, that one should carefully avoid Resnik's notation.

It should be clear that Resnik endorses the version of introducing "universal quantification" in the language of finitist mathematics that we termed ([alpha]). It is, however, hard to believe that ([alpha]) is faithful to Tait's exposition. For one thing, in his 1981 paper Tait does not state explicitly that "f : [for all] x F(x)" is defined through "for arbitrary n : N we have f(n) : F(n)".

Furthermore, the conception of finitist mathematics under consideration does not provide an answer to the question as to how "[for all] x(x + 1 = 1 + x)", construed in the ordinary way, could be proved finitistically at all. Finally, if we endorse interpretation ([alpha]) as regards recursive functions, we see that the first difficulty mentioned by Tait does not emerge at all. This is because it rests on the following consideration: Tait shows, by using a recursive (not necessarily primitive recursive) function g, that [for all] n (g(n) : [logical not][Proof.sub.zf](n, [??])), and concludes then to g : [for all] x[logical not][Proof.sub.zf](x, [??]), i.e. to g : [Con.sub.zf]. In the sense of interpretation ([alpha]), however, "g : [Con.sub.zf]" is per definitionem only an abbreviation of "[for all] n (g(n) : [logical not][Proof.sub.zf](n, [??]))". In this case, we have no recursive proof of the consistency of ZF at all, but only what we have called a proof of the approximative consistency of ZF. This causes no problem if we assume that ZF is consistent and that every true [[summation of].sup.0.sub.0]-sentence is finitistically provable. (15) The first difficulty appealed to by Tait regarding ([for all] r) turns out to be a chimera.

Since the interpretation of ([for all] pr) through ([alpha]) fails to square with the remainder of Tait's account, we think that what Tait has in mind when he speaks of finitist mathematics is rather captured by option ([beta]) of interpreting ([for all] pr). Here it is:

([beta]) ([for all] pr) is considered to be a new rule of inference.

More specifically, for a primitive recursive function f and an equation F(n) in [L.sub.FIN], one may conclude from: for every n : N, f(n) is a finitary proof of F (n), to: [for all] x F(x),

where the finitary proof of [for all] x F(x) is coded by the function f.

"[for all] xF(x)" is here understood as usual. From now on, we use "FIN" as a shorthand expression for the closure of FI[N.sub.0] under the inference rule given by ([for all]pr). FIN can be defined precisely along familiar lines: we define a monotone operator which captures one application of the rule of inference ([for all] pr) and obtain the desired theory as the fixed point of the inductive definition thereby determined. (16) In this context, we need not specify the exact form of the inductive definition. For present purposes, it is enough to invoke

(!) If F(n) is an equation in [L.sub.FIN], and f is a primitive recursive function such that for every n : N, f(n) is a proof of F(n) in FIN, then [for all] xF(x) is provable in FIN.

In what follows, we examine whether Tait's Second Thesis applies if "finitist theorem" is construed as "Theorem of FIN". We demonstrate that there is no axiomatizable extension S of PRA such that FIN and S prove the same formulae. Under this interpretation, Tait's Second Thesis is then bound to fail. To make our line of argument perspicuous, we must now characterize the theory PRA and the closely related theory (QF-IA) in greater detail.

PRA is a theory formulated in a quantifier-free fragment [L.sub.PRA] of a first-order language. The vocabulary of [L.sub.PRA] contains for each primitive recursive function f a unique function sign [bar.f], a "primitive recursive function sign". The axioms of PRA are, apart from classical logic in [L.sub.PRA], the recursion equations for all primitive recursive functions, "[logical not][bar.S]x = [bar.0]" and "[bar.S]x = [bar.S]y [right arrow] x = y". Moreover, PRA is assumed to be closed under the induction rule, couched in the vocabulary of [L.sub.PRA]. (QF-IA) is the theory that results from PRA by adding first-order logic. In particular, its language [L.sub.(QF-IA)] includes all the primitive recursive function signs contained in [L.sub.PRA]. PRA and (QF-IA) are almost the same theory. More specifically, we have:

If [phi]([??]) is a [[PI].sup.0.sub.0]-formula of [L.sub.(QF-IA)], there is a primitive recursive function sign [X.sub.[phi]] such that

(i) PRA [??] [[chi].sub.[phi]]([??]) = [bar.0] [??] (QF-IA) [??] [phi]([??])

Furthermore, there is an important proof-theoretic result of Parsons (cf. Parsons 1970; Sieg 1985, p. 50), stating that

(ii) (QF-IA) [??] [for all] y [there exists] z [phi](y, z) [??] [there exists] f (f is primitive recursive [conjunction] PRA [??] [X.sub.[phi]](y, f(y)) = [bar.0])

(i) + (ii) imply: if [phi](y, z) is a [[PI].sup.0.sub.0]-formula of [L.sub.(QF-IA)], then

(!!) (QF-IA) [??] [for all] y [there exists] z [phi](y, z) [??] [there exists] f (f is primitive recursive [conjunction] (QF-IA) [??] [for all] y [phi](y, [bar.f](y)))

Finally, we have

(iii) (QF-IA) [??] [[chi].sub.[phi]]([??]) = [bar.0] [left and right arrow] [phi]([??])

It is now time to state and prove what we consider to be the key theorem (K):

Theorem K: There is no recursively enumerable theory S which extends PRA such that S and FIN prove the same formulae.

Proof: Let S be a recursively enumerable extension of PRA such that S = FIN, and let [sigma] be a representation of a set of axioms of S which is [[PI].sup.0.sub.0] (which exists by virtue of Craig's Theorem; cf. Craig 1953). Then "[logical not][Proof.sub.[sigma]](x, [??])" is a [[PI].sup.0.sub.0]-formula in [L.sub.PA], and therefore by (iii),

(1) [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII.]

holds. Since, by assumption, FIN contains PRA and proves full first-order logic, it also extends (QF-IA). Thus

(2) [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII.]

Now "[Pr.sub.[sigma]]" is a representation of FIN in [[summation of].sup.0.sub.1]; hence,

(3) [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII.]

follows from (2) by virtue of general metamathematical considerations.

It is, moreover, well known (cf. Smorynski 1977) that

(4) (QF-IA) [??] [for all] x [Pr.sub.[sigma]]([bar.[??][logical not] [Proof.sub.[sigma]]([??], [bar.[??][perpendicular to][??]])[??])]

From this formula and (3) we obtain

(5) [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII.]

Since [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII.] is a [[PI].sup.0.sub.0]-formula in [L.sub.(QF-IA)], it follows from (5) and (!!) that

(6) [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII.]

To be sure, (QF-IA) is sound. (17) Thus, we obtain from (6)

(7') [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII.]

that is (on the assumption we made for S and FIN):

[there exists] f (f is primitive recursive [conjunction] [for all] n (f(n) is a proof of

(7) [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII.]

Now, [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII.] is an equation in [L.sub.FIN]; thus, by applying (!) to (7), we can infer that

(8) [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII.]

which by virtue of (2) yields

(9) FIN [??] [for all] x[logical not][Proof.sub.[sigma]](x, [bar.[??][perpendicular to][??]])

i.e.

S [??] [Con.sub.[sigma]].

But this contradicts a general form of Godel's Second Theorem (cf. Feferman 1960).

Corollary: Tait's Second Thesis is false.

Proof: Assume that FIN proves exactly the universal closures of the formulae [psi]([??]) of [L.sub.PRA] such that PRA [??] [psi]([??]). Then FIN is a recursively enumerable extension of PRA. But by Theorem K this cannot be true.

We should like to emphasize that the specific role of Theorem K is not so much to discredit schema ([for all] pr) or possible alternative versions. We use it rather to undermine Tait's basic tenet that "FIN = PRA" in the light of its own assumptions. The reason is that, in short, ([for all] pr) and "FIN = PRA" are inconsistent with one another. This result is detrimental to Tait's approach, since the alleged plausibility of his Second Thesis is supposed to derive from both ([for all] pr) and his First Thesis. There is no compelling reason to expect that the finitistically provable sentences should be the universal closures of the PRA-theorems. We do think that Tait's Second Thesis can at best be rendered plausible by appeal to considerations such as these: For terminological reasons, one could assume that the finitistically provable sentences should be precisely those whose proofs are finitist objects, for example, finitist functions. Yet according to Tait's First Thesis, the finitist functions are the primitive recursive ones. If one assumes further that ([for all] pr) holds, then the sentences with finitist proofs may seem to be just the closures of the PRA-theorems. Understanding ([for all] pr) as a new rule of inference implies that the theory FIN herewith defined is too strong, however, of, in others words, that ([for all] pr) permits that too many functions be admitted as "good" functions. Hence, if one endorses schema ([for all] G), where the "good" functions are represented by the "finitist" functions, it is Tait's First Thesis that implies the falsity of his Second Thesis.

In sum: In ([for all] pr) either the role of "f: [for all] x F(x)" is newly determined by a contextual definition. The first difficulty mentioned above is then only spurious, (18) and Tait is at a loss to explain how universal sentences can be proved finitistically. Or in ([for all] pr) "[for all] x" is interpreted as usual, both in the definiens and the definiendum, that is, option ([beta]) is accepted. Theorem K then establishes the falsity of Tait's Second Thesis.

We ask the reader to bear in mind that the proof of Theorem K is correct only if we take option ([beta]) to be in force. If instead of ([beta]) we accept option ([alpha]), i.e. that "f: [for all] x F(x)" is only an abbreviation of the phrase "for arbitrary n : N we have f(n) : F(n)" (with suitable f and F), and if in the proof of Theorem K we accordingly replace each occurence of FIN with FIN-, (19) then this modification of Theorem K turns out to be false. To be sure, if we endorse option ([alpha]), we can show "[there exists] f (f is primitive recursive [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII.]. This statement, however, is then per definitionem equivalent to "[there exists] f (f is primitive recursive [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII.], i.e. to (7-); and (7-) by no means implies (8). When interpreted by ([alpha]), ([for all] pr) licenses the transition not from (7-) to (8), but only that from (7-) to (8-). In (8-) and (9-), however, we do not construe "[for all] x[logical not][Proof.sub.[sigma]](x, [bar.[??][perpendicular to][??]])" as a universal quantification in the ordinary sense.

We conclude, then, that Tait fails to meet his own requirements for an adequate explication of "finitist proof of a universally quantified equation". Besides this immanent criticism, we raise the following more general objections to his approach. If we accept interpretation ([beta]), then, at least without the restriction imposed on f, stipulation ([for all] G) is clearly inadequate for classical theories. The reason is that ([for all] pr) or ([for all] G) is a sort of application of an [omega]-rule, though a very weak one. And we know, of course, that, say, Q enlarged to embrace the unrestricted [omega]-rule is already equal to the set of the arithmetically true sentences. In other words, the axiomatizable extensions T of Q must be [omega]-incomplete. We should, therefore, not expect that ([for all] pr) is true for such theories T. (20) It is true enough that Tait's restriction to primitive recursive proof-codes in his definition of FIN makes it more likely that FIN is, in effect, a finitary theory. However, hopes to establish the purportedly finitary nature of FIN are dashed by Theorem K, unless one does not require of a finitary theory that it be recursively enumerable.

We think that ([for all] pr) is unacceptable from Hilbert's finitist point of view, if "[for all] x F(x)" is interpreted as usual (cf. Niebergall and Schirn 1998, section 5). Seen from this angle, Tait's suggestion to deal with finitist proofs of general statements (see Section VI of his 1981 article) contains a finitistically unjustified transition from the proofs of sentences with constants to the proofs of their universally quantified analogues. Thus, we learn that the finitist has no general notion of the equality of two closed terms of type B, but that for two given such terms, s and t, he grasps that s = t (Tait 1981, p. 535). (21) A few passages later (1981, p. 536), however, Tait tells us that he has already observed that [f.sub.0] - [f.sub.7] furnish hypothetical proofs f : [for all] x(F(x) [right arrow] G(x)) that are acceptable for the finitist: [f.sub.0]: [for all] x(0 = 0), [f.sub.1]: [for all] x(s(x) = t(x) [right arrow] s(x)' = t(x)'), and so on. To be sure, the proposed transition is formally correct, if one accepts ([for all] pr). From a "contentual" point of view, however, we regard it as finitistically unacceptable. (22)

Today, proof theorists widely believe in the identification of finitist (meta-)mathematics with PRA. Some of them even seem to take Tait's Second Thesis for granted. Stephen G. Simpson (1988, p. 352), for instance, holds that
```   Tait argues convincingly that Hilbert's finitism is captured
by the formal system PRA [...]. This conclusion is based on
a careful study of what Hilbert said about finitism [...].
PRA seems to embody just that part of mathematics which remains
if we excise all infinitistic concepts and modes of reasoning.
```

Furthermore, Simpson (1988, p. 359) believes that all possible objections to the identification of finitist (meta)mathematics with PRA have been dealt with adequately by Tait in his paper "Finitism". Again, our foregoing discussion (23) ought to have revealed that the identification of finitist mathematics with PRA is questionable, if not untenable. Contrary to what Simpson claims, Tait has certainly not succeeded in defeating all possible objections to this identification. It is perhaps time to reconsider what finitism is or ought to be. (24)

* Thanks to an anonymous referee for his comments and suggestions.

(1) Note that the equations mentioned here may contain free variables. Tait's original formulation is: The finitist theorems are those sentences of the form [for all] x(F(x) [right arrow] G(x)) such that F(x) [right arrow] G(x) is provable in PRA. Since F and G have to be quantifier-free in this case, this version is equivalent to what we call Tait's Second Thesis. PRA will be defined in precise terms below.

(2) Let [phi] be a formula of an arithmetical language L (like [L.sub.PA] or [L.sub.PRA]), A [subset or equal to] [[omega].sup.k] for some k [greater than or equal to] 1; then

[phi] is [[summation of].sup.0.sub.0] (or: [phi] is [[PI].sup.0.sub.0]) : [??] [phi] is quantifier-free of contains at most bounded quantifiers (i.e. expressions of the form "[for all] x [less than or equal to] y" or "[there exists] x [less than or equal to] y").

[phi] is [[summation of].sup.0.sub.k+1] : [??] there exists [psi] (x, [??]) in [[PI].sup.0.sub.k] such that [phi] [equivalent to] [there exists] x[psi] (x, [??]).

[phi] is [[PI].sup.0.sub.k+1] : [??] there exists [phi] (x, [??]) in [[summation of].sup.0.sub.k] such that [phi] [equivalent to] [for all] x[psi] (x, [??]).

A is [[summation of].sup.0.sub.m] ([[PI].sup.0.sub.m], resp.) : [??] there exists a k-place formula [alpha] in [[summation of].sup.0.sub.m] (or in [[PI].sup.0.sub.m]) such that A = {[??]|N[??] [alpha]([??])}.

A is arithmetically definable : [??] A is [[summation of].sup.0.sub.m] for some m [member of] [omega].

(3) For a k-place formula [alpha] in L[PA] and A [subset or equal to] [[omega].sup.k], it is common to define [alpha] is a representation of A : [??] [for all] [n.sub.l], ... [n.sub.k] [member of] [omega] (<[n.sub.l], ..., [n.sub.k]> [member of] A [??] N [??] [alpha]([[bar.n].sub.l], ..., [[bar.n].sub.k])).

Here, for each natural number n, [bar.n] is the (unique) numeral denoting n in the standard model of the natural numbers N. By identifying formulae, taken from language L, with their Godel-numbers, "[tau] is a representation of a set of formulae T" is defined accordingly. Given a representation [tau] of a set of formulae T, the common arithmetizations of "proof in T", "provable in T" and "T is consistent" are these:

[Proof.sub.[tau]] (x, y) : [left and right arrow] Seq(x) [conjunction] y = [x.sub.lh(x)-1] [conjunction] [for all] v < lh(x)(LogAx([x.sub.v]) [disjunction] [tau]([x.sub.v]) [disjunction] [there exists] uw < v([x.sub.w] = [x.sub.u] [??] [x.sub.v])),

[Pr.sub.[tau]](y) : [left and right arrow] [Proof.sub.[tau]](x,y),

[Con.sub.[tau]] : [left and right arrow] [logical not] [Pr.sub.[tau]]([bar.[??][perpendicular to][??]]).

We write "[??]t[??]" for the Godel-number and "[bar.[??]t[??]]" for the Godel-numeral of an expression t. The usual "syntactic" metamathematieal vocabulary like "x is a sequence", "the length of (sequence) x", "x is the conditional of y and z" and "x is an axiom of first-order predicate logic" is represented by [[summation of].sup.0.sub.0]-formulae: "Seq(x)", "lh(x)", "x = y [??] z" and "LogAx(x)", such that features characteristic of these predicates are provable in a weak fragment of PA; see Kaye 1991 and Hajek and Pudlak 1993 for more details. As to the "dot-notation'" see Feferman 1960.

(4) Tait (1981, pp. 525f., 540) regards this distinction as incoherent. He maintains that for Hilbert numbers are representable in intuition, whereas functions, sets, and other transfinite objects are not. Tait claims that Hilbert regards transfinite objects as "ideas of pure reason" (1981, pp. 525, 540). Two comments may be in order here. Firstly: As far as we know there is no place in Hilbert's writings where he says expressly that every number can be represented in intuition. It is true, however, that at least in his papers between 1922 and 1928 (cf. Hilbert 1922, 1923, 1926, 1928a, 1928b) he construes the natural numbers as numerals or figures. In so doing, he faces a serious difficulty. On the one hand, he seems to be advocating the view that every numeral is surveyable. On the other hand, he must have been aware that at least fairly large finite numbers, conceived of as strings of stroke-symbols, can hardly be said to be surveyable. It is further plain that any attempt to establish an upper bound as to the surveyability of strings of numerical figures would founder on the arbitrariness of our actual choices. These and similar observations might be seen as threatening the allegedly intuitive evidence of contentual, finitary statements about large finite numbers. See in this connection Charles Parsons's reflections on the thesis that every string can be intuited (Parsons 1998). Secondly: Having arrived at the result that the infinite is neither present in nature nor admissible as a foundation in our rational thinking (cf. Hilbert 1926, p. 108 [392]), Hilbert concludes his essay "Uber das Unendliche" by assigning to the infinite a certain regulative role, namely that of a Kantian idea. (In the "Transcendental Dialectic" of the Critique of Pure Reason, Kant speaks of pure concepts of reason or transcendental ideas which are designed to determine according to principles how understanding is to be employed in dealing with experience in its totality; cf. Kant 1787, A 321, B 378.) Nevertheless, Hilbert's appeal to Kant implies by no means that he [Hilbert] regarded functions or (infinite) sets as transcendental ideas.

(5) This claim does not follow from the goal of establishing consistency; see in this connection our introduction of the notion of ah approximative consistency proof in Niebergall and Schirn 1998; we define it there as follows (for axiomatizable theories S and T with representation [tau]): S proves the approximative consistency of T : [??] [for al] n S [??] [logical not][Proof.sub.[tau]]([bar.n], [bar.[??][perpendicular to][??]]). In our opinion, the notion of an approximative consistency proof may capture the core of the conception of finitary metamathematical consistency proofs which Hilbert developed in his papers on proof theory in the 1920s.

(6) Both Q and TI[[alpha]] are formulated in [L.sub.PA]. Q results from PA by replacing the induction schema with the sentence which expresses that only 0 is not a successor of a natural number. This is a consequence of PA. TI[[alpha]] is the set of all formulae [for all] x [??] [bar.[alpha]] ([for all] y x[phi](y) [right arrow] [phi](x)) [right arrow] [for all] x [??] [bar.[alpha]] [phi](x)); here, [phi] is an arbitrary formula of [L.sub.PA], [bar.[alpha]] is a notation for a countable ordinal number [alpha], and [??] is an arithmetically definable well-ordering of order-type [alpha]. Since [alpha] may be chosen to be quite large, TI[[alpha]] can be made quite strong. By contrast, Q is a very weak theory.

(7) This modal explanation of what makes a primitive recursive function a finitist function leaves much to be desired, h is precisely the word "can" that requires explication.

(8) Take for example for X the set of the arithmetically true sentences (in the language of PA) and for Y the set of [[summation of].sup.0.sub.3]-sentences. Then X is not arithmetically definable, but X [intersection] Y is.

(9) In Hilbert and Bernays (1934, 26), we find the following explication of the notion of a function: Under a function we understand here an intuitive construction, on the basis of which a numeral is assigned to a given numeral or pair of triple, etc., of numerals.

(10) Take an example from ZF: from ZF [??] [for all] x(x[epsilon] V) it clearly does not follow that the expression "V" designates something, e.g., the universal set.

(11) Tait seems to assume the existence of both primitive recursive and finitist functions. If there are neither primitive recursive nor finitist functions, we face a problem concerning the identity or identification of "non-existing objects". Its solution would depend on an appropriate choice of a free logic.

(12) As a matter of fact, ([for all] G) (for arbitrary formulae) is part of the BHK-interpretation of the logical signs known from intuitionism.

(13) In general, we appreciate Resnik's account of Hilbert's finitism. It seems to us that Resnik discusses, in an illuminating way, a number of philosophically interesting aspects.

(14) We adopt Resnik's notation and write "[logical not](x is a proof in S of '0 = 1')" instead of "[logical not][Proof.sub.[sigma]](x, [bar.[??][perpendicular to][??]])" (where [sigma] is a [[PI].sup.0.sub.0]-formula which represents a set of axioms of S).

(15) See Niebergall and Schirn 1998.

(16) Due to the assumption that only equations are admitted when we come to apply the inference rule ([for all] pr), FIN turns out to be arithmetically definable.

(17) Of course, we do not claim at this point that it is finitistically provable that (QF-IA) is sound.

(18) There is no reason for assuming that Tait treats ([for all] G) on the one hand as a definition, on the other as a rule of inference, depending on whether in ([for all] G) one chooses for the "good" functions only the primitive recursive ones or all recursive functions.

(19) Proofline (k) is thereby converted into a formula which we can (k-).

(20) In his essay "Die Grundlegung der elementaren Zahlenlehre" (1931), Hilbert suggests an extension of PA similar to the one presented by Tait in his 1981 paper. Hilbert extends PA to a theory Z* along the lines of ([for all] G), without confining himself to what we here called "good" functions; and he considers this extension to be finitary. Our own view is that in the light of Hilbert's explication of the word "finitary" (cf. Hilbert and Bernays 1934, p. 32), it is hard to maintain the allegedly finitary character of Z*. For more details see Schirn and Niebergall 2001.

(21) See the ensuing sequence [f.sub.0] : 0 = 0; [f.sub.1] : s = t [right arrow] s' = t'; ...

(22) We wish to draw attention to an important point here. While both the variable-free and the quantifier-free versions are made plausible by Tait, he does not adduce a "contentual" argument for the universally quantified versions. He does not even discuss the question why we should accept the latter version. Nor does he tell us that he has already used ([for all] pr) in order to arrive at [f.sub.0] : [for all] x(0 = 0), [f.sub.1] : [for all] x(s(x) = t(x), [right arrow] s(x)' = t(x)'), and so on, by starting from [f.sub.0] : 0 = 0, [f.sub.1] : s = t [right arrow] s' = t'.

(23) Cf. also Niebergall and Schirn 1998.

(24) We may point out that in Niebergall and Schirn 2002 we argue that a weak version of Hilbert's finitist metamathematics of the 1920s is compatible with Godel's Incompleteness Theorems by using only what are clearly natural provability predicates.

REFERENCES

Craig, W., 1953, "On Axiomatizability Within a System", The Journal Of Symbolic Logic, vol. 18, pp. 30-32.

Feferman, S., 1960, "Arithmetization of Metamathematics in a General Setting", Fundamenta Mathematicae, vol. 49, pp. 35-92.

Hajek, P. and P. Pudlak, 1993, Metamathematics of First-Order Arithmetic, Springer-Verlag, Berlin/Heidelberg/New York.

Heijenoort, J. van (ed.), 1967, From Frege to Godel, a Source Book in Mathematical Logic, 1879-1931, Harvard University Press, Cambridge Mass./London.

Hilbert, D., 1935, Gesammelte Abhandlungen, III, Springer-Verlag, Berlin (second edition 1970).

--, 1931, "Die Grundlegung der elementaren Zahlenlehre", Mathematische Annalen, vol. 104, pp. 485-494.

--, 1928a, "Die Grundlagen der Mathematik", Abhandlungen aus dem Mathematischen Seminar der Hamburger Universitat, vol. 6, pp. 65-85. (Abbreviated version reprinted as appendix IX in the seventh edition of Hilbert 1899, pp. 289-312.) [English translation "The Foundations of Mathematics", in van Heijenoort 1967, pp. 464-479.]

--, 1928b, "Probleme der Grundlegung der Mathematik", Atti del Congreso nazionale del matematici, Bologna 3-10 settembre 1928, vol. 1, pp. 135-141. (With supplementations reprinted in Mathematische Annalen, vol. 102, 1929, pp. 1-9, and as appendix X in the seventh edition of Hilbert 1899, pp. 313-323.)

--, 1926, "Uber das Unendliche", Mathematische Annalen, vol. 95, pp. 161-190. (Reprinted in D. Hilbert, Hilbertiana, Wissenschaftliche Buchgesellschaft, Darmstadt, 1964, pp. 79-108. [English translation "On the Infinite", in van Heijenoort 1967, pp. 367-392.]

--, 1923, "Die logischen Grundlagen der Mathematik", Mathematische Annalen, vol. 88, pp. 151-165. (Reprinted in Hilbert 1935, pp. 178-191.)

--, 1922, "Neubegrundung der Mathematik", Erste Mitteilung, Abhandlungen aus dem Mathematischen Seminar der Hamburger Universitat, vol. 1, pp. 157-177. (Reprinted in Hilbert 1935, pp. 157-177.)

--, 1899, Grundlagen der Geometrie, Teubner, Leipzig 1899. (Seventh revised and enlarged edition 1930.)

Hilbert, D. and P. Bernays, 1939, Grundlagen der Mathematik II, Springer-Verlag, Berlin/Heidelberg. (Second edition with modifications and supplementations, 1970.)

--,1934, Grundlagen der Mathematik I, Springer-Verlag, Berlin/ Heidelberg. (Second edition with modifications and supplementations, 1968.)

Kant, I., 1787, Kritik der reinen Vernunft, ed. R. Schmidt, Hamburg, 1956.

Kaye, R., 1991, Models of Peano Arithmetic, Oxford University Press, Oxford.

Niebergall, K.G. and M. Schirn, 2002, "Hilbert's Programme and Godel's Theorems", Dialectica, vol. 56, pp. 347-370.

--, 1998, "Hilbert's Finitism and the Notion of Infinity", in Schirn 1998, pp. 271-305.

Parsons, C., 1998, "Finitism and Intuitive Knowledge", in Schirn 1998, pp. 249-270.

--, 1970, "On a Number-Theoretic Choice Schema and Its Relation to Induction", in A. Kino, J. Myhill and R.E. Vesley (eds.), Intuitionism and Proof Theory, North-Holland, Amsterdam, pp. 459-473.

Resnik, M.D., 1980, Frege and the Philosophy of Mathematics, Cornell University Press, Ithaca/London.

Schirn, M. (ed.), 1998, The Philosophy of Mathematics Today, Oxford University Press, Oxford.

Schirn, M. and Niebergall, K.G., 2001, "Extensions of the Finitist Point of View", History and Philosophy of Logic, vol. 22, pp. 135-161.

Sieg, W., 1985, "Fragments of Arithmetic", Annals of Pure and Applied Logic, vol. 28, pp. 33-72.

Simpson, S.G., 1988, "Partial Realizations of Hilbert's Program", The Journal of Symbolic Logic, vol. 53, pp. 349-363.

Smorynski, C., 1977, "The Incompleteness Theorems", in J. Barwise (ed.), Handbook of Mathematical Logic, North-Holland, Amsterdam, pp. 821-865.

Tait, W.W., 1981, "Finitism", The Journal of Philosophy, vol. 78, pp. 524-546.

Received January 22, 2003; accepted March 5, 2003.

MATTHIAS SCHIRN

Seminar fur Philosophie, Logik und Wissenschaftstheorie

Universitat Munchen

matthias.schirn@lrz.uni-muenchen.de

KARL-GEORG NIEBERGALL

Seminar fur Philosophie, Logik und Wissenschaftstheorie

Universitat Munchen

kgn@lrz.uni-muenchen.de

RESUMEN: En su articulo "Finitism" (1981), W.W. Tait sostiene que la dificultad principal para quien quiere comprender la concepcion hilbertiana de la matematica finitista es esta: especificar el sentido de la demostrabilidad de enunciados generales sobre los numeros naturales sin presuponer totalidades infinitas. Ademas, Tait argumenta que todo razonamiento finitista es esencialmente primitivo recursivo. En este articulo tratamos de mostrar que su tesis "Las funciones finitistas son precisamente las funciones primitivas recursivas" es discutible y que otra, tambien defendida por el, resulta insostenible. La segunda tesis es que los teoremas finitistas son precisamente las clausuras universales de las ecuaciones que pueden demostrarse en PRA.

PALABRAS CLAVE: funciones finitistas, funciones primitivas recursivas, totalidades infinitas, demostracion de la clausura universal de una ecuacion
COPYRIGHT 2003 UNAM, Instituto de Investigaciones Filosoficas
No portion of this article can be reproduced without the express written permission from the copyright holder.