Theory Loebs_Theorem

chapter‹Löb's Theorem›

(*  Title:       Löb's Theorem
    Author:      Janis Bailitis, 2024
    Maintainer:  Janis Bailitis
*)

section "Preliminaries"

text‹This formalisation relies on Paulson's formalisation of Gödel's incompleteness theorems.›

theory Loebs_Theorem
  imports Goedel_II Goedel_I Quote 
begin

section "Needed Facts on HF and Paulson's Provability Predicate"

text‹The formalised proof of Löb's theorem below relies on a few facts about the deduction rules
of HF set theory and Paulson's provability predicate \<^cite>‹paulson_companion›.
All these facts follow readily from results that Paulson already formalised.›

text‹The modus ponens rule for the provability predicate.›

lemma PfP_inner_ModPon: assumes "ground_fm α" "ground_fm β" shows "{} ⊢ PfP «α IMP β» IMP PfP «α» IMP PfP «β»"
proof -
  have "{} ⊢ α IMP (α IMP β) IMP β"
    by blast
  then have aux: "{} ⊢ PfP «α» IMP PfP «α IMP β» IMP PfP «β»"
    using assms
    using qp0.quote_all_MonPon2_PfP_ssubst
    by (auto simp: qp0.quote_all_MonPon2_PfP_ssubst ground_fm_aux_def) (** This is fully inspired by a proof of Paulson *)
  then have "{ PfP «α IMP β»,  PfP «α» } ⊢  PfP «β»"
    by (metis anti_deduction)
  then have "{ PfP «α», PfP «α IMP β» } ⊢  PfP «β»"
     by (metis rotate2)
  thus ?thesis
     by (metis Imp_I)
 qed

text‹Slight reformulation of @{thm PfP_inner_ModPon}
where one of the implications is on the meta level.›

lemma PfP_distr: assumes "ground_fm α" "ground_fm β" "{} ⊢ PfP «α IMP β»" shows "{} ⊢ PfP «α» IMP PfP «β»" 
proof -
  have "{} ⊢ α IMP β"
    using assms
    by (metis proved_iff_proved_PfP)
  thus ?thesis
    using assms
    by (metis Imp_I MonPon_PfP_implies_PfP)
qed

text‹The provability predicate also satisfies internal necessitation.›

lemma Int_nec: assumes "ground_fm δ" shows "{} ⊢ PfP «δ» IMP PfP «PfP «δ»»"
  by (auto simp: Provability ground_fm_aux_def supp_conv_fresh)

text‹Fact on HF set theory stating that implications are transitive. Follows readily from the 
deduction theorem (@{thm anti_deduction}).›

lemma Imp_trans: assumes "{} ⊢ α IMP β" "{} ⊢ β IMP γ" shows "{} ⊢ α IMP γ"
proof -
  have "{α} ⊢ β" 
    using assms(1)
    by (metis anti_deduction)
  moreover have "{β} ⊢ γ"
    using assms(2)
    by (metis anti_deduction)
  ultimately have "{α} ⊢ γ"
    by (metis rcut1)
  thus ?thesis
    by (metis Imp_I)
qed

text‹Specialisation of the S deduction rule (@{thm S}) for empty contexts.›

lemma S': assumes "{} ⊢ α IMP β IMP γ" "{} ⊢ α IMP β" shows "{} ⊢ α IMP γ"
proof -
  have "{} ∪ {} ⊢ α IMP γ"
    using assms
    by (metis S)
  thus ?thesis
    by simp
qed

section "Proof of Löb's Theorem"

text‹The proof of Löb's theorem for HF set theory and Paulson's provability predicate, roughly
following the paper version by Smith \<^cite>‹smith2020›. The key ideas in the proof are due to
Löb \<^cite>‹loeb1955› himself, but Smith gives a much more structured version.›

theorem Loeb: assumes "ground_fm α" "{} ⊢ PfP «α» IMP α" shows "{} ⊢ α"
proof -
  obtain k::name
    where atoms: "atom k ♯ α"
    by (metis obtain_fresh)
  obtain δ where del: "{} ⊢ δ IFF ((PfP (Var k)) IMP α)(k::=«δ»)"
             and suppd: "supp δ = supp ((PfP (Var k)) IMP α) - {atom k}"
    by (metis diagonal)
  then have "{} ⊢ δ IFF ((PfP (Var k))(k::=«δ») IMP α(k::=«δ»))"
    by (metis SyntaxN.Neg SyntaxN.Disj)
  moreover have "atom k ♯ α"
    using assms
    by simp
  ultimately have "{} ⊢ δ IFF ((PfP (Var k))(k::=«δ») IMP α)"
    by (metis forget_subst_fm)
  then have diag: "{} ⊢ δ IFF ((PfP «δ») IMP α)"
    by simp
  then have del_supp: "ground_fm δ"
    using assms
    using suppd
    by (auto simp: ground_fm_aux_def supp_conv_fresh) 
  then have imp_supp: "ground_fm  (PfP «δ» IMP α)"
    using assms
    using suppd
    by (auto simp: ground_fm_aux_def supp_conv_fresh) 
  then have prf_del_supp: "ground_fm (PfP «δ»)"
    using suppd
    by (auto simp: ground_fm_aux_def supp_conv_fresh) 
  then have "{} ⊢ δ IMP ((PfP «δ») IMP α)"
    by (metis Conj_E2 Iff_def Iff_sym diag) 
  then have "{} ⊢ PfP «δ IMP ((PfP «δ») IMP α)»"
    by (metis  proved_iff_proved_PfP)
  then have "{} ⊢ PfP «δ» IMP (PfP «PfP «δ» IMP α»)"
    using imp_supp
    using del_supp
    by (metis PfP_distr)
  moreover have "{} ⊢ PfP «PfP «δ» IMP α» IMP PfP «PfP «δ»» IMP PfP «α»"
    using assms(1)
    using prf_del_supp
    by (metis PfP_inner_ModPon)
  ultimately have "{} ⊢  PfP «δ» IMP PfP «PfP «δ»» IMP PfP «α»"
    by (metis Imp_trans)
  then have "{} ⊢ PfP «δ» IMP PfP «α»"
    using del_supp
    by (metis Int_nec S')
  then have imp_a: "{} ⊢ PfP «δ» IMP α"
    using assms(2)
    by (metis Imp_trans)
  then have "{} ⊢ PfP «δ»"
    using diag
    by (metis Iff_MP2_same proved_iff_proved_PfP)
  thus ?thesis
    using imp_a
    by (metis MP_same)
qed
  
end