Theory Abstract_First_Goedel

chapter ‹Abstract Formulations of Gödel's First Incompleteness Theorem›

(*<*)
theory Abstract_First_Goedel imports Goedel_Formula Standard_Model_More
begin
(*>*)

section ‹Proof-Theoretic Versions of Gödel's First›

context Goedel_Form
begin

subsection ‹The easy half›

text ‹First the "direct", positive formulation:›
lemma goedel_first_theEasyHalf_pos:
assumes "prv φG"   shows "prv fls"
proof-
  have "prv (neg (PP ⟨φG⟩))" using prv_eqv_prv[OF _ _ assms prv_φG_eqv] by auto
  moreover
  {have "bprv (PP ⟨φG⟩)" using HBL1[OF φG Fvars_φG assms] unfolding PP_def .
   from bprv_prv[OF _ _ this, simplified] have "prv (PP ⟨φG⟩)" .
  }
  ultimately show ?thesis using PP prv_neg_fls by (meson φG enc in_num)
qed

text ‹... then the more standard contrapositive formulation:›
corollary goedel_first_theEasyHalf:
"consistent ⟹ ¬ prv φG"
using goedel_first_theEasyHalf_pos unfolding consistent_def by auto

end ― ‹context @{locale Goedel_Form}›


subsection ‹The hard half›

text ‹The hard half needs explicit proofs:›
context Goedel_Form_Proofs begin

lemma goedel_first_theHardHalf:
assumes oc: "ωconsistent"
shows "¬ prv (neg φG)"
proof
  assume pn: "prv (neg φG)"
  hence pnn: "prv (neg (neg (wrepr.PP ⟨φG⟩)))"
    using prv_eqv_imp_transi num wrepr.PP φG fls neg neg_def prv_φG_eqv prv_eqv_sym
    by (metis (full_types) enc in_num)
  note c = ωconsistent_implies_consistent[OF oc]
  have np: "¬ prv φG" using pn c unfolding consistent_def3 by blast
  have "∀p ∈ num. bprv (neg (PPf p ⟨φG⟩))" using not_prv_prv_neg_PPf[OF _ _ np] by auto
  hence 0: "∀p ∈ num. prv (neg (PPf p ⟨φG⟩))" using not_prv_prv_neg_PPf[OF _ _ np]
    by (fastforce intro: bprv_prv)
  have "¬ prv (neg (neg (exi yy (PPf (Var yy) ⟨φG⟩))))" using 0 oc unfolding ωconsistent_def by auto
  hence "¬ prv (neg (neg (wrepr.PP ⟨φG⟩)))"
    unfolding wrepr.PP_def by (subst P_def) (simp add:  PPf_def2)
  thus False using pnn by auto
qed

theorem goedel_first:
assumes "ωconsistent"
shows "¬ prv φG ∧ ¬ prv (neg φG)"
  using assms goedel_first_theEasyHalf goedel_first_theHardHalf ωconsistent_implies_consistent by blast

theorem goedel_first_ex:
assumes "ωconsistent"
shows "∃ φ. φ ∈ fmla ∧ ¬ prv φ ∧ ¬ prv (neg φ)"
  using assms goedel_first by (intro exI[of _ φG]) blast


end ― ‹context @{locale Goedel_Form_Proofs}›


section ‹Model-Theoretic Versions of Gödel's First›

text ‹The model-theoretic twist is that of additionally proving
the truth of Gödel sentences.›


subsection ‹First model-theoretic version›

locale Goedel_Form_Proofs_Minimal_Truth =
Goedel_Form_Proofs
  var trm fmla Var FvarsT substT Fvars subst
  num
  eql cnj imp all exi
  fls
  prv bprv
  enc
  S
  dsj
  "proof" prfOf encPf
  Pf
+
Minimal_Truth_Soundness
  var trm fmla Var FvarsT substT Fvars subst
  eql cnj imp all exi
  fls
  dsj
  num
  bprv
  isTrue
for
var :: "'var set" and trm :: "'trm set" and fmla :: "'fmla set"
and Var FvarsT substT Fvars subst
and eql cnj imp all exi
and fls
and dsj
and num
and prv bprv
and enc ("⟨_⟩")
and S
and "proof" :: "'proof set" and prfOf encPf
and Pf
and isTrue
begin

text ‹Recall that "consistent" and "$\omega$-consistent" refer to @{term prv}, not to @{term bprv}.›

theorem isTrue_φG:
  assumes "consistent"
  shows "isTrue φG"
proof-
  have "∀ n ∈ num. bprv (neg (PPf n ⟨φG⟩))"
  using not_prv_prv_neg_PPf[OF _ _ goedel_first_theEasyHalf[OF assms]] by auto
  hence "∀ n ∈ num. isTrue (neg (PPf n ⟨φG⟩))" by (auto intro: sound_isTrue)
  hence "isTrue (all yy (neg (PPf (Var yy) ⟨φG⟩)))" by (auto intro: isTrue_all)
  moreover have "isTrue (imp (all yy (neg (PPf (Var yy) ⟨φG⟩))) φG)"
  using bprv_eqv_all_not_PPf_imp_φG by (auto intro!: sound_isTrue)
  ultimately show ?thesis by (rule isTrue_imp[rotated -2]) auto
qed

text ‹The "strong" form of Gödel's First (also asserting the truth of
the Gödel sentences):›

theorem goedel_first_strong:
"ωconsistent ⟹ ¬ prv φG ∧ ¬ prv (neg φG) ∧ isTrue φG"
  using goedel_first isTrue_φG ωconsistent_implies_consistent by blast

theorem goedel_first_strong_ex:
"ωconsistent ⟹ ∃ φ. φ ∈ fmla ∧ ¬ prv φ ∧ ¬ prv (neg φ) ∧ isTrue φ"
  using goedel_first_strong by (intro exI[of _ φG]) blast

end ― ‹context @{locale Goedel_Form_Proofs_Minimal_Truth}›


subsection ‹Second model-theoretic version›

locale Goedel_Form_Minimal_Truth_Soundness_HBL1iff_Compl_Pf =
Goedel_Form
  var trm fmla Var num
  FvarsT substT Fvars subst
  eql cnj imp all exi
  fls
  prv bprv
  enc
  S
  P
+
Minimal_Truth_Soundness_HBL1iff_Compl_Pf
  var trm fmla Var FvarsT substT Fvars subst
  eql cnj imp all exi
  fls
  dsj
  num
  enc
  prv bprv
  P
  isTrue
  Pf
for
var :: "'var set" and trm :: "'trm set" and fmla :: "'fmla set"
and Var FvarsT substT Fvars subst
and eql cnj imp all exi
and fls
and dsj
and num
and prv bprv
and enc ("⟨_⟩")
and S
and isTrue
and P
and Pf


locale Goedel_Form_Minimal_Truth_Soundness_HBL1iff_Compl_Pf_Compl_NegPf =
Goedel_Form_Minimal_Truth_Soundness_HBL1iff_Compl_Pf
  var trm fmla Var FvarsT substT Fvars subst
  eql cnj imp all exi
  fls
  dsj
  num
  prv bprv
  enc
  S
  isTrue
  P
  Pf
+
Minimal_Truth_Soundness_HBL1iff_Compl_Pf_Compl_NegPf
  var trm fmla Var FvarsT substT Fvars subst
  eql cnj imp all exi
  fls
  dsj
  num
  enc
  prv bprv
  P
  isTrue
  Pf
for
var :: "'var set" and trm :: "'trm set" and fmla :: "'fmla set"
and Var FvarsT substT Fvars subst
and eql cnj imp all exi
and fls
and dsj
and num
and prv bprv
and enc ("⟨_⟩")
and S
and isTrue
and P
and Pf
+
assumes prv_ωconsistent: "ωconsistent"

(* Semantic Goedel's first, Goedel-style, second variant
... established as a sublocale statement *)
sublocale
  Goedel_Form_Minimal_Truth_Soundness_HBL1iff_Compl_Pf_Compl_NegPf <
  recover_proofs: Goedel_Form_Proofs_Minimal_Truth
  where prfOf = prfOf and "proof" = "proof" and encPf = encPf
  and prv = prv and bprv = bprv
  by standard

(* ... and here is the explicit statement, inside the locale that
provides all the assumptions *)
context Goedel_Form_Minimal_Truth_Soundness_HBL1iff_Compl_Pf_Compl_NegPf begin
thm recover_proofs.goedel_first_strong

end


section ‹Classical-Logic Versions of Gödel's First›


subsection ‹First classical-logic version›

locale Goedel_Form_Classical_HBL1_rev_prv =
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 num FvarsT substT Fvars subst
and eql cnj imp all exi
and fls
and prv bprv
and enc ("⟨_⟩")
and S
and P
+
assumes
― ‹NB: we don't really need to assume classical reasoning (double negation)
for all formulas, but only for the provability predicate:›
classical_P_prv: "⋀ φ. φ ∈ fmla ⟹ Fvars φ = {} ⟹ let PP = (λt. subst P t xx) in
  prv (neg (neg (PP ⟨φ⟩))) ⟹ prv (PP ⟨φ⟩)"
and
HBL1_rev_prv: "⋀ φ. φ ∈ fmla ⟹ Fvars φ = {} ⟹ prv (PP ⟨φ⟩) ⟹ prv φ"
begin

lemma HBL1_rev:
  assumes f: "φ ∈ fmla" and fv: "Fvars φ = {}" and bp: "bprv (PP ⟨φ⟩)"
  shows "prv φ"
  using assms by (auto intro!: HBL1_rev_prv bprv_prv[OF _ _ bp])

lemma classical_PP_prv: "φ ∈ fmla ⟹ Fvars φ = {} ⟹ prv (neg (neg (PP ⟨φ⟩))) ⟹ prv (PP ⟨φ⟩)"
  using classical_P_prv unfolding PP_def by auto

lemma HBL1_iff: "φ ∈ fmla ⟹ Fvars φ = {} ⟹ bprv (PP ⟨φ⟩) ⟷ prv φ"
  using HBL1 HBL1_rev unfolding PP_def by auto

lemma HBL1_iff_prv: "φ ∈ fmla ⟹ Fvars φ = {} ⟹ prv (PP ⟨φ⟩) ⟷ prv φ"
  by (meson HBL1_PP HBL1_rev_prv PP d_dwf.bprv_prv' enc in_num)

lemma goedel_first_theHardHalf_pos:
assumes "prv (neg φG)"   shows "prv fls"
proof-
  have "prv (neg (neg (PP ⟨φG⟩)))"
    using assms neg_def prv_φG_eqv prv_eqv_imp_transi_rev by fastforce
  hence "prv (PP ⟨φG⟩)" using classical_PP_prv by auto
  hence "prv φG" using Fvars_φG HBL1_rev_prv by blast
  thus ?thesis using assms prv_neg_fls by blast
qed

corollary goedel_first_theHardHalf:
"consistent ⟹ ¬ prv (neg φG)"
  using goedel_first_theHardHalf_pos unfolding consistent_def by auto

theorem goedel_first_classic:
assumes "consistent"
shows "¬ prv φG ∧ ¬ prv (neg φG)"
  using assms goedel_first_theEasyHalf goedel_first_theHardHalf by blast

theorem goedel_first_classic_ex:
assumes "consistent"
shows "∃ φ. φ ∈ fmla ∧ ¬ prv φ ∧ ¬ prv (neg φ)"
  using assms goedel_first_classic by (intro exI[of _ φG]) blast

end ― ‹context @{locale Goedel_Form_Classical_HBL1_rev_prv}›


subsection ‹Second classical-logic version›

locale Goedel_Form_Classical_HBL1_rev_prv_Minimal_Truth_Soundness_TIP =
Goedel_Form_Classical_HBL1_rev_prv
  var trm fmla Var num FvarsT substT Fvars subst
  eql cnj imp all exi
  fls
  prv bprv
  enc
  S
  P
+
Minimal_Truth_Soundness
  var trm fmla Var FvarsT substT Fvars subst
  eql cnj imp all exi
  fls
  dsj
  num
  bprv
  isTrue
for
var :: "'var set" and trm :: "'trm set" and fmla :: "'fmla set"
and Var num FvarsT substT Fvars subst
and eql cnj dsj imp all exi
and fls
and prv bprv
and enc ("⟨_⟩")
and S
and P
and isTrue
+
assumes
―‹Truth of @{term φ} implies provability (TIP) of (the internal representation of) @{term φ}›
TIP: "⋀ φ. φ ∈ fmla ⟹ Fvars φ = {} ⟹
  let PP = (λt. subst P t xx) in
  isTrue (PP ⟨φ⟩) ⟹ prv φ"
begin

lemma TIP_PP: "φ ∈ fmla ⟹ Fvars φ = {} ⟹ isTrue (PP ⟨φ⟩) ⟹ prv φ"
  using TIP unfolding PP_def by auto

theorem isTrue_φG:
  assumes consistent
  shows "isTrue φG"
proof-
  {assume "¬ isTrue φG"
   hence 1: "isTrue (neg φG)" using isTrue_neg by fastforce
   have "bprv (imp (neg φG) (neg (neg (PP ⟨φG⟩))))"
   by (auto simp add: bprv_φG_eqv B.prv_imp_eqvER B.prv_imp_neg_rev)
   from prv_imp_implies_isTrue[OF _ _ _ _ this 1, simplified]
   have "isTrue (neg (neg (PP ⟨φG⟩)))" .
   from isTrue_neg_neg[OF _ _ this, simplified] have "isTrue (PP ⟨φG⟩)" .
   hence "prv φG" using assms TIP_PP by auto
   hence False using goedel_first_classic assms by auto
  }
  thus ?thesis by auto
qed

theorem goedel_first_classic_strong: "consistent ⟹ ¬ prv φG ∧ ¬ prv (neg φG) ∧ isTrue φG"
  using goedel_first_classic isTrue_φG by simp

theorem goedel_first_classic_strong_ex:
"consistent ⟹ ∃ φ. φ ∈ fmla ∧ ¬ prv φ ∧ ¬ prv (neg φ) ∧ isTrue φ"
  using goedel_first_classic_strong by (intro exI[of _ φG]) blast

end ― ‹context @{locale Goedel_Form_Classical_HBL1_rev_prv_Minimal_Truth_Soundness_TIP}›


subsection ‹Third classical-logic version›

locale Goedel_Form_Minimal_Truth_Soundness_HBL1iff_prv_Compl_Pf_Classical =
Goedel_Form
  var trm fmla Var num FvarsT substT Fvars subst
  eql cnj imp all exi
  fls
  prv bprv
  enc
  S
  P
+
Minimal_Truth_Soundness_HBL1iff_prv_Compl_Pf_Classical
  var trm fmla Var FvarsT substT Fvars subst
  eql cnj imp all exi
  fls
  dsj
  num
  enc
  prv bprv
  P
  isTrue
  Pf
for
var :: "'var set" and trm :: "'trm set" and fmla :: "'fmla set"
and Var FvarsT substT Fvars subst
and eql cnj imp all exi
and fls
and dsj
and num
and prv bprv
and enc ("⟨_⟩")
and S
and isTrue
and P
and Pf


sublocale Goedel_Form_Minimal_Truth_Soundness_HBL1iff_prv_Compl_Pf_Classical <
  recover_proofs: Goedel_Form_Classical_HBL1_rev_prv_Minimal_Truth_Soundness_TIP where prv = prv and bprv = bprv
proof (standard, goal_cases classical rev_rpv TIPf)
  case (classical φ)
  then show ?case using HBL1_iff classical_P by (simp add: mts_prv_mts.PP_deff)
next
  case (rev_rpv φ)
  then show ?case using HBL1_iff_prv PP_def by simp
next
  case (TIPf φ)
  then show ?case using classical_P by (simp add: SS_def PP_def mts_prv_mts.TIP)
qed

context Goedel_Form_Minimal_Truth_Soundness_HBL1iff_prv_Compl_Pf_Classical begin
thm recover_proofs.goedel_first_classic_strong
end ―‹context @{locale Goedel_Form_Minimal_Truth_Soundness_HBL1iff_prv_Compl_Pf_Classical}›

(*<*)
end
(*>*)