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.