theory Surprise_Paradox imports Incompleteness.Goedel_I Incompleteness.Pseudo_Coding begin text ‹ The Surprise Paradox comes in a few variations, one being the following: \begin{quote} A judge sentences a felon to death by hanging, to be executed at noon the next week, Monday to Friday. As an extra punishment, the judge does not disclose the day of the hanging and promises the felon that it will come at a surprise. The felon, probably a logician, then concludes that he cannot be hanged on Friday, as by then it would not longer be a surprise. Using this fact and similar reasoning, he cannot be hanged on Thursday, and so on. He reaches the conclusion that he cannot be hanged at all, and contently returns to his cell. Wednesday, at noon, the hangman comes to the very surprised felon, and executes him. \end{quote} Obviously, something is wrong here: Does the felon reason wrongly? It looks about right. Or is the judge lying? But his prediction became true! It is an interesting exercise to try to phrase the Surprise Paradox in a rigorous manner, and see this might clarify things. In 1964, Frederic Fitch suggested a formulation that refines the notion of ``surprise'' as ``cannot be proven from the given assumptions'' \<^cite>‹Fitch›. To formulate that, we need propositions that reference their own provability, so just as Fitch builds on Gödel's work, we build on Paulson's formalisation of Gödel's incompleteness theorems in Isabelle \<^cite>‹Incompleteness›. › section ‹Excluded or› text ‹Although the proof goes through with regular disjunction, Fitch phrases the judge's proposition using exclusive or, so we add syntax for that.› abbreviation Xor :: "fm ⇒ fm ⇒ fm" (infix "XOR" 120) where "Xor A B ≡ (A OR B) AND ((Neg A) OR (Neg B))" section ‹Formulas with variables› text ‹ In Paulson's formalisation of terms and formulas, only terms carry variables. This is sufficient for his purposes, because the proposition that is being diagonalised needs itself as a parameter to @{term_type PfP}, which does take a term (which happens to be a quoted formula). In order to stay close to Fitch, we need the diagonalised proposition to occur deeper in a quotation of a few logical conjunctions. Therefore, we build a small theory of formulas with variables (``holed'' formulas). These support substituting a formula for a variable, this substitution commutes with quotation, and closed holed formulas can be converted to regular formulas. In our application, we do not need holes under an quantifier, which greatly simplifies things here. In particular, we can use @{command datatype} and @{command fun}. ›