# 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"

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