FOM: ultrafinitism

[Robert Black]

Professors Sazanov and Kanovei both seem to be defending some form of
ultrafinitism. That's fine, it's a good old Russian tradition, and perhaps
they're right (though I don't myself think so). What is odd, though, is
that they both seem to think that this viewpoint is just obviously true,
whereas it's (1) *radically* revisionary of what we ordinarily think and
(2) to my knowledge at least has never achieved any adequate formal
expression (e.g. in the way Heyting managed to give formal expression to
intuitionist ideas).

There are all sorts of problems with this sort of ultrafinitism (which is
not to say that the problems are insoluble). Just for starters, if
mathematical proof has to do with formal provability in, say, ZFC, and if
the latter is to be understood not in terms of the existence of abstract
structures but in terms of concrete, feasible proofs made of dried ink, is
there any reason at all to think that formalizations in ZFC of currently
accepted proofs would fit into the universe? (There can be spectacular
blow-ups here: I seem to remember a FOM posting of a couple of months ago
giving a quite grotesque length for Bourbaki's definition of '2' reduced to
primitive notation.)

Robert Black
Dept of Philosophy
University of Nottingham
Nottingham NG7 2RD

tel. 0115-951 5845