Logic - 2020-10-27

« first day (1532 days earlier) ← previous day next day → last day (1285 days later) »

1:20 PM

A: Intuitionistically unprovable statements about the natural numbers

> "As an illustrative example, Goodstein's theorem is known to be unprovable in PA but provable in a stronger theory, and it can be understood purely as a statement about numbers. (This is in contrast to Gödel statements, which, while they technically are statements about numbers, can't readily b...

@MaliceVidrine @user2103480: ^ Do you have an example of a Really Simple sentence that HA cannot prove but PA can? Namely, that is not constructed using any sort of sequence encoding or computation-related facts?

4 hours later…

Malice Vidrine

5:36 PM

@user21820 - I don't know! There is almost certainly something simple, like some function we can't prove total because it's usually defined piecewise.

@user21820 - There's Francois's answer here, but I think the overhead it glosses over is not insubstantial.

user21820

@MaliceVidrine It's pretty much the same as all the computability-based examples.

I think there must be simple examples, but have never heard of them.

Although one could argue that polynomial zeros make it so much more interesting (and difficult) than just halting problem kind of stuff.

But that thread you found has another example that almost makes it:

A: What can be proven in Peano arithmetic but not Heyting arithmetic?

According to Harvey Friedman, the following theorem is provable in PA but not HA: Every polynomial $P:\mathbb{Z}^n \to \mathbb{Z}^m$ with integer coefficients assumes a value closest to the origin. That is, there is a value which is at least as close to the origin, in the Euclidean distance...