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