[FOM] Feasible and Utterable Numbers

[Karlis Podnieks]

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
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.

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

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.

My best wishes,
Karlis Podnieks