A `natural' theorem not provable in PA?
Timothy Y. Chow
tchow at math.princeton.edu
Mon Jun 15 12:49:02 EDT 2020
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
More information about the FOM
mailing list