chapter ‹Löb's Theorem› (*<*) theory Loeb imports Loeb_Formula Derivability_Conditions begin (*>*) text ‹We have set up the formalization of Gödel's first (easy half) and Gödel's second so that the following generalizations, leading to Löb's theorem, are trivial modifications of these, replacing negation with "implies @{term φ}" in all proofs.› locale Loeb_Assumptions = HBL1_2_3 var trm fmla Var FvarsT substT Fvars subst num eql cnj imp all exi prv bprv enc P + Loeb_Form var trm fmla Var num FvarsT substT Fvars subst eql cnj imp all exi prv bprv enc S P for var :: "'var set" and trm :: "'trm set" and fmla :: "'fmla set" and Var num FvarsT substT Fvars subst and eql cnj imp all exi and prv bprv and enc ("⟨_⟩") and S and P begin text ‹Generalization of $\mathit{goedel\_first\_theEasyHalf\_pos}$, replacing @{term fls} with a sentence @{term φ}:› lemma loeb_aux_prv: assumes φ[simp]: "φ ∈ fmla" "Fvars φ = {}" and p: "prv (φL φ)" shows "prv φ" proof- have "prv (imp (PP ⟨φL φ⟩) φ)" using assms prv_eqv_prv[OF _ _ p prv_φL_eqv] by auto moreover have "bprv (PP ⟨φL φ⟩)" using HBL1[OF φL[OF φ] _ p] unfolding PP_def by simp from bprv_prv[OF _ _ this, simplified] have "prv (PP ⟨φL φ⟩)" . ultimately show ?thesis using PP φL by (meson assms enc in_num prv_imp_mp) qed lemma loeb_aux_bprv: assumes φ[simp]: "φ ∈ fmla" "Fvars φ = {}" and p: "bprv (φL φ)" shows "bprv φ" proof- note pp = bprv_prv[OF _ _ p, simplified] have "bprv (imp (PP ⟨φL φ⟩) φ)" using assms B.prv_eqv_prv[OF _ _ p bprv_φL_eqv] by auto moreover have "bprv (PP ⟨φL φ⟩)" using HBL1[OF φL[OF φ] _ pp] unfolding PP_def by simp ultimately show ?thesis using PP φL by (meson assms enc in_num B.prv_imp_mp) qed text ‹Generalization of $\mathit{P\_G}$, the main lemma used for Gödel's second:› lemma P_L: assumes φ[simp]: "φ ∈ fmla" "Fvars φ = {}" shows "bprv (imp (PP ⟨φL φ⟩) (PP ⟨φ⟩))" proof- have 0: "prv (imp (φL φ) (imp (PP ⟨φL φ⟩) φ))" using prv_φL_eqv by (intro prv_imp_eqvEL) auto have 1: "bprv (PP ⟨imp (φL φ) (imp (PP ⟨φL φ⟩) φ)⟩)" using HBL1_PP[OF _ _ 0] by simp have 2: "bprv (imp (PP ⟨φL φ⟩) (PP ⟨imp (PP ⟨φL φ⟩) φ⟩))" using HBL2_imp2[OF _ _ _ _ 1] by simp have 3: "bprv (imp (PP ⟨φL φ⟩) (PP ⟨PP ⟨φL φ⟩⟩))" using HBL3[OF φL[OF φ] _] by simp have 23: "bprv (imp (PP ⟨φL φ⟩) (cnj (PP ⟨PP ⟨φL φ⟩⟩) (PP ⟨imp (PP ⟨φL φ⟩) φ⟩)))" using B.prv_imp_cnj[OF _ _ _ 3 2] by simp have 4: "bprv (imp (cnj (PP ⟨PP ⟨φL φ⟩⟩) (PP ⟨imp (PP ⟨φL φ⟩) φ⟩)) (PP ⟨φ⟩))" using HBL2[of "PP ⟨φL φ⟩" φ] by simp show ?thesis using B.prv_prv_imp_trans[OF _ _ _ 23 4] by simp qed text ‹Löb's theorem generalizes the positive formulation Gödel's Second ($\mathit{goedel\_second}$). In our two-provability-relation framework, we get two variants of Löb's theorem. A stronger variant, assuming @{term prv} and proving @{term bprv}, seems impossible.› theorem loeb_bprv: assumes φ[simp]: "φ ∈ fmla" "Fvars φ = {}" and p: "bprv (imp (PP ⟨φ⟩) φ)" shows "bprv φ" proof- have "bprv (imp (PP ⟨φL φ⟩) φ)" by (rule B.prv_prv_imp_trans[OF _ _ _ P_L p]) auto hence "bprv (φL φ)" by (rule B.prv_eqv_prv_rev[OF _ _ _ bprv_φL_eqv, rotated 2]) auto thus ?thesis using loeb_aux_bprv[OF φ] by simp qed theorem loeb_prv: assumes φ[simp]: "φ ∈ fmla" "Fvars φ = {}" and p: "prv (imp (PP ⟨φ⟩) φ)" shows "prv φ" proof- note PL = bprv_prv[OF _ _ P_L, simplified] have "prv (imp (PP ⟨φL φ⟩) φ)" by (rule prv_prv_imp_trans[OF _ _ _ PL p]) auto hence "prv (φL φ)" by (rule prv_eqv_prv_rev[OF _ _ _ prv_φL_eqv, rotated 2]) auto thus ?thesis using loeb_aux_prv[OF φ] by simp qed text ‹We could have of course inferred $\mathit{goedel\_first\_theEasyHalf\_pos}$ and $\mathit{goedel\_second}$ from these more general versions, but we leave the original arguments as they are more instructive.› end ― ‹context @{locale Loeb_Assumptions}› (*<*) end (*>*)