diff --git a/thys/Surprise_Paradox/Surprise_Paradox.thy b/thys/Surprise_Paradox/Surprise_Paradox.thy --- a/thys/Surprise_Paradox/Surprise_Paradox.thy +++ b/thys/Surprise_Paradox/Surprise_Paradox.thy @@ -1,225 +1,225 @@ 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}. \ 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) where "(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 begin fun quot_hfm :: "hfm \ tm" where "quot_hfm (HVar name) = (Var name)" - | "quot_hfm (HFm A) = \A\" + | "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 .. end -lemma subst_quot_hfm[simp]: "subst i \P\ \A\ = \A(i:::=P)\" +lemma subst_quot_hfm[simp]: "subst i \P\ \A\ = \A(i:::=P)\" by (induction A) auto fun hfm_to_fm :: "hfm \ fm" where "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" where "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\" +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 \Q\<^sub>1\ and \Q\<^sub>2\ represent the propositions that the hanging occurs on the first resp.\@ the second day, but these can obviously be any propositions. \ context fixes Q\<^sub>1 :: fm and Q\<^sub>2 :: fm assumes Q_closed: "supp Q\<^sub>1 = {}" "supp Q\<^sub>2 = {}" begin 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 = Q\<^sub>1 AND Neg (PfP \HVar X0 HIMP HFm Q\<^sub>1\) XOR - Q\<^sub>2 AND Neg (PfP \HVar X0 HAND HNeg (HFm Q\<^sub>1) HIMP (HFm Q\<^sub>2)\)" + "H = Q\<^sub>1 AND Neg (PfP \HVar X0 HIMP HFm Q\<^sub>1\) XOR + Q\<^sub>2 AND Neg (PfP \HVar X0 HAND HNeg (HFm Q\<^sub>1) HIMP (HFm Q\<^sub>2)\)" - definition P where "P = (SOME P. {} \ P IFF H(X0 ::= \P\))" + definition P where "P = (SOME P. {} \ P IFF H(X0 ::= \P\))" - lemma P': "{} \ P IFF H(X0 ::= \P\)" + lemma P': "{} \ P IFF H(X0 ::= \P\)" proof- from diagonal[where \ = "H" and i = X0] - obtain \ where "{} \ \ IFF H(X0 ::= \\\)". + obtain \ where "{} \ \ IFF H(X0 ::= \\\)". thus ?thesis unfolding P_def by (rule someI) qed 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 - (Q\<^sub>1 AND Neg (PfP \P IMP Q\<^sub>1\) XOR - Q\<^sub>2 AND Neg (PfP \P AND Neg Q\<^sub>1 IMP Q\<^sub>2\))" + (Q\<^sub>1 AND Neg (PfP \P IMP Q\<^sub>1\) XOR + Q\<^sub>2 AND Neg (PfP \P AND Neg Q\<^sub>1 IMP Q\<^sub>2\))" 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 Q\<^sub>1) IMP Q\<^sub>2" by (intro propositional_calculus "7_E") - lemma 10: "{} \ PfP \(P AND Neg Q\<^sub>1) IMP Q\<^sub>2\" + lemma 10: "{} \ PfP \(P AND Neg Q\<^sub>1) IMP Q\<^sub>2\" using 8 by (rule proved_imp_proved_PfP) lemmas "10_I" = 10[THEN thin0] lemma 11: "{} \ P IMP Q\<^sub>1" by (intro propositional_calculus "7_E" "10_I") - lemma 12: "{} \ PfP \P IMP Q\<^sub>1\" + lemma 12: "{} \ PfP \P IMP Q\<^sub>1\" 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") end 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 others.\ 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')) = + 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)) = + 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)\" + "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) end diff --git a/thys/Surprise_Paradox/document/root.tex b/thys/Surprise_Paradox/document/root.tex --- a/thys/Surprise_Paradox/document/root.tex +++ b/thys/Surprise_Paradox/document/root.tex @@ -1,68 +1,70 @@ \documentclass[11pt,a4paper]{article} \usepackage{isabelle,isabellesym} \usepackage[utf8]{inputenc} % further packages required for unusual symbols (see also % isabellesym.sty), use only when needed +\usepackage[ngerman]{babel} % for guillemots + %\usepackage{amssymb} %for \, \, \, \, \, \, %\, \, \, \, \, %\, \, \ %\usepackage{eurosym} %for \ %\usepackage[only,bigsqcap]{stmaryrd} %for \ %\usepackage{eufrak} %for \ ... \, \ ... \ (also included in amssymb) %\usepackage{textcomp} %for \, \, \, \, \, %\ % this should be the last package used \usepackage{pdfsetup} % urls in roman style, theory text in math-similar italics \urlstyle{rm} \isabellestyle{it} \begin{document} \title{The Surprise Paradox} \author{Joachim Breitner\\ Programming Paradigms Group\\ Karlsruhe Institute for Technology\\ \url{breitner@kit.edu}} \maketitle \begin{abstract} In 1964, Fitch showed that the paradox of the surprise hanging can be resolved by showing that the judge’s verdict is inconsistent. His formalization builds on Gödel’s coding of provability. In this theory, we reproduce his proof in Isabelle, building on Paulson’s formalisation of Gödel’s incompleteness theorems. \end{abstract} \tableofcontents \bigskip % sane default for proof documents \parindent 0pt\parskip 0.5ex % generated text of all theories \input{session} % optional bibliography \bibliographystyle{abbrv} \bibliography{root} \end{document} %%% Local Variables: %%% mode: latex %%% TeX-master: t %%% End: