A `natural' theorem not provable in PA?

[Arnon Avron]

Recently I came across a rather new paper: "Fusible numbers and Peano Arithmetic", by
Erickson, Nivasch, and Xu (https://arxiv.org/abs/2003.14342).
[2003.14342] Fusible numbers and Peano Arithmetic<https://arxiv.org/abs/2003.14342>
If you have a disability and are having trouble accessing information on this website or need materials in an alternate format, contact web-accessibility at cornell.edu for assistance.web-accessibility at cornell.edu for assistance.
arxiv.org
One of the results of this paper is the following:

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

Now a theorem about the termination of an algorithm, especially one that was
introduced while investigating a mathematical subject that had been
inspired by a mathematical riddle involving fuses (see in the paper),
seems to me as `natural' as one might wish.

I would like to know whether other people in this list agree or disagree with that.

Arnon Avron

-------------- next part --------------
An HTML attachment was scrubbed...
URL: </pipermail/fom/attachments/20200614/eca8f46e/attachment.html>