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

```