The Coq mailing list

[Emilio Jesús Gallego Arias <e AT x80.org>]

"R. Pollack" 
<rpollack0 AT gmail.com>
 writes:

> ​Nelson was not as nutty as this might suggest.  He took the view that
> natural number induction is not predicative, because one quantifies over
> all natural numbers.  In his classic monograph "Predicative Arithmetic" he
> discusses formal systems​ that are predicative in his sense. IIRC such
> systems do not prove totality of exponentiation, so Godel's Theorem may be
> unprovable.

Just to be clear I wasn't meaning "nutty" [not that I would dare to even
qualify scientist of that caliper] but indeed I was thinking of the
exponentiation story.

IMVHO a system where exponentiation is not total does quality as
"radical", but of course totally acceptable if you are an
ultrafinitist. I think it is safe to assume that all the computational
meta-theory of systems such as Coq takes place in a
finite-but-memory-unbounded Turing machine.

E.