By the way, there are other reasons that we use quining to study decision theories within (virtual) mathematical universes. Most importantly, it lets us play with the logic of provability in a straightforward way, which gives us some really nice polynomial-time tools for analyzing the outcomes. See Benja’s modal UDT implementation in Haskell and my intro to why this works (especially Sections 6 and 7).
Of course, there are things outside that scope we want to study, but for the moment provability logic is a good lamppost under which we can search for keys.
By the way, there are other reasons that we use quining to study decision theories within (virtual) mathematical universes. Most importantly, it lets us play with the logic of provability in a straightforward way, which gives us some really nice polynomial-time tools for analyzing the outcomes. See Benja’s modal UDT implementation in Haskell and my intro to why this works (especially Sections 6 and 7).
Of course, there are things outside that scope we want to study, but for the moment provability logic is a good lamppost under which we can search for keys.