[FOM] Feasible and Utterable Numbers

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

Quoting Karlis Podnieks <Karlis.Podnieks at mii.lu.lv> Mon, 24 Jul 2006:

> The following posting by Harvey Friedman may become relevant to this 
> discussion:
> http://www.cs.nyu.edu/pipermail/fom/2006-February/009764.html.
>
> When reading it, I prepared a kind of proposal, but did not post it 
> then (suspecting naivety of the idea). Now, it follows.
>
> [Start of quote]
> ...
> The axioms of T0
> R0.
> (forall x)(Rx implies RSx).
> ...
> [End of quote.]
>
> What about the following version of T0?
>
> Let us start with the system T00 whose language is 0,S,+, *, ^, R1, 
> R2, R3, R4 where

Do you assume also the ordinary axioms describing 0,S,+, *, ^, that 
(semi-formally) Sx is different from all y < or = x, that +, *, ^ 
behave as usually?


> R1, R2, R3, R4 are unary predicate symbols. Equality is assumed.
>
> R1(0).
> R2(0).
> R3(0).
> R4(0).
> (forall x)(R1(x) implies R1(Sx)).
> (forall x, y) [ R2(x) & R2(y) implies R2(Sx) & R2(x+y) ].
> (forall x, y) [ R3(x) & R3(y) implies R3(Sx) & R3(x+y) & R3(x*y) ].
> (forall x, y) [ R4(x) & R4(y) implies R4(Sx) & R4(x+y) & R4(x*y) &
> R4(x^y) ].
> ...
>
> Thus, in T00, we have, for any term t allowed in the language, an 
> easy (relative to t) proof of R4(t) . But proving of R3(t), R2(t) and 
> - especially of R1(t) may be, for some t, much harder.

No, not much harder.

According to a well-known idea of V. Orevkov, we can formally prove in 
a quite feasible number of steps for some minor variation of T00 
(assuming the ordinary classical logic which you seems do not intend to 
restrict) that quite a big number (given by the exponential tower 
2^(2^(2^...^2)) of the height 1000) belongs to R1. (See the simple 
exposition in my paper "On feasible numbers".) Therefore the effects 
you want to demonstrate require a restriction on logic (see the op. 
cit.).


>
> But, of course, proving of R1(t) for all t-s becomes easy by 
> postulating the traditional induction:
> F0 & (forall x) (Fx->FSx) -> (forall x) Fx.

As R.Parikh has shown in his paper "Feasibility in arithmetic" (JSL, 
1971), (for much bigger t) this depends on whether the predicates Ri 
above are allowed to participate in the induction formula F. (In this 
framework no restriction on the underlying logic is necessary to 
demonstrate that it is consistent that the exponential tower of the 
height roughly 2^1000 belongs neither to R1 nor R2 nor R3. Note that 
Parikh considered R1 or R2 or R3, but not R4, as possybly staying for 
"feasible".)


> Or, at least, by postulating its consequence (as in Robinson's system):
> (forall x) (~(x=0) -> (exists y)(x=Sy)).

Here I do not understand how this highly weak and "innocent" axiom on 
the predecessor can help to prove existence in R1 of huge numbers.

>
> What kind of arithmetic would arise, if we would replace the 
> traditional induction by the following one?
>
> F0 & (forall x, y) [ Fx & Fy implies FSx & F(x+y) & F(x*y) & F(x^y) ] 
> -> (forall x) Fx.

This is evidently a weakening of the ordinary Induction Schema. But I 
would like to understand what is its intuitive background or goal? For 
example, the ordinary Bounded Induction has the goal to have a 
restricted class of provably recursive functions. If "provably 
recursive" means "provably total Turing computable" then this gives 
rise exactly to polynomial time computability. In particular, Bounded 
Induction does not prove that exponential is total function (what can 
be considered as "practically" true and therefore as a kind of appeal 
in favour of Bounded Induction). In other respects Bounded Induction is 
sufficiently strong allowing us to prove "whatever we want", what is 
also a good point. What about the above version of Induction Axiom? At 
least, what about any preliminary but desirably articulate 
considerations or hopes, etc. on what it is good for?

What I see, is that T=T00 + the above Induction Axiom proves forall x 
R4(x). Thus, R4 serves as a universe of "all" numbers in T. It seems 
consistent with T (and would be quite reasonable) that R1 is proper 
subset of R2 which is proper subset of R3 which is proper subset of the 
universe R4. This way Ri would hopefully model some "degrees of (non-) 
feasibility". (See also my other posting to FOM today.)

One question is how strong is the above weak Induction to prove 
"whatever we want", like in Bounded Arithmetic?

But what I really want to have (even more than the strength of 
Induction) it is that R1(2^1000) or even R2(2^1000) should be 
non-provable in T. However, this is not possible (at least for a quite 
small, innocent variation of T where, as we mentioned above, Orevkov?s 
proof could be carried out showing that even much bigger than 2^1000 
"tower" number belongs to R1).

Thus, the above weakening of induction is still too strong to approach 
to "true" feasibility and therefore the underlying logic should 
inevitably be restricted like in my paper "On feasible numbers".


Kind regards,

Vladimir Sazonov


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