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