# Theory Goedel_Formula

```chapter ‹Gödel Formulas›

(*<*)
theory Goedel_Formula imports Diagonalization Derivability_Conditions
begin
(*>*)

text ‹Gödel formulas are defined by diagonalizing the negation of the provability predicate.›

locale Goedel_Form =
― ‹Assuming the @{term fls} (False) connective gives us negation:›
Deduct2_with_False
var trm fmla Var FvarsT substT Fvars subst
eql cnj imp all exi
fls
num
prv bprv
+
Repr_SelfSubst
var trm fmla Var FvarsT substT Fvars subst
num
eql cnj imp all exi
prv bprv
enc
S
+
HBL1
var trm fmla Var FvarsT substT Fvars subst
num
eql cnj imp all exi
prv bprv
enc
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
begin

text ‹The Gödel formula.
NB, we speak of "the" Gödel formula because the diagonalization function makes a choice.›
definition φG :: 'fmla where "φG ≡ diag (neg P)"

lemma φG[simp,intro!]: "φG ∈ fmla"
and
Fvars_φG[simp]: "Fvars φG = {}"
unfolding φG_def PP_def by auto

lemma bprv_φG_eqv:
"bprv (eqv φG (neg (PP ⟨φG⟩)))"
unfolding φG_def PP_def using bprv_diag_eqv[of "neg P"] by simp

lemma prv_φG_eqv:
"prv (eqv φG (neg (PP ⟨φG⟩)))"
using bprv_prv[OF _ _ bprv_φG_eqv, simplified] .

end ― ‹context @{locale Goedel_Form}›

text ‹Adding cleanly representable proofs to the assumptions
behind Gödel formulas:›

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

text ‹... and extending the sublocale relationship @{locale CleanRepr_Proofs} < @{locale HBL1}:›
sublocale Goedel_Form_Proofs < Goedel_Form where P = P by standard

context Goedel_Form_Proofs
begin

lemma bprv_φG_eqv_not_exi_PPf:
"bprv (eqv φG (neg (exi yy (PPf (Var yy) ⟨φG⟩))))"
proof-
have P: "P = exi yy Pf" using P_def by (simp add: PPf_def2)
hence "subst P ⟨φG⟩ xx = subst (exi yy Pf) ⟨φG⟩ xx" by auto
hence "subst P ⟨φG⟩ xx = exi yy (subst Pf ⟨φG⟩ xx)" by simp
thus ?thesis using bprv_φG_eqv by (simp add: wrepr.PP_def PPf_def2)
qed

lemma prv_φG_eqv_not_exi_PPf:
"prv (eqv φG (neg (exi yy (PPf (Var yy) ⟨φG⟩))))"
using bprv_prv[OF _ _ bprv_φG_eqv_not_exi_PPf, simplified] .

lemma bprv_φG_eqv_all_not_PPf:
"bprv (eqv φG (all yy (neg (PPf (Var yy) ⟨φG⟩))))"
by (rule B.prv_eqv_trans[OF _ _ _ bprv_φG_eqv_not_exi_PPf B.prv_neg_exi_eqv_all_neg]) auto

lemma prv_φG_eqv_all_not_PPf:
"prv (eqv φG (all yy (neg (PPf (Var yy) ⟨φG⟩))))"
using bprv_prv[OF _ _ bprv_φG_eqv_all_not_PPf, simplified] .

lemma bprv_eqv_all_not_PPf_imp_φG:
"bprv (imp (all yy (neg (PPf (Var yy) ⟨φG⟩))) φG)"
using bprv_φG_eqv_all_not_PPf by (auto intro: B.prv_imp_eqvER)

lemma prv_eqv_all_not_PPf_imp_φG:
"prv (imp (all yy (neg (PPf (Var yy) ⟨φG⟩))) φG)"
using bprv_prv[OF _ _ bprv_eqv_all_not_PPf_imp_φG, simplified] .

end ― ‹context @{locale Goedel_Form_Proofs}›

(*<*)
end
(*>*)
```