# Is finitism an extreme form of constructivism?

I hope this question is not too soft for MO.

The Wikipedia says about finitism that it is an extreme form of constructivism. See http://en.wikipedia.org/wiki/Finitism. I doubt that this is correct.

As I understand, there were different approaches to solve the crisis of the foundation of mathematics. One was constructivism, where there must be a witness of an object. Finitism was another approach were one (Hilbert) tried to give existing mathematics a foundation in finitism. But it was not a rejection of certain mathematical methods, just finding a foundation. Finally, the third approach was just adapting the logics, which led to ZFC and type-theory.

Hilbert opposed the intuitionism of Brouwer. So, it is a little bit strange to count them to the same family.

In more modern finitism, related to reverse mathematics, one tries to prove that a finitism result obtained by infinitism methods, has a finitism proof. This has many successes and it has been shown that this is at least true for large parts of mathematics. Again, this is not a rejection of infinitism methods, but just an attempt to find a better foundation. While, constructivism is really a rejection of certain arguments.

So, based on above arguments, I believe the statement in the Wikipedia is totally wrong.

Maybe someone has more historical knowledge than me? If I am right, I can try to correct the article.

Regards,

Lucas

Edit: Thanks for the answers. I agree with Mike Schulman that both can mean a variety of things. I do think that the article in the Wikipedia needs some rewriting. It might be the case that finitism is more strict, however, I think it is not a subset of constructivism by definition (after lots of reasoning, one might conclude that).

-
Well, if Wikipedia says so... – Andrej Bauer Jan 10 '11 at 21:24
@Lucas, perhaps you might consider rephrasing your question to avoid mentioning Wikipedia? I'm not sure if MO is supposed to be an oversight or appeals mechanism for it. – Adam Jan 10 '11 at 21:45
I think a reference to the Wikipedia is more precise than 'they'. – Lucas K. Jan 10 '11 at 23:12
If the question can't be asked without mentioning Wikipedia, that's probably a sign that it is a question about Wikipedia rather than a question about mathematics. – Lamont C Jan 11 '11 at 8:28
Adam, Lamont C: Would you have the same difficulty if the question started out, "A professor of mine once claimed that" rather than "Wikipedia says that"? – Charles Staats Jan 12 '11 at 4:35

this is not a rejection of infinitism methods, but just an attempt to find a better foundation. While, constructivism is really a rejection of certain arguments.

I think that's arguable. There do exist (or, at least, there have existed) people who are philosophically finitist, in that they really do reject infinitistic arguments as wrong or meaningless. On the other hand, many people working on "constructive mathematics" nowadays are not philosophically constructivist like Brouwer, but would phrase their study as preferring to have constructive proofs than nonconstructive ones. (For instance, this is useful even if one "believes" in classical mathematics, since in the internal logic of a topos, only constructive mathematics is valid.)

I think that "finitist" and "constructivist" can both mean a variety of different things -- they can refer to a philosophical viewpoint, or merely to a mathematical enterprise. In the latter sense, I think finitism is indeed a "more restrictive" framework than constructivism. In the former sense, I think finitism is one extreme type of constructivism, although as you point out it is incompatible with some other types of constructivism.

-
I agree that "finitist" and "constructivist" can both mean a variety of different things, and that some forms of finitism are actually incompatible with some forms of constructivism. Precisely because of this fact, I agree with Lucas that it is misleading to start off the Wikipedia article with a sentence that seems to define finitism as a proper subset of constructivism. It would be better to offer a definition of finitism that doesn't refer to constructivism, and then have a separate paragraph discussing the relationship between finitism and constructivism. – Timothy Chow Jan 10 '11 at 23:45
@Timothy: I'm not sure what in specific you have in mind, but I'm not sure this general fact is important. After all, some forms of constructivism are also actually incompatible with other forms of constructivism. – Daniel Mehkeri Jan 11 '11 at 2:42

Hilbert was looking for proofs by "finitistic methods", and I believe that any of the common proof calculi of first order logic qualifies for this.

Finitism, on the other hand, rejects the existence of infinite objects. For example, each natural number exists, but the set of natural numbers does not.
This actually is an extreme form of constructivism.

-
Suppose you have a first order theorem proven in ACA0. The proof contains second order intermediate results. When you are proponent of finitism, then there is not much objection against such proof, because you know that there is a first order theorem that proves the same. This can be proven by finitistics methods. However, the proponent of constructivism, may object because the theory may not show how the result is constructed. – Lucas K. Jan 10 '11 at 23:01
Can you elaborate on what you mean by "the proof contains second order immediate results"? – Stefan Geschke Jan 10 '11 at 23:15
ACA0 is second order logic that is conservative over Peano arithmetic (Reverse Mathematics). You can have a final result theorem that is first order, but for deriving the theorem, some second order theorems were used. – Lucas K. Jan 10 '11 at 23:19
Yes, but if ACA0 is a conservative extension of Peano arithmetic, you can just prove you first order theorem using a first order proof. – Stefan Geschke Jan 11 '11 at 19:09
I still think that Hilbert's finitistic methods are something rather unrelated to finitism in the sense of what one might want to call extreme constructivism. Even though strictly speaking you could be a finitist in the sense that you don't accept the existence of infinite objects, but you don't insist on not having the law of the excluded middle, I believe that this position is rarely (if ever) taken. – Stefan Geschke Jan 11 '11 at 19:19

I think the assertion is basically correct. A finitist in Tait's (or Simpson's, or Hilbert's) sense would not object to a quantifier-free theorem in RCA_0 because there is a quantfier-free (in fact logic-free) proof of it in primitive recursive arithmetic. It would not extend to first-order proofs. A constructivist will not object. Kreisel's argument that finitism should extend to $<\epsilon_0$ still only includes the quantifier-free part, NOT all of first-order PA. In this sense finitism is definitely a subset of constructivism.

It is not contradictory for Hilbert to be in the same category as Brouwer because his point would then be that RCA_0 (or ACA_0 per Kreisel) is then justified as a conservative extension of finitist methods (not that they are themselves finitist).

There is of course a looser sense of "finitist" which is all of PA, because its domain of discourse is just the natural numbers, and not sets. But there are looser senses of "constructive" as well. Sometimes a result in classical set theory is called constructive if it just avoids the axiom of choice!

-

There are two kinds of thinking in foundations/reverse mathematics that could be called finitism.

One is Hilbert's program, which is associated with finitistic reasoning (proofs themselves are finite even though infinite objects may be allowed).

Another is a subset of PA which allows only finite objects, as in bounded arithmetic where all variables are implicitly bounded, which is often associated with constructivism.

Though the second concept is not necessarily a strict subset of contructivism (itself a term that is not particularly strict), I feel that the term 'finitism' usually refers to the restriction to finite objects.

-