Theory Surprise_Paradox
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}.
›