Vladimir.Sazonov at liverpool.ac.uk
Wed Oct 17 20:07:19 EDT 2007
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).
This message was sent using IMP, the Internet Messaging Program.
More information about the FOM