chapter ‹Abstract Formulation of Gödel's Second Incompleteness Theorem› (*<*) theory Abstract_Second_Goedel imports Abstract_First_Goedel Derivability_Conditions begin (*>*) text ‹We assume all three derivability conditions, and assumptions behind Gödel formulas:› locale Goedel_Second_Assumptions = HBL1_2_3 var trm fmla Var FvarsT substT Fvars subst num eql cnj imp all exi prv bprv enc P + Goedel_Form var trm fmla Var num FvarsT substT Fvars subst eql cnj imp all exi fls prv bprv enc S P for var :: "'var set" and trm :: "'trm set" and fmla :: "'fmla set" and Var FvarsT substT Fvars subst and num and eql cnj imp all exi and prv bprv and enc ("⟨_⟩") and S and P and fls begin lemma P_G: "bprv (imp (PP ⟨φG⟩) (PP ⟨fls⟩))" proof- have 0: "prv (imp φG (neg (PP ⟨φG⟩)))" using prv_φG_eqv by (intro prv_imp_eqvEL) auto have 1: "bprv (PP ⟨imp φG (neg (PP ⟨φG⟩))⟩)" using HBL1_PP[OF _ _ 0] by simp have 2: "bprv (imp (PP ⟨φG⟩) (PP ⟨neg (PP ⟨φG⟩)⟩))" using HBL2_imp2[OF _ _ _ _ 1] by simp have 3: "bprv (imp (PP ⟨φG⟩) (PP ⟨PP ⟨φG⟩⟩))" using HBL3[OF φG] by simp have 23: "bprv (imp (PP ⟨φG⟩) (cnj (PP ⟨PP ⟨φG⟩⟩) (PP ⟨neg (PP ⟨φG⟩)⟩)))" using B.prv_imp_cnj[OF _ _ _ 3 2] by simp have 4: "bprv (imp (cnj (PP ⟨PP ⟨φG⟩⟩) (PP ⟨neg (PP ⟨φG⟩)⟩)) (PP ⟨fls⟩))" using HBL2[of "PP ⟨φG⟩" fls] unfolding neg_def[symmetric] by simp show ?thesis using B.prv_prv_imp_trans[OF _ _ _ 23 4] by simp qed text ‹First the "direct", positive formulation:› lemma goedel_second_pos: assumes "prv (neg (PP ⟨fls⟩))" shows "prv fls" proof- note PG = bprv_prv[OF _ _ P_G, simplified] have "prv (neg (PP ⟨φG⟩))" using PG assms unfolding neg_def by (rule prv_prv_imp_trans[rotated 3]) auto hence "prv φG" using prv_φG_eqv by (rule prv_eqv_prv_rev[rotated 2]) auto thus ?thesis ―‹The only part of Goedel's first theorem that is needed:› using goedel_first_theEasyHalf_pos by simp qed text ‹Then the more standard, counterpositive formulation:› theorem goedel_second: "consistent ⟹ ¬ prv (neg (PP ⟨fls⟩))" using goedel_second_pos unfolding consistent_def by auto text ‹It is an immediate consequence of Gödel's Second HLB1, HLB2 that (assuming consistency) @{term "prv (neg (PP ⟨φ⟩))"} holds for no sentence, be it provable or not. The theory is omniscient about what it can prove (thanks to HLB1), but completely ignorant about what it cannot prove.› corollary not_prv_neg_PP: assumes c: "consistent" and [simp]: "φ ∈ fmla" "Fvars φ = {}" shows "¬ prv (neg (PP ⟨φ⟩))" proof assume 0: "prv (neg (PP ⟨φ⟩))" have "prv (imp fls φ)" by simp hence "bprv (PP ⟨imp fls φ⟩)" by (intro HBL1_PP) auto hence "bprv (imp (PP ⟨fls⟩) (PP ⟨φ⟩))" by (intro HBL2_imp2) auto hence "bprv (imp (neg (PP ⟨φ⟩)) (neg (PP ⟨fls⟩)))" by (intro B.prv_imp_neg_rev) auto from prv_imp_mp[OF _ _ bprv_prv[OF _ _ this, simplified] 0, simplified] have "prv (neg (PP ⟨fls⟩))" . thus False using goedel_second[OF c] by simp qed end ― ‹context @{locale Goedel_Second_Assumptions}› (*<*) end (*>*)