Theory Loeb_Formula

chapter ‹Löb  Formulas›

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

text ‹The Löb formula, parameterized by a sentence @{term φ}, is defined by diagonalizing @{term "imp P φ"}.›


locale Loeb_Form =
Deduct2
  var trm fmla Var FvarsT substT Fvars subst
  num
  eql cnj imp all exi
  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 prv bprv
and enc ("⟨_⟩")
and S
and P
begin

text ‹The Löb formula associated to a formula @{term φ}:›
definition φL :: "'fmla ⇒ 'fmla" where "φL φ ≡ diag (imp P φ)"

lemma φL[simp,intro]: "⋀φ. φ ∈ fmla ⟹ Fvars φ = {} ⟹ φL φ ∈ fmla"
and
Fvars_φL[simp]: "φ ∈ fmla ⟹ Fvars φ = {} ⟹ Fvars (φL φ) = {}"
  unfolding φL_def PP_def by auto

lemma bprv_φL_eqv:
"φ ∈ fmla ⟹ Fvars φ  = {} ⟹ bprv (eqv (φL φ) (imp (PP ⟨φL φ⟩) φ))"
  unfolding φL_def PP_def using bprv_diag_eqv[of "imp P φ"] by auto

lemma prv_φL_eqv:
"φ ∈ fmla ⟹ Fvars φ  = {} ⟹ prv (eqv (φL φ) (imp (PP ⟨φL φ⟩) φ))"
  using bprv_prv[OF _ _ bprv_φL_eqv, simplified] by auto

end ― ‹context @{locale Loeb_Form}›

(*<*)
end
(*>*)