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
3 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Sep 13, 2022 at 6:51 | comment | added | user103227 | 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. | |
| Sep 13, 2022 at 0:18 | comment | added | Akiva Weinberger | Wait, how do you square Kurahashi's Corollary 4.1 (some fixed points are independent) with Halbach & Visser (none can be)? | |
| Aug 18, 2022 at 9:32 | history | answered | user103227 | CC BY-SA 4.0 |