Theory Rosser_Formula

chapter ‹Rosser Formulas›

text ‹The Rosser formula is a modification of the Gödel formula that
is undecidable assuming consistency only (not $\omega$-consistency).›

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

locale Rosser_Form =
Deduct2_with_PseudoOrder
  var trm fmla Var FvarsT substT Fvars subst
  eql cnj imp all exi
  fls
  dsj
  num
  prv bprv
  Lq
  +
Repr_Neg
  var trm fmla Var FvarsT substT Fvars subst
  eql cnj imp all exi
  fls
  num
  prv bprv
  enc
  N
  +
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 FvarsT substT Fvars subst
    and num
    and eql cnj imp all exi
    and fls
    and prv bprv
    and Lq
    and dsj
    and enc (‹⟨_⟩›)
    and N S P


locale Rosser_Form_Proofs =
Deduct2_with_PseudoOrder
  var trm fmla Var FvarsT substT Fvars subst
  eql cnj imp all exi
  fls
  dsj
  num
  prv bprv
  Lq
  +
Repr_Neg
  var trm fmla Var FvarsT substT Fvars subst
  eql cnj imp all exi
  fls
  num
  prv bprv
  enc
  N
  +
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
    and num
    and eql cnj imp all exi
    and fls
    and prv bprv
    and Lq
    and dsj and "proof" :: "'proof set" and prfOf
    and enc (‹⟨_⟩›)
    and N
    and S
    and encPf Pf

context Rosser_Form_Proofs
begin

definition R where "R = all zz (imp (LLq (Var zz) (Var yy))
                                     (all xx' (imp (NN (Var xx) (Var xx'))
                                                   (neg (PPf (Var zz) (Var xx'))))))"

definition RR where "RR t1 t2 = psubst R [(t1,yy), (t2,xx)]"

lemma R[simp,intro!]: "R ∈ fmla" unfolding R_def by auto

lemma RR_def2:
  "t1 ∈ trm ⟹ t2 ∈ trm ⟹ xx ∉ FvarsT t1 ⟹ RR t1 t2 = subst (subst R t1 yy) t2 xx"
  unfolding RR_def by (rule psubst_eq_rawpsubst2[simplified]) auto

definition P' where "P' = exi yy (cnj (PPf (Var yy) (Var xx)) (RR (Var yy) (Var xx)))"

definition PP' where "PP' t = subst P' t xx"

lemma Fvars_R[simp]: "Fvars R = {xx,yy}" unfolding R_def by auto

lemma [simp]: "Fvars (RR (Var yy) (Var xx)) = {yy,xx}" by (auto simp: RR_def2)

lemma P'[simp,intro!]: "P' ∈ fmla" unfolding P'_def by (auto simp: PPf_def2 RR_def2)

lemma Fvars_P'[simp]: "Fvars P' = {xx}" unfolding P'_def by (auto simp: PPf_def2 RR_def2)

lemma PP'[simp,intro!]: "t ∈ trm ⟹ PP' t ∈ fmla"
  unfolding PP'_def by auto

lemma RR[simp,intro]: "t1 ∈ trm ⟹ t2 ∈ trm ⟹ RR t1 t2 ∈ fmla"
  by (auto simp: RR_def)

lemma RR_simps[simp]:
   "n ∈ num ⟹ subst (RR (Var yy) (Var xx)) n xx = RR (Var yy) n"
   "m ∈ num ⟹ n ∈ num ⟹ subst (RR (Var yy) m) n yy = RR n m"
  by (simp add: RR_def2 subst2_fresh_switch)+


text ‹The Rosser modification of the Gödel formula›
definition φR :: 'fmla where "φR ≡ diag (neg P')"

lemma φR[simp,intro!]: "φR ∈ fmla" and Fvars_φR[simp]: "Fvars φR = {}"
  unfolding φR_def wrepr.PP_def by auto

lemma bprv_φR_eqv:
  "bprv (eqv φR (neg (PP' ⟨φR⟩)))"
  unfolding φR_def PP'_def using bprv_diag_eqv[of "neg P'"] by simp

lemma bprv_imp_φR:
  "bprv (imp (neg (PP' ⟨φR⟩)) φR)"
  by (rule B.prv_imp_eqvER) (auto intro: bprv_φR_eqv)

lemma prv_φR_eqv:
  "prv (eqv φR (neg (PP' ⟨φR⟩)))"
  using dwf_dwfd.d_dwf.bprv_prv'[OF _ bprv_φR_eqv, simplified] .

lemma prv_imp_φR:
  "prv (imp (neg (PP' ⟨φR⟩)) φR)"
  by (rule prv_imp_eqvER) (auto intro: prv_φR_eqv)

end ― ‹context @{locale Rosser_Form}›


sublocale Rosser_Form_Proofs < Rosser_Form where P = P
  by standard

sublocale Rosser_Form_Proofs < Goedel_Form where P = P
  by standard

(*<*)
end
(*>*)