The Coq mailing list

[Siddharth Bhat <siddu.druid AT gmail.com>]

What is a "finite" but memory unbounded turing machine? Asking since I have never heard that term before :)

Thanks

Siddharth

On Wed 2 May, 2018, 22:08 Emilio Jesús Gallego Arias, <e AT x80.org> wrote:

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

--

Sending this from my phone, please excuse any typos!