[FOM] primer on vagueness

[Vladimir Sazonov]

Charles Silver asked on a feasible proof of existence of a number 
as big as 2^1000, as I understand, from as simple as possibly 
assumptions. 


The following is a very simple proof that 2^1024 (= 2^{2^10}) 
does exist (despite it is intuitively non-feasible) from several 
evident universal axioms on 0, 1, +, log (base two logarithm) 
and < by using the ordinary classical first order logic. 

I am too lazy to explicitly write down these axioms - nothing 
peculiar in them. The main point is that they are quite elementary 
(say, x =< log y => x+1 =< log (y + y), etc.) and involve only 
universal external quantifiers. 
The language does not involve even multiplication. 
No induction axiom is assumed. 

We represent existence of 2^1024 as the sentence 

     exists y(log log y >= 10). 

Let us assume that its negation 

     forall y (log log y < 10) 

holds and get a contradiction. 

Define M(x) as exists y (x =< log y). M(x) means intuitively that 
x is a "medium", i.e. not so big number. Then we can easily deduce 

 (i) M(0), (ii) forall x (M(x) => M(x+1)), and (iii) not M(1024). 

That is, medium numbers constitute an initial part of all numbers 
which is closed under successor, but bounded by 1024. Note, that 
the above basic property of logarithm is used here. Once "all" 
numbers are closed under + and therefore under multiplication by 2, 
then the logarithmically bounded numbers in M are closed under 
successor operation. 

Then deduce step-by step:

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

The last sentence gives a contradiction. (Just in the line of the 
heap paradox.)

QED. 



Some comments:

This proof consists of (roughly) 1000 of routine steps, each 
involving up to (roughly) 1000 of symbols (we should use numerals 
0+1+1+...+1 instead of decimal notations like 1000). Altogether 
this is about 1,000,000 symbols. It could be made shorter by 
allowing in an appropriate way the decimal notations for the 
numerals. Anyway, 1,000,000 of symbols (or the like) is quite 
feasible even for a human being. Contemporary computers can do 
much more. Thus, whether this proof can be made considerably 
shorter is interesting, but not so crucial question. Anyway, 
we are usually presenting only an idea of a proof which should 
be sufficiently convincing to be (feasibly) formalizable. 

Another important point about this proof is that, if written 
down in the natural deduction style, it is *not normal*. 
Also, if written in the Gentsen sequent calculus, it involves 
the *cut rule*. Moreover, it is impossible to normalize this 
derivation or to eliminsate using the cut rule in it 
*if* we require that the proof should contain (intuitively) 
only feasible number of symbols. (Details and motivation 
for the restriction to the normal derivations is omitted.) 

Therefore the axiom 

forall y (log log y < 10)

(considered above as the assumption to derive a contradiction)
may be considered as (feasibly) consistent with the axioms on 
0, 1, +, log and < mentioned above. The resulting formal theory, 
called FEAS and based on the ***restricted*** classical logic 
with only normal (or cut-free) deductions allowed, formalizes 
the intuitive and vague concept of feasible numbers so that 
2^1024 is considered (quite plausibly) as non-feasible. 

Therefore the deduction presented above is *not* a contradiction 
of FEAS. It only demonstrates an interesting peculiarity of this 
system. This peculiarity requires some separate comments... 

Whether we like or dislike such kind of consistency of FEAS, 
we could play with this or any similar theory to realize what 
is the concept of feasible numbers so formalized and thereby  
made to be mathematical, quite rigorous one: We have an intuition 
put in the framework of a formal system. This is exactly in the 
line of the usual mathematical activity: making to be precise 
any idea what we want to consider -- be that geometry or the 
idea of infinitesimals or of feasible numbers or of anything else. 

In particular, the heap paradox finds some formal solution via 
FEAS and the predicate M above. 

More on this topic is presented in 
http://www.csc.liv.ac.uk/~sazonov/papers/lcc.ps


Vladimir Sazonov


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