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