# Theory Loeb

```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
(*>*)

```