1 chapter‹Löb's Theorem based on Paulson's provability predicate›
   2 
   3 theory Loeb
   4 imports Incompleteness.Goedel_II Incompleteness.Goedel_I Incompleteness.Quote 
   5 begin
   6 
   7 text‹Some lemmas in preparation of Löb's theorem (needed to give the proof of Löb's theorem as outlined in the thesis.›
   8 lemma PfP_inner_ModPon: assumes "ground_fm α" "ground_fm β" shows  "{} ⊢ PfP «α IMP β» IMP  PfP «α» IMP PfP «β»"
   9 proof -
  10   have H: "{} ⊢ α IMP (α IMP β) IMP β"
  11     by blast
  12   then have aux: "{} ⊢ PfP «α» IMP PfP «α IMP β» IMP PfP «β»"
  13     using assms
  14     using H
  15     using qp0.quote_all_MonPon2_PfP_ssubst
  16     by (auto simp: qp0.quote_all_MonPon2_PfP_ssubst ground_fm_aux_def) (** This is fully inspired by a proof of Paulson *)
  17   then have  "{ PfP «α IMP β»,  PfP «α» } ⊢  PfP «β»"
  18     by (metis anti_deduction)
  19   then have  "{ PfP «α», PfP «α IMP β» } ⊢  PfP «β»"
  20      by (metis rotate2)
  21   thus "{} ⊢ PfP «α IMP β» IMP  PfP «α» IMP PfP «β»"
  22      by (metis Imp_I)
  23  qed
  24 
  25 lemma PfP_distr: assumes "ground_fm α" " ground_fm β" "{} ⊢ PfP «α IMP β»" shows "{} ⊢ PfP «α» IMP PfP «β»" 
  26 proof -
  27   have H: "{} ⊢ α IMP β"
  28     using assms
  29     by (metis proved_iff_proved_PfP)
  30   thus "{} ⊢ PfP «α» IMP PfP «β»"
  31     using assms
  32     by (metis Imp_I MonPon_PfP_implies_PfP)
  33 qed
  34 
  35 lemma Imp_trans: assumes "{} ⊢ α IMP β" "{} ⊢ β IMP γ" shows "{} ⊢ α IMP γ"
  36 proof -
  37   have H: "{α} ⊢ β" 
  38     using assms(1)
  39     by (metis anti_deduction)
  40   then have "{β} ⊢ γ"
  41     using assms(2)
  42     by (metis anti_deduction)
  43   then have "{α} ⊢ γ"
  44     using H
  45     by (metis rcut1)
  46   thus ?thesis
  47     by (metis Imp_I)
  48 qed
  49 
  50 lemma Int_nec: assumes "ground_fm δ" shows "{} ⊢ PfP «δ» IMP PfP «PfP «δ»»"
  51   by (auto simp: Provability ground_fm_aux_def supp_conv_fresh)
  52 
  53 lemma S': assumes "{} ⊢ α IMP β IMP γ" "{} ⊢ α IMP β" shows "{} ⊢ α IMP γ"
  54 proof -
  55   have "{} ∪ {} ⊢ α IMP γ"
  56     using assms
  57     by (metis S)
  58   thus ?thesis
  59     by simp
  60 qed
  61 
  62 text‹The proof of Löb's theorem›
  63 
  64 theorem Loeb: assumes "ground_fm α" "{} ⊢ PfP «α» IMP α" shows "{} ⊢ α"
  65 proof -
  66   obtain k::name
  67     where atoms: "atom k ♯ α"
  68     by (metis obtain_fresh)
  69   obtain δ where del: "{} ⊢ δ IFF ((PfP (Var k)) IMP α)(k::=«δ»)"
  70              and suppd: "supp δ = supp ((PfP (Var k)) IMP α) - {atom k}"
  71     by (metis  diagonal)
  72   then have diag: "{} ⊢ δ IFF ((PfP (Var k))(k::=«δ») IMP α(k::=«δ»))"
  73     by (metis SyntaxN.Neg SyntaxN.Disj)
  74   moreover have  "atom k ♯ α"
  75     using assms
  76     by simp
  77   then have diag': "{} ⊢ δ IFF ((PfP (Var k))(k::=«δ») IMP α)"
  78     using diag
  79     by (metis forget_subst_fm)
  80   then have diag'': "{} ⊢ δ IFF ((PfP «δ») IMP α)"
  81     by simp
  82   then have del_supp: "ground_fm δ"
  83     using assms
  84     using suppd
  85      by (auto simp: ground_fm_aux_def supp_conv_fresh) 
  86   then have imp_supp: "ground_fm  (PfP «δ» IMP α)"
  87     using assms
  88     using suppd
  89     by  (auto simp: ground_fm_aux_def supp_conv_fresh) 
  90   then have prf_del_supp: "ground_fm (PfP «δ»)"
  91     using suppd
  92      by  (auto simp: ground_fm_aux_def supp_conv_fresh) 
  93   then  have H2: "{} ⊢ δ IMP ((PfP «δ») IMP α)"
  94     by (metis Conj_E2 Iff_def Iff_sym diag'') 
  95   then have H3: "{} ⊢ PfP «δ IMP ((PfP «δ») IMP α)»"
  96     by (metis  proved_iff_proved_PfP H2)
  97   then have H4: "{} ⊢ PfP «δ» IMP (PfP «PfP «δ» IMP α»)"
  98     using imp_supp
  99     using del_supp
 100     by (metis PfP_distr)
 101   then have H5: "{} ⊢ PfP «PfP «δ» IMP α» IMP PfP «PfP «δ»» IMP PfP «α»"
 102     using assms(1)
 103     using prf_del_supp
 104     by (metis PfP_inner_ModPon)
 105   then have "{} ⊢  PfP «δ» IMP PfP «PfP «δ»» IMP PfP «α»"
 106     using H4
 107     by (metis Imp_trans)
 108   then have "{} ⊢ PfP «δ» IMP PfP «α»"
 109     using del_supp
 110     by (metis Int_nec S')
 111   then have H6: "{} ⊢ PfP «δ» IMP α"
 112     using assms(2)
 113     by (metis Imp_trans)
 114   then have "{} ⊢ δ"
 115     using diag''
 116     by (metis Iff_MP2_same)
 117   then have "{} ⊢ PfP «δ»"
 118     by (metis  proved_iff_proved_PfP)
 119   thus ?thesis
 120     using H6
 121     by (metis MP_same)
 122 qed
 123   
 124 end