Theory Surprise_Paradox

theory Surprise_Paradox

text ‹
The Surprise Paradox comes in a few variations, one being the following:

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.

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'' citeFitch. 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 citeIncompleteness.

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}.

datatype hfm =
   HVar name
 | HFm fm
 | HDisj hfm hfm (infixr "HOR" 130)
 | HNeg  hfm

abbreviation HImp :: "hfm  hfm  hfm"  (infixr "HIMP" 125)
  where "HImp A B  HDisj (HNeg A) B"

definition HConj :: "hfm  hfm  hfm"   (infixr "HAND" 135)
  where "HConj A B  HNeg (HDisj (HNeg A) (HNeg B))"

abbreviation HXor :: "hfm  hfm  hfm" (infix "HXOR" 120)
 where "HXor A B  (A HOR B) HAND (HNeg A HOR HNeg B)"

fun  subst_hfm :: "hfm  name  fm  hfm" ("_'(_:::=_')" [1000, 0, 0] 200)
    "(HVar name)(i:::=x) = (if i = name then HFm x else HVar name)"
  | "(HDisj A B)(i:::=x) = HDisj (A(i:::=x)) (B(i:::=x))"
  | "(HNeg A)(i:::=x) = HNeg (A(i:::=x))"
  | "(HFm A)(i:::=x) = HFm A"

lemma subst_hfml_Conj[simp]:
  "(HConj A B)(i:::=x) = HConj (A(i:::=x)) (B(i:::=x))"
 unfolding HConj_def by simp

instantiation hfm :: quot
fun quot_hfm :: "hfm  tm"
   "quot_hfm (HVar name) = (Var name)"
 | "quot_hfm (HFm A) = «A»"
 | "quot_hfm (HDisj A B) = HPair (HTuple 3) (HPair (quot_hfm A) (quot_hfm B))"
 | "quot_hfm (HNeg A) = HPair (HTuple 4) (quot_hfm A)"

instance ..

lemma subst_quot_hfm[simp]: "subst i «P» «A» = «A(i:::=P)»"
  by (induction A) auto

fun hfm_to_fm :: "hfm  fm"
   "hfm_to_fm (HVar name) = undefined"
 | "hfm_to_fm (HFm A) = A"
 | "hfm_to_fm (HDisj A B) = Disj (hfm_to_fm A) (hfm_to_fm B)"
 | "hfm_to_fm (HNeg A) = Neg (hfm_to_fm A)"

lemma hfm_to_fm_Conj[simp]:
  "hfm_to_fm (HConj A B) = Conj (hfm_to_fm A) (hfm_to_fm B)"
unfolding HConj_def Conj_def by simp

fun closed_hfm  :: "hfm  bool"
   "closed_hfm (HVar name)  False"
 | "closed_hfm (HFm A)  True"
 | "closed_hfm (HDisj A B)  closed_hfm A  closed_hfm B"
 | "closed_hfm (HNeg A)  closed_hfm A"

lemma closed_hfm_Conj[simp]:
  "closed_hfm (HConj A B)  closed_hfm A  closed_hfm B"
unfolding HConj_def by simp

lemma quot_closed_hfm[simp]: "closed_hfm A  «A» = «hfm_to_fm A»"
  by (induction A) (auto simp add: quot_fm_def)

declare quot_hfm.simps[simp del]

section ‹Fitch's proof›

text ‹
For simplicity, Fitch (and we) restrict the week to two days. Propositions Q1 and Q2
represent the propositions that the hanging occurs on the first resp.\@ the second day, but
these can obviously be any propositions.

  fixes Q1 :: fm and Q2 :: fm
  assumes Q_closed: "supp Q1 = {}" "supp Q2 = {}"

  text ‹
  In order to define the judge's proposition, which is self-referential, we apply the usual trick
  of defining a proposition with a variable, and then using Gödel's diagonalisation lemma.

  definition H :: fm where
    "H = Q1 AND Neg (PfP «HVar X0 HIMP HFm Q1») XOR 
     Q2 AND Neg (PfP «HVar X0 HAND HNeg (HFm Q1) HIMP (HFm Q2)»)"

  definition P where "P = (SOME P. {}  P IFF H(X0 ::= «P»))"

  lemma P': "{}  P IFF H(X0 ::= «P»)"
    from diagonal[where α = "H" and i = X0]
    obtain δ where "{}  δ IFF H(X0 ::= «δ»)".
    thus ?thesis  unfolding P_def by (rule someI)

  text ‹
  From now on, the lemmas are named after their number in Fitch's paper, and correspond to his
  statements pleasingly closely.

  lemma 7: "{}  P IFF
     (Q1 AND Neg (PfP «P IMP Q1») XOR
      Q2 AND Neg (PfP «P AND Neg Q1 IMP Q2»))"
    using P' unfolding H_def
    by (simp add: Q_closed forget_subst_fm[unfolded fresh_def])
  lemmas "7_E" = 7[THEN thin0, THEN Iff_MP_left', OF Conj_E, OF thin2]

  lemmas propositional_calculus = 
    AssumeH Neg_I Imp_I Conj_E Disj_E ExFalso[OF Neg_E]
    ExFalso[OF rotate2, OF Neg_E] ExFalso[OF rotate3, OF Neg_E]  
  lemma 8: "{}  (P AND Neg Q1) IMP Q2"
    by (intro propositional_calculus "7_E")

  lemma 10: "{}  PfP «(P AND Neg Q1) IMP Q2»"
    using 8 by (rule proved_imp_proved_PfP)
  lemmas "10_I" = 10[THEN thin0]

  lemma 11: "{}  P IMP Q1"
    by (intro propositional_calculus "7_E" "10_I")
  lemma 12: "{}  PfP «P IMP Q1»"
    using 11 by (rule proved_imp_proved_PfP)
  lemmas "12_I" = 12[THEN thin0]

  lemma 13: "{}  Neg P"
    by (intro propositional_calculus "7_E" "10_I" "12_I")

section ‹Substitution, quoting and V-quoting›

text ‹In the end, we did not need the lemma at the end of this section, but it may be useful to

lemma trans_tm_forgets: "atom ` set is ♯* t  trans_tm is t = trans_tm [] t"
  by (induct t rule: tm.induct)
     (auto simp: lookup_notin fresh_star_def fresh_at_base)

lemma vquot_dbtm_fresh: "atom ` V ♯* t  vquot_dbtm V t = quot_dbtm t"
  by (nominal_induct t rule: dbtm.strong_induct)
     (auto simp add: fresh_star_def fresh_at_base)

lemma subst_vquot_dbtm_trans_tm[simp]:
  "atom i  is  atom ` set is ♯* t 
   subst i «t» (vquot_dbtm {i} (trans_tm is t')) =
   quot_dbtm (trans_tm is (subst i t t'))"
  by (nominal_induct t' avoiding: "is" i t rule: tm.strong_induct)
     (auto simp add:  quot_tm_def lookup_notin fresh_imp_notin_env
                      vquot_dbtm_fresh lookup_fresh
           intro: trans_tm_forgets[symmetric])

lemma subst_vquot_dbtm_trans_fm[simp]:
  "atom i  is  atom ` set is ♯* t 
   subst i «t» (vquot_dbfm {i} (trans_fm is A)) =
   quot_dbfm (trans_fm is (subst_fm A i t))"
  by (nominal_induct A avoiding: "is" i t rule: fm.strong_induct)
     (auto simp add: quot_fm_def fresh_Cons)

lemma subst_vquot[simp]:
  "subst i «t» A{i} = «A(i ::= t)»"
  by (nominal_induct A avoiding: i t rule: fm.strong_induct)
     (auto simp add: vquot_fm_def quot_fm_def fresh_Cons)