[FOM] primer on vagueness

[Vladimir Sazonov]

The main point of my previous posting was that although the 
existence of 2^1024 = 2^{2^10} is provable by means of 
classical logic from some simple assumptions, there is a 
mathematically rigorous way to consider this number as not 
existing (non-feasible) under a restricted version of 
classical logic. So to speak, we need here a microscope 
instead of the habitual "classical" telescope. 

Anyway, if we are still interested in as short as possible 
formal classical existence proof of 2^1024, we can make 
the sub-derivation 

M(0), M(0) => M(1), M(1),...,M(1023), M(1023) => M(1024), M(1024) 

from that posting (and therefore the whole derivation of existence 
of 2^1024) to be considerably shorter. 

First, infer from the sentence (ii) forall x (M(x) => M(x+1)) 
derived in the previous posting the following sequence of 
corollaries, step-by-step: 

(*) forall x (M(x) => M(x + 2^i)),  i = 0,1,...,10.

Indeed, the case i=0 is just (ii). Then, assuming that this is 
proved for some i, we can infer this for i+1:

M(x) => M(x + 2^i) and M(x + 2^i) => M(x + 2^i + 2^i) 
entail M(x) => M(x + 2^{i+1}).

Then apply the last formula in (*) to x = 0 and use M(0) 
and modus ponens to get M(1024). This proof contains only 
10 of routine steps instead of 1024. 

Probably a compression of this kind was mentioned by 
Charles Silver and Michael Sheard. But even more can be done:  

By using this idea we can feasibly derive existence even of  
exponential tower 2_1000 = 2^{2^{...^2...}} of the height 1000 
which denotes the number incomparably larger than that denoted 
by the short tower 2^1024 = 2^{2^10}. (Note, that some iterated 
abbreviations for formulas are used here.) Such a derivation can 
be extracted from V. Orevkov's proof of non-elementary complexity 
of cut elimination (1979) and is also presented in my paper 
"On feasible numbers" to demonstrate that non-restricted classical 
logic is not appropriate for formalizing feasibility. 

Vladimir Sazonov


----------------------------------------------------------------
This message was sent using IMP, the Internet Messaging Program.