Timeline for What is the logical status of the sentence combining the ideas of Löb and Rosser, "this sentence is provable before any proof of its negation"?
Current License: CC BY-SA 4.0
11 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Aug 8 at 14:38 | vote | accept | Joel David Hamkins | ||
| Aug 18, 2022 at 9:32 | comment | added | user103227 | Thanks, I have turned my comment into an answer. | |
| Aug 14, 2022 at 14:18 | comment | added | Akiva Weinberger | @user103227 Why not make that a separate answer rather than just a comment? | |
| Aug 13, 2022 at 1:12 | comment | added | Joel David Hamkins | Yes.$\quad\quad$ | |
| Aug 12, 2022 at 23:23 | comment | added | Akiva Weinberger | @user103227 Sorry, but what is the Rosser provability predicate? Is it "there's a proof before any disproof"? | |
| Aug 12, 2022 at 22:00 | comment | added | user103227 | 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. | |
| Aug 12, 2022 at 22:00 | comment | added | user103227 | 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). | |
| Aug 12, 2022 at 19:32 | comment | added | Joel David Hamkins | 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"? | |
| Aug 12, 2022 at 19:24 | comment | added | Joel David Hamkins | 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. | |
| Aug 12, 2022 at 18:16 | comment | added | Akiva Weinberger | Oh lol that's kinda funny that those count | |
| Aug 12, 2022 at 17:58 | history | answered | Will Sawin | CC BY-SA 4.0 |