Forgive me if I’m missing something but as far as I can tell, this line of inquiry was already pursued to its logical conclusion (namely, an Agda-verified quinean proof of Löb’s theorem) in this paper by Jason Gross, Jack Gallagher and Benya Fallenstein.
Thanks for raising this! I assume you’re talking about this part?
They explore a pretty interesting set-up, but they don’t avoid the narrowly-self-referential sentence Ψ:
So, I don’t think their motivation was the same as mine. For me, the point of trying to use a quine is to try to get away from that sentence, to create a different perspective on the foundations for people that find that kind of sentence confusing, but who find self-referential documents less confusing. I added a section “Further meta-motivation (added Nov 26)” about this in the OP.
Forgive me if I’m missing something but as far as I can tell, this line of inquiry was already pursued to its logical conclusion (namely, an Agda-verified quinean proof of Löb’s theorem) in this paper by Jason Gross, Jack Gallagher and Benya Fallenstein.
Thanks for raising this! I assume you’re talking about this part?
They explore a pretty interesting set-up, but they don’t avoid the narrowly-self-referential sentence Ψ:
So, I don’t think their motivation was the same as mine. For me, the point of trying to use a quine is to try to get away from that sentence, to create a different perspective on the foundations for people that find that kind of sentence confusing, but who find self-referential documents less confusing. I added a section “Further meta-motivation (added Nov 26)” about this in the OP.