A `natural' theorem not provable in PA?

[Timothy Y. Chow]

Arnon Avron wrote:

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

I like it!

This is the first time I've heard about this work, although it has 
apparently been around for at least ten years.  The OEIS has an entry for 
fusible numbers:

http://oeis.org/A188545

If you chase down the references then you'll see that the authors made 
some mistakes in their original analysis of the problem.  Presumably those 
mistakes have been corrected, although obviously it would be good for more 
people to look at the proofs and confirm that they're right.

Tim