Solovay’s Theorem and the Unexpected Examination

I discuss two versions of the “unexpected examination” paradox, and produce mathematically rich formalizations of the paradoxes in the setting of Peano arithmetic. In the first section I examine the classical paradox and show how a straightforward formalization of the paradoxical reasoning leads naturally to a proof of Gödel’s second incompleteness theorem. In the second section, I introduce a generalization of the classical paradox and show how a formalization of this more general paradox leads to a proof of Solovay’s arithmetical completeness theorem for provability logic. I infer that Ramsey’s thesis, separating logical paradoxes from mathematically inert epistemological paradoxes, is false, and offer some thoughts on Ramsey’s oversight.