# [FOM] primer on vagueness

Thu May 26 14:25:34 EDT 2005

```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)

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

QED.

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

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