[FOM] Feasibility

[Vladimir Sazonov]

To the Moderator: sorry, I added the subject.

On 17 Oct 2007 at 0:30, Vaughan Pratt wrote:

> Number theory will no doubt demand larger numbers, feasibility be 
> damned, but for reasoning about the real world, 2^^6, a stack of six 
> 2's, may well suffice.

1. I realize very well that the usual mathematics demands very large 
numbers, but not because it is its goal to work with very large. 
(Infinity is another story.) This is because of the formalism of FOL 
(first order logic) and because of extensive use of Induction Axiom. 
That is, very large numbers are the consequence (or side effect) of the 
deductive apparatus used. We have no "better" formalisms. Moreover, any 
attempts to find something radically different (like formalizations of 
feasibility I mentioned in my posting) look not so "nice", expressive, 
etc. It even looks strange (see the link in my posting). Anyway, the 
question is whether feasibility can or not be formalized in principle. 
The next question is to improve this in a "nicer" way, then to try to 
make it useful for the ordinary or applied mathematics, etc.

2. Your 2^^6 (vs 2^1000) is the upper bound for various configurations 
potentially possible in the real world, as you write yourself. On the 
other hand 2^1000 is the upper bound to the real world "as it is" (for 
the number of electrons, or the like, may be for the time the world 
could exist in the past or in the future - I do not know). Moreover, 
for my considerations this is even not the most important fact. 2^1000 
is just large enough for our computational activity (the number of bits 
in a computer memory, the number of computational steps, the 
"practical" upper bound for (feasible) natural numbers (in unary 
notation!) we could ever use. For practical purposes we could take even 
smaller upper bound 2^100 or even 2^50 of our capabilities. This can 
serve as an upper bound for the length of formulas and formal 
derivations we could practically use. And if we have a formal 
derivation of 0=1 from some axioms which requires
> 2^1000 symbols (in fact we would have in this
case a much shorter, feasible proof that such an extra long derivation 
of a contradiction exists) then this derivation can be considered as 
imaginary one and ignored. Real mathematical proof is always something 
feasible (written by people or computer).

Of course we can discuss on higher exponential towers (and on longer 
"infinite" rows of natural numbers extending the semiset F mentioned in 
my posting; in fact, I do this in my paper "On feasible numbers"), but 
I would prefer for a while to fix the ideas and appropriate upper bound 
related with F (closed under successor and + but nevertheless upper 
bounded by 2^1000).

Note that postulating that F is upper bounded by 2^10 is contradictory 
even under my formalization. But the above bigger bound 2^1000 makes it 
(feasibly) consistent. (However, "the devil is in the details" which 
are quite formal, but simple enough, and omitted here, and without 
which such an F might look as a nonsense).


Vladimir Sazonov


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