[FOM] Feasible and Utterable Numbers

[Charles Silver]

On Aug 4, 2006, at 11:52 AM, V.Sazonov at csc.liv.ac.uk wrote:
>
> First note that, M is considered not as a primitive predicate.
>
> Second, we can restrict logical derivations to be normal natural
> deduction proofs (or cut free sequent style proof). But it is
> intuitively more appealing to formulate (or think about) the
> restriction as:
>
> * abbreviation of terms is not allowed (and formal derivations should
> be, of course, of feasible length).
>
> 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"?
	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.
	Multiplication is missing, so 2*x cannot abbreviate x + x, and in  
fact all abbreviations are forbidden   (as well as induction? ).    
All formulas are of feasible length.
	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.

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

	Thanks for the information.

Charlie Silver