Logicians are familiar with the variety of self-referential sentences expressible in the language of arithmetic:

• The Gödel sentence, "this sentence is not provable", which indeed is not provable in whichever base theory that was used when formulating it and hence is true yet unprovable.

• The Rosser sentence, "for any proof of this sentence there is a smaller proof of its negation," which is also true and unprovable. This sentence offers a technical improvement on the Gödel sentence in that the independence of the Rosser sentence can be proved assuming only the consistency of the base theory, whereas Gödel has used $\omega$-consistency.

• The Löb sentence, "this sentence is provable," is indeed provable, remarkably, by Löb's theorem.

My question is about the sentence that we might form by combining the ideas of Rosser and Löb. Namely, by the usual fixed-point methods, we can form a sentence $\zeta$ that PA provably asserts:

$\qquad$"$\zeta$ is provable in PA by a proof that is smaller than any proof of $\neg\zeta$."

We mean "smaller" here, just as with the Rosser sentence, in the sense of the Gödel codes of the proof.

Question. What is the logical status of the combined Rosser-Löb sentence $\zeta$? Is it provable, independent, or what?

This question grew out of discussion on Twitter concerning the recent question of Henry Yuen on MathOverflow, Will this Turing machine find a proof of its halting? and several comments on my answer there.

Namely, one can formulate a version of the question above in the context of computability (and Akiva Weinberger did so in the Twitter thread), by considering the Turing machine program $z$ that searches for proofs that $z$ halts or does not halt, and if it finds a proof of halting before finding any proof of nonhalting, then it halts. Does $z$ halt?

Logicians are familiar with the variety of self-referential sentences expressible in the language of arithmetic:

• The Gödel sentence, "this sentence is not provable", which indeed is not provable in whichever base theory that was used when formulating it and hence is true yet unprovable.

• The Rosser sentence, "for any proof of this sentence there is a smaller proof of its negation," which is also true and unprovable. This sentence offers a technical improvement on the Gödel sentence in that the independence of the Rosser sentence can be proved assuming only the consistency of the base theory, whereas Gödel has used $\omega$-consistency.

• The Löb sentence, "this sentence is provable," is indeed provable, remarkably, by Löb's theorem.

My question is about the sentence that we might form by combining the ideas of Rosser and Löb. Namely, by the usual fixed-point methods, we can form a sentence $\zeta$ that PA provably asserts:

$\qquad$"$\zeta$ is provable in PA by a proof that is smaller than any proof of $\neg\zeta$."

We mean "smaller" here, just as with the Rosser sentence, in the sense of the Gödel codes of the proof.

Question. What is the logical status of the combined Rosser-Löb sentence $\zeta$? Is it provable, independent, or what?

The usual arguments for the Rosser and Löb sentences don't seem to gain any traction on the combined sentence.

This question grew out of discussion on Twitter concerning the recent question of Henry Yuen on MathOverflow, Will this Turing machine find a proof of its halting? and several comments on my answer there.

Namely, one can formulate a version of the question above in the context of computability (and Akiva Weinberger did so in the Twitter thread), by considering the Turing machine program $z$ that searches for proofs that $z$ halts or does not halt, and if it finds a proof of halting before finding any proof of nonhalting, then it halts. Does $z$ halt?

Logicians are familiar with the variety of self-referential sentences expressible in the language of arithmetic:

• The Gödel sentence, "this sentence is not provable", which indeed is not provable in whichever base theory that was used when formulating it and hence is true yet unprovable.

• The Rosser sentence, "for any proof of this sentence there is a smaller proof of its negation," which is also true and unprovable. This sentence offers a technical improvement on the Gödel sentence in that the independence of the Rosser sentence can be proved assuming only the consistency of the base theory, whereas Gödel has used $\omega$-consistency.

• The Löb sentence, "this sentence is provable," is indeed provable, remarkably, by Löb's theorem.

My question is about the sentence that we might form by combining the ideas of Rosser and Löb. Namely, by the usual fixed-point methods, we can form a sentence $\zeta$ that PA provably asserts:

$\qquad$"$\zeta$ is provable in PA by a proof that is smaller than any proof of $\neg\zeta$."

We mean "smaller" here, just as with the Rosser sentence, in the sense of the Gödel codes of the proof.

Question. What is the logical status of the combined Rosser-Löb sentence $\zeta$? Is it provable, independent, or what?

This question grew out of discussion on Twitter concerning the recent question of Henry Yuen on MathOverflow, Will this Turing machine find a proof of its halting? and several comments on my answer there.

Namely, one can formulate a version of the question above in the context of computability, by considering the Turing machine program $z$ that searches for proofs that $z$ halts or does not halt, and if it finds a proof of halting before finding any proof of nonhalting, then it halts. Does $z$ halt?

Logicians are familiar with the variety of self-referential sentences expressible in the language of arithmetic:

• The Gödel sentence, "this sentence is not provable", which indeed is not provable in whichever base theory that was used when formulating it and hence is true yet unprovable.

• The Rosser sentence, "for any proof of this sentence there is a smaller proof of its negation," which is also true and unprovable. This sentence offers a technical improvement on the Gödel sentence in that the independence of the Rosser sentence can be proved assuming only the consistency of the base theory, whereas Gödel has used $\omega$-consistency.

• The Löb sentence, "this sentence is provable," is indeed provable, remarkably, by Löb's theorem.

My question is about the sentence that we might form by combining the ideas of Rosser and Löb. Namely, by the usual fixed-point methods, we can form a sentence $\zeta$ that PA provably asserts:

$\qquad$"$\zeta$ is provable in PA by a proof that is smaller than any proof of $\neg\zeta$."

We mean "smaller" here, just as with the Rosser sentence, in the sense of the Gödel codes of the proof.

Question. What is the logical status of the combined Rosser-Löb sentence $\zeta$? Is it provable, independent, or what?

This question grew out of discussion on Twitter concerning the recent question of Henry Yuen on MathOverflow, Will this Turing machine find a proof of its halting? and several comments on my answer there.

Namely, one can formulate a version of the question above in the context of computability (and Akiva Weinberger did so in the Twitter thread), by considering the Turing machine program $z$ that searches for proofs that $z$ halts or does not halt, and if it finds a proof of halting before finding any proof of nonhalting, then it halts. Does $z$ halt?