# Theory Abstract_First_Goedel_Rosser

```chapter ‹Abstract Formulations of Gödel-Rosser's First Incompleteness Theorem›

(*<*)
theory Abstract_First_Goedel_Rosser
imports Rosser_Formula Standard_Model_More
begin
(*>*)

text ‹The development here is very similar to that of Gödel First Incompleteness Theorem.
It lacks classical logical variants, since for them Rosser's trick does bring
any extra value.›

section ‹Proof-Theoretic Versions›

context Rosser_Form_Proofs
begin

lemma NN_neg_unique_xx':
assumes [simp]:"φ ∈ fmla" "Fvars φ = {}"
shows
"bprv (imp (NN ⟨φ⟩ (Var xx'))
(eql ⟨neg φ⟩ (Var xx')))"
using B.prv_subst[of yy _ "Var xx'", OF _ _ _ NN_neg_unique[OF assms]] by fastforce

lemma NN_imp_xx':
assumes [simp]: "φ ∈ fmla" "Fvars φ = {}" "χ ∈ fmla"
shows "bprv (imp (subst χ ⟨neg φ⟩ xx')
(all xx' (imp (NN ⟨φ⟩ (Var xx')) χ)))"
proof-
have 2: "bprv (imp (eql ⟨neg φ⟩ (Var xx')) (imp (subst χ ⟨neg φ⟩ xx') χ))"
using B.prv_eql_subst_trm[of xx' χ "⟨neg φ⟩" "Var xx'", simplified] .
have 1: "bprv (imp (subst χ ⟨neg φ⟩ xx') (imp (eql ⟨neg φ⟩ (Var xx')) χ))"
by (simp add: "2" B.prv_imp_com)
have 0: "bprv (imp (subst χ ⟨neg φ⟩ xx') (imp (NN ⟨φ⟩ (Var xx')) χ))"
using 1
by (elim B.prv_prv_imp_trans[rotated 3])
(auto simp add: B.prv_imp_com B.prv_imp_monoR NN_neg_unique_xx')
show ?thesis by (rule B.prv_all_imp_gen) (auto simp: 0)
qed

lemma goedel_rosser_first_theEasyHalf:
assumes c: "consistent"
shows "¬ prv φR"
proof
assume 0: "prv φR"
then obtain "prf" where [simp]: "prf ∈ proof" and "prfOf prf φR" using prv_prfOf by auto
hence 00: "bprv (PPf (encPf prf) ⟨φR⟩)" using prfOf_PPf by auto
from dwf_dwfd.d_dwf.bprv_prv'[OF _ 00, simplified] have b00: "prv (PPf (encPf prf) ⟨φR⟩)" .
have "¬ prv (neg φR)" using 0 c unfolding consistent_def3 by auto
hence "∀ prf ∈ proof.  ¬ prfOf prf (neg φR)" using 00 prv_prfOf by auto
hence "bprv (neg (PPf p ⟨neg φR⟩))" if "p ∈ num" for p using not_prfOf_PPf Clean_PPf_encPf that
by (cases "p ∈ encPf ` proof") auto
hence 1: "prv (all zz (imp (LLq (Var zz) (encPf prf)) (neg (PPf (Var zz) ⟨neg φR⟩))))"
(* here use locale assumption about the order-like relation: *)
by (intro LLq_num) auto
have 11: "prv (RR (encPf prf) ⟨φR⟩)"
using NN_imp_xx'[of φR "neg (PPf (Var zz) (Var xx'))", simplified]
by (auto simp add: RR_def2 R_def
intro!: prv_all_congW[OF _ _ _ _ 1] prv_imp_monoL[OF _ _ _ dwf_dwfd.d_dwf.bprv_prv'])
have 3: "prv (cnj (PPf (encPf prf) ⟨φR⟩) (RR (encPf prf) ⟨φR⟩))"
by (rule prv_cnjI[OF _ _ b00 11]) auto
have "prv ((PP' ⟨φR⟩))" unfolding PP'_def P'_def
using 3 by (auto intro: prv_exiI[of _ _ "encPf prf"])
moreover have "prv (neg (PP' ⟨φR⟩))"
using prv_eqv_prv[OF _ _ 0 prv_φR_eqv] by auto
ultimately show False using c unfolding consistent_def3 by auto
qed

lemma goedel_rosser_first_theHardHalf:
assumes c: "consistent"
shows "¬ prv (neg φR)"
proof
assume 0: "prv (neg φR)"
then obtain "prf" where [simp,intro!]: "prf ∈ proof" and pr: "prfOf prf (neg φR)" using prv_prfOf by auto
define p where p: "p = encPf prf"
have [simp,intro!]: "p ∈ num" unfolding p by auto
have 11: "bprv (PPf p ⟨neg φR⟩)" using pr prfOf_PPf unfolding p by auto
have 1: "bprv (NN ⟨φR⟩ ⟨neg φR⟩)" using NN_neg by simp

have "¬ prv φR" using 0 c unfolding consistent_def3 by auto
from not_prv_prv_neg_PPf[OF _ _ this]
have b2: "∀ r ∈ num. bprv (neg (PPf r ⟨φR⟩))" by auto
hence 2: "∀ r ∈ num. prv (neg (PPf r ⟨φR⟩))"
by (auto intro: dwf_dwfd.d_dwf.bprv_prv')

obtain P where P[simp,intro!]: "P ⊆num" "finite P"
and 3: "prv (dsj (sdsj {eql (Var yy) r |r. r ∈ P}) (LLq p (Var yy)))"
(* here use the other locale assumption about the order-like relation: *)
using LLq_num2 by auto

have "prv (imp (cnj (PPf (Var yy) ⟨φR⟩) (RR (Var yy) ⟨φR⟩)) fls)"
proof(rule prv_dsj_cases[OF _ _ _ 3])
{fix r assume r: "r ∈ P" hence rn[simp]: "r ∈ num" using P(1) by blast
have "prv (imp (cnj (PPf r ⟨φR⟩) (RR r ⟨φR⟩)) fls)"
using 2 unfolding neg_def
by (metis FvarsT_num PPf RR rn φR all_not_in_conv cnj enc fls imp in_num prv_imp_cnj3L prv_imp_mp)
hence "prv (imp (eql (Var yy) r)
(imp (cnj (PPf (Var yy) ⟨φR⟩) (RR (Var yy) ⟨φR⟩)) fls))"
using prv_eql_subst_trm_id[of yy "cnj (PPf (Var yy) ⟨φR⟩) (RR (Var yy) ⟨φR⟩)" r,simplified]
unfolding neg_def[symmetric]
by (intro prv_neg_imp_imp_trans) auto
}
thus "prv (imp (sdsj {eql (Var yy) r |r. r ∈ P})
(imp (cnj (PPf (Var yy) ⟨φR⟩) (RR (Var yy) ⟨φR⟩)) fls))"
using Var P(1) eql by (intro prv_sdsj_imp) (auto 0 0 simp: set_rev_mp)
next
let ?φ = "all xx' (imp (NN ⟨φR⟩ (Var xx')) (neg (PPf p (Var xx'))))"
have "bprv (neg ?φ)"
using 1 11 by (intro B.prv_imp_neg_allWI[where t = "⟨neg φR⟩"]) (auto intro: B.prv_prv_neg_imp_neg)
hence "prv (neg ?φ)" by (auto intro: dwf_dwfd.d_dwf.bprv_prv')
hence 00: "prv (imp (LLq p (Var yy))
(imp (imp (LLq p (Var yy)) ?φ) fls))"
unfolding neg_def[symmetric] by (intro prv_imp_neg_imp_neg_imp) auto
have "prv (imp (LLq p (Var yy))
(imp (RR (Var yy) ⟨φR⟩) fls))"
unfolding neg_def[symmetric] using 00[folded neg_def]
by (auto simp add: RR_def2 R_def intro!: prv_imp_neg_allI[where t = p])
thus "prv (imp (LLq p (Var yy))
(imp (cnj (PPf (Var yy) ⟨φR⟩) (RR (Var yy) ⟨φR⟩)) fls))"
unfolding neg_def[symmetric] by (intro prv_imp_neg_imp_cnjR) auto
qed(auto, insert Var P(1) eql, simp_all add: set_rev_mp)
hence "prv (neg (exi yy (cnj (PPf (Var yy) ⟨φR⟩) (RR (Var yy) ⟨φR⟩))))"
unfolding neg_def[symmetric] by (intro prv_neg_neg_exi) auto
hence "prv (neg (PP' ⟨φR⟩))" unfolding PP'_def P'_def by simp
hence "prv φR" using prv_φR_eqv by (meson PP' φR enc in_num neg prv_eqv_prv_rev)
with ‹¬ prv φR› show False using c unfolding consistent_def3 by auto
qed

theorem goedel_rosser_first:
assumes "consistent"
shows "¬ prv φR ∧ ¬ prv (neg φR)"
using assms goedel_rosser_first_theEasyHalf goedel_rosser_first_theHardHalf by blast

theorem goedel_rosser_first_ex:
assumes "consistent"
shows "∃ φ. φ ∈ fmla ∧ ¬ prv φ ∧ ¬ prv (neg φ)"
using assms goedel_rosser_first by (intro exI[of _ φR]) blast

end ― ‹context @{locale Rosser_Form}›

section ‹Model-Theoretic Versions›

subsection ‹First model-theoretic version›

locale Rosser_Form_Proofs_Minimal_Truth =
Rosser_Form_Proofs
var trm fmla Var FvarsT substT Fvars subst
num
eql cnj imp all exi
fls
prv bprv
Lq
dsj
"proof" prfOf
enc
N S
encPf
Pf
+
Minimal_Truth_Soundness
var trm fmla Var FvarsT substT Fvars subst
eql cnj imp all exi
fls
dsj
num
bprv
isTrue
for
var :: "'var set" and trm :: "'trm set" and fmla :: "'fmla set"
and Var FvarsT substT Fvars subst
and eql cnj imp all exi
and fls
and dsj
and num
and Lq
and prv bprv
and enc ("⟨_⟩")
and N S P
and "proof" :: "'proof set" and prfOf encPf
and Pf
and isTrue
begin

lemma Fvars_PP'[simp]: "Fvars (PP' ⟨φR⟩) = {}" unfolding PP'_def
by (subst Fvars_subst) auto

lemma Fvars_RR'[simp]: "Fvars (RR (Var yy) ⟨φR⟩) = {yy}"
unfolding RR_def
by (subst Fvars_psubst) (fastforce intro!: exI[of _ "{yy}"])+

lemma isTrue_PPf_implies_φR:
assumes "isTrue (all yy (neg (PPf (Var yy) ⟨φR⟩)))"
(is "isTrue ?H")
shows "isTrue φR"
proof-
define F where "F ≡ RR (Var yy) ⟨φR⟩"
have [simp]: "F ∈ fmla" "Fvars F = {yy}"
unfolding F_def by auto
have [simp]: "exi yy (PPf (Var yy) ⟨φR⟩) ∈ fmla"
unfolding PPf_def by auto

have 1: "bprv
(imp (all yy (neg (PPf (Var yy) ⟨φR⟩)))
(neg (exi yy (PPf (Var yy) ⟨φR⟩))))"
(is "bprv (imp (all yy (neg ?G)) (neg (exi yy ?G)))")
using B.prv_all_neg_imp_neg_exi[of yy ?G] by auto
have 2: "bprv (imp (neg (exi yy ?G)) (neg (exi yy (cnj ?G F))))"
by (auto intro!: B.prv_imp_neg_rev B.prv_exi_cong B.prv_imp_cnjL)
have "bprv (imp (all yy (neg ?G)) (neg (exi yy (cnj ?G F))))"
using B.prv_prv_imp_trans[OF _ _ _  1 2] by simp
hence "bprv (imp ?H (neg (PP' ⟨φR⟩)))"
unfolding PP'_def P'_def
by (simp add: F_def)
from B.prv_prv_imp_trans[OF _ _ _  this bprv_imp_φR]
have "bprv (imp ?H φR)" by auto
from prv_imp_implies_isTrue[OF _ _ _ _ this assms, simplified]
show ?thesis .
qed

theorem isTrue_φR:
assumes "consistent"
shows "isTrue φR"
proof-
have "∀ n ∈ num. bprv (neg (PPf n ⟨φR⟩))"
using not_prv_prv_neg_PPf[OF _ _ goedel_rosser_first_theEasyHalf[OF assms]]
by auto
hence "∀ n ∈ num. isTrue (neg (PPf n ⟨φR⟩))" by (auto intro: sound_isTrue)
hence "isTrue (all yy (neg (PPf (Var yy) ⟨φR⟩)))" by (auto intro: isTrue_all)
thus ?thesis using isTrue_PPf_implies_φR by auto
qed

theorem goedel_rosser_first_strong: "consistent ⟹ ¬ prv φR ∧ ¬ prv (neg φR) ∧ isTrue φR"
using isTrue_φR goedel_rosser_first by blast

theorem goedel_rosser_first_strong_ex:
"consistent ⟹ ∃ φ. φ ∈ fmla ∧ ¬ prv φ ∧ ¬ prv (neg φ) ∧ isTrue φ"
using goedel_rosser_first_strong by (intro exI[of _ φR]) blast

end ― ‹context @{locale Rosser_Form_Proofs_Minimal_Truth}›

subsection ‹Second model-theoretic version›

context Rosser_Form
begin
print_context
end

locale Rosser_Form_Minimal_Truth_Soundness_HBL1iff_Compl_Pf =
Rosser_Form
var trm fmla Var
FvarsT substT Fvars subst
num
eql cnj imp all exi
fls
prv bprv
Lq
dsj
enc
N
S
P
+
Minimal_Truth_Soundness_HBL1iff_Compl_Pf
var trm fmla Var FvarsT substT Fvars subst
eql cnj imp all exi
fls
dsj
num
enc
prv bprv
P
isTrue
Pf
for
var :: "'var set" and trm :: "'trm set" and fmla :: "'fmla set"
and Var FvarsT substT Fvars subst
and eql cnj imp all exi
and fls
and dsj
and num
and prv bprv
and Lq
and enc ("⟨_⟩")
and N S
and isTrue
and P Pf

locale Rosser_Form_Minimal_Truth_Soundness_HBL1iff_Compl_Pf_Compl_NegPf =
Rosser_Form_Minimal_Truth_Soundness_HBL1iff_Compl_Pf
var trm fmla Var FvarsT substT Fvars subst
eql cnj imp all exi
fls
dsj
num
prv bprv
Lq
enc
N S
isTrue
P
Pf
+
M : Minimal_Truth_Soundness_HBL1iff_Compl_Pf_Compl_NegPf
var trm fmla Var FvarsT substT Fvars subst
eql cnj imp all exi
fls
dsj
num
enc
prv bprv
N
isTrue
Pf
for
var :: "'var set" and trm :: "'trm set" and fmla :: "'fmla set"
and Var FvarsT substT Fvars subst
and eql cnj imp all exi
and fls
and dsj
and num
and prv bprv
and Lq
and enc ("⟨_⟩")
and N S P
and isTrue
and Pf

sublocale
Rosser_Form_Minimal_Truth_Soundness_HBL1iff_Compl_Pf_Compl_NegPf <
recover_proofs: Rosser_Form_Proofs_Minimal_Truth
where prfOf = prfOf and "proof" = "proof" and encPf = encPf
and prv = prv and bprv = bprv
by standard

context Rosser_Form_Minimal_Truth_Soundness_HBL1iff_Compl_Pf_Compl_NegPf
begin
thm recover_proofs.goedel_rosser_first_strong
end

(*<*)
end
(*>*)

```