[FOM] Feasible and Utterable Numbers

[V.Sazonov@csc.liv.ac.uk]

Quoting Charles Silver <silver_1 at mindspring.com> Sat, 05 Aug 2006:

> On Aug 4, 2006, at 11:52 AM, V.Sazonov at csc.liv.ac.uk wrote:

>> See (quite simple) details in my posting to FOM:
>>
>> http://www.cs.nyu.edu/pipermail/fom/2006-February/009746.html
>>
>> Please consider this text as a semi-formal presentation of a quite
>> FORMAL considerations. The mere intuition is highly insufficient in
>> reasoning on feasibility if we pretend to consider this as a
>> mathematical concept.
>
> 	I imagine it takes a while working with the system for it to seem
> natural.   (Is "natural" what is meant by "pretend[ing] to consider
> this as a mathematical concept"?

"Natural" is good (and can be subjective and depending on time), but I 
consider that the main criterion for any idea to be mathematical is 
"adequately formalisable".

For me the question is: can we ever treat feasibility in a 
mathematically rigorous way or it is non-formalisable at all and 
nothing except useless speculations is possible? The answer is: it is 
formalisable, but somewhat unusually. The formalisation could/should be 
probably improved to be more natural. Anyway, it is better to have some 
(adequate) formalisation than nothing at all.


> 	In your paper, I located the following limitations besides those
> listed above.   Are these correct?   Are some missing?
>
> 	Ay log log y <10, meaning that all feasible numbers are < 2 ^1024.

This is *non-logical* axiom saying that we are dealing with numbers 
which can be called feasible as they should be much smaller than 
2^1000. This is, of course not a restriction on the logic. This is 
rather a sufficiently adequate limitation to the subject matter 
(feasibility).


> 	Multiplication is missing, so 2*x cannot abbreviate x + x, and in
> fact all abbreviations are forbidden   (as well as induction? ).

Yes, if we really want to formalise feasibility we must restrict 
ourselves in some way. I see no other way in the framework of formal 
axiomatic approach. Again, forbidding multiplication (unlike forbidding 
abbreviations) is not a limitation on logic.

In principle, we could allow some weak forms of induction as it is 
commented in my paper. In principle, we could also consider 
multiplication as a partial function, as well as exp. We could extend 
this theory by (Turing or other kind of) computability. This is 
potentially a theory of our real world of computations, so, it could be 
quite rich. (I only strongly doubt that Church-Turing Thesis would hold 
in this framework in the lack of multiplication/substitution which are 
necessary for proving that the ordinary Universal Turing machine is 
really universal one - behaves, i.e. imitates other TMs as required).


> All formulas are of feasible length.


Yes, and proofs as well, exactly as in the ordinary (semi-formal) 
mathematics. (Metamathematics is another story.)

> 	You have both Ax (M(x) -> M(x+1) *and*  ⅂Ax (M(x) -> M(x+1)(where M
> is a "middle" number) but no formal contradiction, because the Cut
> rule  (MP) is eliminated from your system.

Formally it is cut rule which is forbidden. But things could be 
presented (in a way, also formally) in more intuitively appealing way:

(*) during a proof terms cannot be abbreviated.

Note that abbreviations are not something external and additional to 
logic. The ordinary quantifier rules allow abbreviation of terms:

Introduction of existential quantifier *introduces* a name for a term; 
then (somewhere later in the proof) elimination of this quantifier 
*uses* this abbreviation of the term. This is forbidden according to 
(*). As a side effect, this also restricts using the cut and modus 
ponens rules (or using non-normal derivations).

The ordinary cut elimination (or normalisation) theorem says that cuts 
can be used because they can be *potentially* eliminated. If we can 
*practically* eliminate the cut rule in a proof, then it is OK. But the 
fact is that it is not always possible. By using the cut rule we can 
trivially prove M(1), M(2),...,M(n),...,M(1000) (for the above M 
defined as M(n) iff exists m (n < log m)) but we can really eliminate 
cut only for the case of not so big n. It is impossible for M(1000). 
So, we have (provable in our theory)

M(0), forall(M(x)->M(x+1) and not M(1000)

without formal contradiction.

So M, being bounded by 1000, has, nevertheless, no last number.

>
> 	One comment:  In ordinary systems, for any sentence phi, if you get
> phi and ⅂phi (i.e., Ax (M(x) -> M(x+1) *and*  ⅂Ax (M(x) -> M(x
> +1)), you already have a contradiction.   So, I imagine that a
> contradiction for your system must also be restricted (to an atomic
> formula?)

In particular, we simultaneously have that M has a last number (see my 
paper), what looks as a formal contradiction. (This is a new unexpected 
fact on feasible numbers in terms of which M is defined! The question 
is what is the meaning of this: the world is continuous and discrete 
simultaneously?? To use this fact for formalising a Feasible 
Nonstandard Analysis?)

But, let us accept:

(**) a system is contradictory if it is trivial in the sense that 
everything is provable. Otherwise, it is considered as consistent and, 
therefore having probably *some* meaning.

In the formal system for feasible numbers we discuss here the negation 
is not a primitive symbol and not-A is *definable* as A => false with 
false a primitive. It is also postulated that false => anything. Once 
false is non-provable, the system is consistent according to the above 
definition. Moreover this system is conservative extension of the 
result of omitting the axiom forall n log log n < 10 with respect to 
existential sentences (i.e. sentences having a concrete computational 
meaning; all these sentences are true in the traditional sense). So, it 
is both non-trivial in the above sense and computationally meaningful. 
On the other hand, some theoretical statements (involving quantifiers 
over the vague semi-set of "all" feasible numbers) have somewhat 
unusual meaning. But the subject matter is very unusual, too, and the 
naive intuition is not very helphul here until more developed one will 
appear while working in such kind of formalisms. (In general, 
mathematical intuition cannot exist in absolute isolation from 
mathematical formalisms.)


All the best,

Vladimir Sazonov



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