My belief is that this one was fine, because self-reference occurs only under quotation, so it can be constructed by modal fixpoint / quining. But that is why the base definition of “good” is built non-recursively.
Is that what you were talking about?
(Edit: I’ve made an update to the post to be clearer on this.)
My belief is that this one was fine, because self-reference occurs only under quotation, so it can be constructed by modal fixpoint / quining. But that is why the base definition of “good” is built non-recursively.
Is that what you were talking about?
(Edit: I’ve made an update to the post to be clearer on this.)
Sorry, I was wrong. By Lob’s theorem, all versions of goodnew are provably equivalent, so they will trust each other.