Theory Abstract_Second_Goedel

chapter ‹Abstract Formulation of Gödel's Second Incompleteness Theorem›

(*<*)
theory Abstract_Second_Goedel imports Abstract_First_Goedel Derivability_Conditions
begin
(*>*)

text ‹We assume all three derivability conditions, and assumptions
behind Gödel formulas:›
locale Goedel_Second_Assumptions =
HBL1_2_3
  var trm fmla Var FvarsT substT Fvars subst
  num
  eql cnj imp all exi
  prv bprv
  enc
  P
+
Goedel_Form
  var trm fmla Var num FvarsT substT Fvars subst
  eql cnj imp all exi
  fls
  prv bprv
  enc
  S
  P
for
var :: "'var set" and trm :: "'trm set" and fmla :: "'fmla set"
and Var FvarsT substT Fvars subst
and num
and eql cnj imp all exi
and prv bprv
and enc (‹⟨_⟩›)
and S
and P
and fls
begin

lemma P_G:
"bprv (imp (PP ⟨φG⟩) (PP ⟨fls⟩))"
proof-
  have 0: "prv (imp φG (neg (PP ⟨φG⟩)))"
  using prv_φG_eqv by (intro prv_imp_eqvEL) auto
  have 1: "bprv (PP ⟨imp φG (neg (PP ⟨φG⟩))⟩)"
  using HBL1_PP[OF _ _ 0] by simp
  have 2: "bprv (imp (PP ⟨φG⟩) (PP ⟨neg (PP ⟨φG⟩)⟩))"
  using HBL2_imp2[OF _ _  _ _ 1] by simp
  have 3: "bprv (imp (PP ⟨φG⟩) (PP ⟨PP ⟨φG⟩⟩))"
    using HBL3[OF φG] by simp
  have 23: "bprv (imp (PP ⟨φG⟩)
                      (cnj (PP ⟨PP ⟨φG⟩⟩)
                           (PP ⟨neg (PP ⟨φG⟩)⟩)))"
  using B.prv_imp_cnj[OF _ _ _ 3 2] by simp
  have 4: "bprv (imp (cnj (PP ⟨PP ⟨φG⟩⟩)
                          (PP ⟨neg (PP ⟨φG⟩)⟩))
                     (PP ⟨fls⟩))"
    using HBL2[of "PP ⟨φG⟩" fls] unfolding neg_def[symmetric] by simp
  show ?thesis using B.prv_prv_imp_trans[OF _ _ _ 23 4] by simp
qed

text ‹First the "direct", positive formulation:›
lemma goedel_second_pos:
assumes "prv (neg (PP ⟨fls⟩))"
shows "prv fls"
proof-
  note PG = bprv_prv[OF _ _ P_G, simplified]
  have "prv (neg (PP ⟨φG⟩))"
  using PG assms unfolding neg_def by (rule prv_prv_imp_trans[rotated 3]) auto
  hence "prv φG" using prv_φG_eqv by (rule prv_eqv_prv_rev[rotated 2]) auto
  thus ?thesis
  ―‹The only part of Goedel's first theorem that is needed:›
  using goedel_first_theEasyHalf_pos by simp
qed

text ‹Then the more standard, counterpositive formulation:›
theorem goedel_second:
"consistent ⟹ ¬ prv (neg (PP ⟨fls⟩))"
using goedel_second_pos unfolding consistent_def by auto


text ‹It is an immediate consequence of Gödel's Second HLB1, HLB2 that
(assuming consistency)  @{term "prv (neg (PP ⟨φ⟩))"} holds for no sentence, be it
provable or not. The theory is omniscient about what it can prove
(thanks to HLB1), but completely ignorant about what it cannot prove.›

corollary not_prv_neg_PP:
assumes c: "consistent" and [simp]: "φ ∈ fmla" "Fvars φ = {}"
shows "¬ prv (neg (PP ⟨φ⟩))"
proof
  assume 0: "prv (neg (PP ⟨φ⟩))"
  have "prv (imp fls φ)" by simp
  hence "bprv (PP ⟨imp fls φ⟩)" by (intro HBL1_PP) auto
  hence "bprv (imp (PP ⟨fls⟩) (PP ⟨φ⟩))" by (intro HBL2_imp2) auto
  hence "bprv (imp (neg (PP ⟨φ⟩)) (neg (PP ⟨fls⟩)))" by (intro B.prv_imp_neg_rev) auto
  from prv_imp_mp[OF _ _ bprv_prv[OF _ _ this, simplified] 0, simplified]
  have "prv (neg (PP ⟨fls⟩))" .
  thus False using goedel_second[OF c] by simp
qed

end ― ‹context @{locale Goedel_Second_Assumptions}›

(*<*)
end
(*>*)