Skip to main content
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