sazonov at logic.botik.ru
Mon Oct 5 17:36:58 EDT 1998
> <For example,
> <if one is an ultrafinitist,
Question to Holmes: Do you denote by the term "ultrafinitism"
a kind of mathematical religion?
one may flatly deny that proofs of
> <sufficiently large finite size whose existence can be deduced formally
> <(though they are in practice completely unsurveyable) even exist, much
> <less prove anything.
> Is there any example of a proof (concrete proof, I mean,
> not a hypothesis of its existence), seriously denied
> exactly by the reason that it is too long ?
First, what does it mean "concrete" if the proof is "too long"?
If it is infeasible so that it cannot exist in our real world
then it probably cannot be called "concrete". On the other hand,
it may be considered as "concrete" analogously to, say, concrete
cardinal number aleph_17 which surely also does not exist in our
Of course, classical mathematical theories (PA, ZFC, etc.)
with their set-theoretic (Tarski) semantics are essentially
insensitive to length of proofs. This is probably the reply
to your question.
There exist however classically inconsistent formal theories
(initiated by R.Parikh) formalizing feasibility concept which
I described here in fom. It can be shown that the shortest
proof of contradiction in these systems has the length >
approx. 2^1000. Therefore such theories are practically
consistent and the proof of their contradiction which you can
easily imagine (by applying modus ponens many-many times) but
newer really write symbol-by-symbol may be considered only as
These theories have some intuitive semantics. Thus the
imaginary proof of their contradiction can be denied. Whether
it is a "serious" reason probably depends on your interest in
formalizing the concept of feasibility and of course on whether
you allow considering such kind of formalization at all.
Also it is necessary to have much more experience with such
kind of formalizations to make them more convincing to
I believe that feasibility could become a new fundamental
concept for mathematics as it was new the concept of (actually
infinite) set. It needs a new kind of formalization. The
first experience shows at least that the enterprise is not
More information about the FOM