Is finitism an extreme form of constructivism? - MathOverflow

Is finitism an extreme form of constructivism?

2011-01-10T20:57:52Z

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).

Answer by Mike Shulman for Is finitism an extreme form of constructivism?

2011-01-10T22:45:27Z

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.

Answer by Stefan Geschke for Is finitism an extreme form of constructivism?

2011-01-10T22:50:57Z

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.

Answer by Daniel Mehkeri for Is finitism an extreme form of constructivism?

2011-01-11T03:30:29Z

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!

Answer by Mitch Harris for Is finitism an extreme form of constructivism?

2011-01-11T03:50:16Z

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.