34
$\begingroup$

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?

Improve this question
$\endgroup$
10
  • 2
    $\begingroup$ I repeat my conjecture that this depends on the implementation of $\zeta$ (that is, the choice of Gödel coding and fixed point). I think by varying those parameters in how $\zeta$ is written, you can force it to be either provable, disprovable, or independent. $\endgroup$
    – Akiva Weinberger
    Commented Aug 12, 2022 at 16:24
  • $\begingroup$ That might sound reasonable, except that one might also have found it reasonable for the Rosser sentence as well, but it isn't true for the Rosser sentence---they are all independent. $\endgroup$
    – Joel David Hamkins
    Commented Aug 12, 2022 at 16:34
  • $\begingroup$ In the modal proof of Löb's theorem on Wikipedia, all you really need are certain facts about the modal operator (i.e., necessitation, internal necessitation, and box distibutivity). You don't really need the fact it is the provability predicate. Doesn't the modal operator $\square A$ that represents "there is a proof of $A$, and no shorter proof of $\neg A$" satisfy all these needed conditions? For example, if $\vdash A$, then we can search for a proof of $A$, and directly verify that no shorter proof yields $\neg A$, hence $\vdash \square A$. $\endgroup$
    – Pace Nielsen
    Commented Aug 12, 2022 at 17:14
  • 3
    $\begingroup$ Pace, I tried something that basically amounts to that, but it seems to be difficult to think about internal necessitation ⊢□p→□□p. And even ⊢□(p→q)→(□p→□q) is not so clear. $\endgroup$
    – Joel David Hamkins
    Commented Aug 12, 2022 at 17:43
  • $\begingroup$ Here's an observation: doesn't $\lnot\zeta$ (let's call it $\eta$) make the same assertion? $\zeta$ asserts that, of the two, $\zeta$ gets proved first; $\eta$ asserts $\eta$ gets proved first. $\endgroup$
    – Akiva Weinberger
    Commented Aug 12, 2022 at 23:02

2 Answers 2

Reset to default
22
$\begingroup$

As Akiva Weinberger conjectured, this depends on the implementation.

Indeed, $0=0$ is a sentence of this type, i.e. $0=0$ is equivalent to the claim that there is a proof of $0=0$ that is shorter than all proofs of its negation, since we can prove this and check, by enumeration, that the proof is shorter than all proofs of its negation, and two tautologies are equivalent.

Similarly, $0=1$ is equivalent to the claim that there is a proof of $0=1$ that is shorter than all proofs of its negation, since we can disprove this and check, by enumeration, that there is no shorter proof, and two contradictions are equivalent.

I concur with Akiva's conjecture that there also exist undecidable sentences of this type.

Even for Rosser sentences, while they are all undecidable, I don't know if there is reason to believe they are all equivalent to each other (as Gödel and Löb sentences are). I don't think Rosser-type operations have unique fixed points.

Improve this answer
$\endgroup$
9
  • 5
    $\begingroup$ Will, thanks very much for this answer! +1 It's too bad that the notion isn't more robust. I'm going to wait and see if someone can find an independent instance. But also, I would say that your argument is not about "the implementation" of the system, but rather about the choice of the fixed-point, even for a fixed standard implementation. Indeed, assuming consistency, your analysis of the two trivial fixed points work with any implementation. $\endgroup$
    – Joel David Hamkins
    Commented Aug 12, 2022 at 19:24
  • 4
    $\begingroup$ Volker Halbach emphasizes that merely being a fixed-point is sometimes not what we mean by saying that a sentence expresses a self-referential assertion, because of the kinds of examples like yours. I wonder whether we can say something about a sentence $\zeta$ that is more literally expressing that "$\ulcorner\zeta\urcorner$ is the Godel code of a sentence that is provable before any proof of its negation"? $\endgroup$
    – Joel David Hamkins
    Commented Aug 12, 2022 at 19:32
  • 5
    $\begingroup$ It does indeed depend on the implementation. Kurahashi (Henkin sentences and local reflection principles for Rosser provability, APAL 167(2):73-94, 2016) shows that there are standard proof predicates such that the Rosser provability predicates based on them have provable and refutable fixed points only (Theorem 4.2), and that there are other standard proof predicates such that their Rosser provability predicates have independent fixed points (Corollary 4.1). $\endgroup$
    – user103227
    Commented Aug 12, 2022 at 22:00
  • 4
    $\begingroup$ See also Question 7.2 of Halbach & Visser (Self-reference in arithmetic II, RSL 7(4):692-712, 2014) and the ensuing discussion, which seems to imply that the fixed point of a Rosser provability predicate, as obtained by the canonical Gödel diagonalisation, can not be independent. $\endgroup$
    – user103227
    Commented Aug 12, 2022 at 22:00
  • 2
    $\begingroup$ @user103227 Why not make that a separate answer rather than just a comment? $\endgroup$
    – Akiva Weinberger
    Commented Aug 14, 2022 at 14:18
9
$\begingroup$

As Akiva Weinberger and Will Sawin have already pointed out, the answer does depend on the details of the of the formalisation of the notion of proof.

Let's fix some terminology: Given a proof predicate $\mathrm{Prf}_\tau(x,y)$, the corresponding provability predicate $\mathrm{Pr}_\tau(x)$ is defined as $\exists y \mathrm{Prf}_\tau(x,y)$, and the corresponding Rosser provability predicate as $\exists y (\mathrm{Prf}_\tau(x,y) \land \forall z \leq y \lnot \mathrm{Prf}_\tau(\lnot x,z))$. A provability predicate is standard if it agrees, provably in PA, with "the ordinary" provability predicate. A fixed point of a provability predicate $\mathrm{Pr}(x)$ is often called a Henkin sentence.

Now, Kurahashi (Henkin sentences and local reflection principles for Rosser provability, APAL 167(2):73-94, 2016) shows that there are standard proof predicates such that their corresponding Rosser provability predicates have provable and refutable Henkin sentences only (Theorem 4.2), and that there are other standard proof predicates such that their Rosser provability predicates have independent Henkin sentences (Corollary 4.1).

See also Question 7.2 of Halbach & Visser (Self-reference in arithmetic II, RSL 7(4):692-712, 2014) and the ensuing discussion, which seems to imply that the fixed point of a Rosser provability predicate, as obtained by the canonical Gödel diagonalisation, can not be independent.

Improve this answer
$\endgroup$
2
  • $\begingroup$ Wait, how do you square Kurahashi's Corollary 4.1 (some fixed points are independent) with Halbach & Visser (none can be)? $\endgroup$
    – Akiva Weinberger
    Commented Sep 13, 2022 at 0:18
  • 1
    $\begingroup$ Not all fixed points are obtained by the canonical Gödel diagonalisation. As pointed out by Will Sawin, both 0 = 0 and 0 = 1 are fixed points of "the ordinary" Rosser provability predicate, but at most one of these sentences (and probably none of them) is the result of applying the diagonal lemma to the ordinary Rosser provability predicate. They still satisfy the desired provable equivalence, though. Moreover, the Rosser provability predicate of Kurahashi's Corollary 4.1 is based on a standard provability predicate, but not on "the ordinary" one. $\endgroup$
    – user103227
    Commented Sep 13, 2022 at 6:51

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .