A `natural' theorem not provable in PA?
Dennis E. Hamilton
dennis.hamilton at acm.org
Mon Jun 15 14:12:06 EDT 2020
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.
More information about the FOM
mailing list