A `natural' theorem not provable in PA?

[Dennis E. Hamilton]

From: fom-bounces at cs.nyu.edu <fom-bounces at cs.nyu.edu> On Behalf Of Arnon
Avron
Sent: Sunday, June 14, 2020 02:44
To: Foundations of Mathematics <fom at cs.nyu.edu>
Cc: Arnon Avron <aa at tauex.tau.ac.il>
Subject: A `natural' theorem not provable in PA?

[ . ]

Consider the algorithm "M(x): if x < 0 return -x, else return M(x -M(x -
1))/2." Then
M terminates on real inputs, although PA cannot prove the statement "M
terminates on all
natural inputs."

[ . ]

Consider

M(0) = M(0-M(-1))/2 = M(0-1)/2 = 1/2

And if 0 is not natural enough, then consider

M(1) = M(1-M(0))/2 = M(1/2)/2 = M(1/2 - M(-1/2))/4 = M(0)/4 = 1/8

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