Timeline for Self-referential Quinean proof of Löb's Theorem
Current License: CC BY-SA 4.0
7 events
when toggle format | what | by | license | comment | |
---|---|---|---|---|---|
Dec 1, 2022 at 11:17 | comment | added | Martín S | @BenedictEastaugh That resonates with my intuition that we'll just be "moving the diagonal lemma around". Thanks for this resource, I'll look into it! | |
Nov 28, 2022 at 14:01 | comment | added | Benedict Eastaugh | It seems like a proof of this sort would just be pushing the fixed-point lemma into the Gödel numbering. See for example Appendix A of Halbach and Visser (2014). | |
S Nov 28, 2022 at 13:39 | history | suggested | CommunityBot | CC BY-SA 4.0 |
Fix cite of article
|
Nov 28, 2022 at 11:28 | review | Suggested edits | |||
S Nov 28, 2022 at 13:39 | |||||
Nov 26, 2022 at 22:43 | comment | added | Martín S | @NikWeaver Yes, that's my intuition as well. I guess the hope would be for some diagonal method to prove "I can prove that "This proof is a proof of C"", where "This proof" is specified as a quined object by some properties. | |
Nov 25, 2022 at 17:29 | comment | added | Nik Weaver | I'm having trouble with the intuition behind this. The question is whether the intuitive template describes a valid proof. The only questionable step is (1), so we can say that it is a valid proof if and only if (1) is valid. That is, it is valid if and only if it is valid. I don't see how to go further than that. | |
Nov 25, 2022 at 13:27 | history | asked | Martín S | CC BY-SA 4.0 |