FOM: unsurveyability

[Vladimir Sazonov]

Kanovei wrote:
> 
> Holmes:
> 
> <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 
world. 

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 
a fiction. 

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

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


Vladimir Sazonov