FOM: ultrafinitism and mathematical rigor

[Vladimir Sazonov]

Robert Black wrote:

> Professors Sazanov and Kanovei both seem to be defending some form of
> ultrafinitism.

I do not know about Professor Kanovei, but defending ultrafinitism was not
my goal in the current discussion on mathematical truth. Even without taking
into consideration ultrafinitism (as a conception, as a possible approach
to mathematics) the statements "A is true" or "A is (not) provable" considered
not in a specific rigorous (meta)mathematical context, i.e. not properly
formalized has, at least, a very doubtful character. Ultrafinitism is only a
side effect of the discussion on the nature of mathematics and how it may
be related with the reality. On the other hand, it is a very natural and
symptomatic side effect.


> 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,

Sorry, what is obviously true? I understand ultrafinitism as an important
idea which, I believe, could be properly formalized. I never said that
ultrafinitism or classical set theory or any other mathematical theory
is true. I am against of using the term truth in any similar situations, as
the current discussion should demonstrate. The only thing I could
say that some formalism is reasonable (by such and such reason)
and sufficiently adequately formalizes the initial (usually very vague)
idea.


> whereas it's (1) *radically* revisionary of what we ordinarily think

The concepts of irrational numbers, of continuity were also *radical*, as
well as Cantor's set theory with his cardinal arithmetic.


> 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 were some (unfortunately, not so many) quite mathematical rigorous
attempts (as well as some non-mathematical, very informal ones). This
subject is really comparatively new and it is sufficiently difficult to find
really working normalization which would be universally adopted. This is
a challenge for mathematicians (or logicians)!


> 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,

Do you suggest to WORKING mathematicians to use "abstract structures"
instead of the ordinary rigorous "feasible proofs made of dried ink"?
How will people read these "proofs"? Will it be considered as a mathematics
at all? On the other hand, the problem of unrealistically long proofs, if done
in ZFC *as it is*, demonstrates that in a sense we actually did not reach
the complete mathematical rigor (if it is possible at all). The reasonable
solution

consists in extending any given formalism (like ZFC) by some explicitly fixed
abbreviation mechanisms, and this can be done in various ways, probably
non-equivalent from the point of deductive power of the formalism (with taking
into account feasibility of proofs). Moreover, the concept of consistency of a
formal system should be respectively changed (made more precise!) if
feasibility of proofs is (explicitly) required. Let me ask again, is a proof
of non-feasible length (what does it mean???) a fully fledged mathematical
rigorous proof?


> is
> there any reason at all to think that formalizations in ZFC of currently
> accepted proofs would fit into the universe?

Yes, we should think about this more. Of course, I do not believe that
ZFC will not survive after taking into account the requirement of
feasibility of proofs (possibly with abbreviations). Also I do not think
that somebody should force mathematicians to write absolutely formal
feasible proofs in a formalism (as programmers write their computer
programs). This is a question to F.O.M. to realize what happens.
Anyway, what is or should be mathematical rigor, really?

I should add that I almost did not represent here my views on what
is ultrafinitism (or the concept of feasibility). Only the informal
requirement of feasibility of proofs was discussed and (what is a
separate question) that the very concept of feasibility could be
formalized. We need not have formalisation of feasibility to realize
that normal mathematical proofs are always feasible (even if they
are not rigorous, using a natural language, or even mistaken).


Vladimir Sazonov