A `natural' theorem not provable in PA?

[Dennis E. Hamilton]

-----Original Message-----
From: fom-bounces at cs.nyu.edu <fom-bounces at cs.nyu.edu> On Behalf Of Timothy
Y. Chow
Sent: Wednesday, June 17, 2020 09:47
To: fom at cs.nyu.edu
Subject: Re: A `natural' theorem not provable in PA?

> Dennis Hamilton wrote:
>>
>> so M:Z -> Q and no wonder the termination cannot be proven in PA.

> I don't understand this objection.  It sounds like an implicit claim that
statements about rational numbers cannot be expressed in the first-order
language of arithmetic, which is obviously false.  Maybe I misunderstand?

It is my foolishness.  I didn't recognize that denumerability of Q meant
there had to be a way to express the function in a suitable
representation/encoding in N.

 I'm not so clear that the statement "M terminates on all natural inputs" is
very natural though, since it amounts to confirming (encoded) M(N/1)
termination, and that depends on termination of *some* M(p/q)'s where q > 1
and does not divide p.  Hurts my tiny brain.

Dennis