Theory Jeroslow_Simplified

```section ‹A Simplification of Jeroslow's Original Argument›

(*<*)
theory Jeroslow_Simplified imports Abstract_Jeroslow_Encoding
begin
(*>*)

text ‹This is the simplified version of Jeroslow's Second Incompleteness Theorem
The simplification consists of replacing pseudo-terms with plain terms
and representability with (what we call in the paper) term-representability.
This simplified version does not incur the complications of the original.›

subsection ‹Jeroslow-style term-based diagonalization›

locale Jeroslow_Diagonalization =
Deduct_with_False
var trm fmla Var FvarsT substT Fvars subst
eql cnj imp all exi
fls
num
prv
+
Encode
var trm fmla Var FvarsT substT Fvars subst
num
enc
+
TermEncode
var trm fmla Var FvarsT substT Fvars subst
num
Ops tenc
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 num
and prv
and enc ("⟨_⟩")
and Ops and tenc
+
fixes F :: "('trm ⇒ 'trm) set"
and encF :: "('trm ⇒ 'trm) ⇒ ('trm ⇒ 'trm)"
and N :: "'trm ⇒ 'trm"
and ssap :: "'fmla ⇒ 'trm ⇒ 'trm"
assumes
F[simp,intro!]: "⋀ f n. f ∈ F ⟹ n ∈ num ⟹ f n ∈ num"
and
encF[simp,intro!]: "⋀ f. f ∈ F ⟹ encF f ∈ Ops"
and
N[simp,intro!]: "N ∈ F"
and
ssap[simp]: "⋀φ. φ ∈ fmla ⟹ Fvars φ = {xx} ⟹ ssap φ ∈ F"
and
ReprF: "⋀f n. f ∈ F ⟹ n ∈ num ⟹ prv (eql (encF f n) (f n))"
and
CapN: "⋀φ. φ ∈ fmla ⟹ Fvars φ = {} ⟹ N ⟨φ⟩ = ⟨neg φ⟩"
and
CapSS:
"⋀ ψ f. ψ ∈ fmla ⟹ Fvars ψ = {xx} ⟹ f ∈ F ⟹
ssap ψ (tenc (encF f)) = ⟨inst ψ (encF f (tenc (encF f)))⟩"
begin

definition tJ :: "'fmla ⇒ 'trm" where
"tJ ψ ≡ encF (ssap ψ) (tenc (encF (ssap ψ)))"

definition φJ :: "'fmla ⇒ 'fmla" where
"φJ ψ ≡ subst ψ (tJ ψ) xx"

lemma tJ[simp]:
assumes "ψ ∈ fmla" and "Fvars ψ = {xx}"
shows "tJ ψ ∈ trm"
using assms tJ_def by auto

lemma FvarsT_tJ[simp]:
assumes "ψ ∈ fmla" and "Fvars ψ = {xx}"
shows "FvarsT (tJ ψ) = {}"
using assms tJ_def by auto

lemma φJ[simp]:
assumes "ψ ∈ fmla" and "Fvars ψ = {xx}"
shows "φJ ψ ∈ fmla"
using assms φJ_def by auto

lemma Fvars_φJ[simp]:
assumes "ψ ∈ fmla" and "Fvars ψ = {xx}"
shows "Fvars (φJ ψ) = {}"
using assms φJ_def by auto

lemma diagonalization:
assumes "ψ ∈ fmla" and "Fvars ψ = {xx}"
shows "prv (eql (tJ ψ) ⟨inst ψ (tJ ψ)⟩) ∧
prv (eqv (φJ ψ) (inst ψ ⟨φJ ψ⟩))"
proof
define fJ where "fJ ≡ ssap ψ"
have fJ[simp]: "fJ ∈ F" unfolding fJ_def using assms by auto
have "fJ (tenc (encF fJ)) = ⟨inst ψ (tJ ψ)⟩"
by (simp add: CapSS assms fJ_def tJ_def)
thus **: "prv (eql (tJ ψ) ⟨inst ψ (tJ ψ)⟩)"
using ReprF fJ fJ_def tJ_def by fastforce
show "prv (eqv (φJ ψ) (inst ψ ⟨φJ ψ⟩))"
using assms prv_eql_subst_trm_eqv[OF xx _  _ _ **, of "ψ"]
by (auto simp: φJ_def inst_def)
qed

end ― ‹context @{locale Jeroslow_Diagonalization}›

subsection ‹Term-based version of Jeroslow's Second Incompleteness Theorem›

locale Jeroslow_Godel_Second =
Jeroslow_Diagonalization
var trm fmla Var FvarsT substT Fvars subst
eql cnj imp all exi
fls
num
prv
enc
Ops tenc
F encF N ssap
+
HBL1
var trm fmla Var FvarsT substT Fvars subst
num
eql cnj imp all exi
prv prv
enc
P
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 num
and prv
and enc ("⟨_⟩")
and Ops and tenc
and P
and F encF N ssap
+
assumes
SHBL3: "⋀t. t ∈ trm ⟹ FvarsT t = {} ⟹ prv (imp (PP t) (PP ⟨PP t⟩))"
begin

text ‹Consistency formula a la Jeroslow:›
definition jcons :: "'fmla" where
"jcons ≡ all xx (neg (cnj (PP (Var xx)) (PP (encF N (Var (xx))))))"

lemma prv_eql_subst_trm3:
"x ∈ var ⟹ φ ∈ fmla ⟹ t1 ∈ trm ⟹ t2 ∈ trm ⟹
prv (eql t1 t2) ⟹ prv (subst φ t1 x) ⟹ prv (subst φ t2 x)"
using prv_eql_subst_trm2
by (meson subst prv_imp_mp)

lemma prv_eql_neg_encF_N:
assumes "φ ∈ fmla" and "Fvars φ = {}"
shows "prv (eql ⟨neg φ⟩ (encF N ⟨φ⟩))"
unfolding CapN[symmetric, OF assms]
by (rule prv_prv_eql_sym) (auto simp: assms intro: ReprF)

lemma prv_imp_neg_encF_N_aux:
assumes "φ ∈ fmla" and "Fvars φ = {}"
shows "prv (imp (PP ⟨neg φ⟩) (PP (encF N ⟨φ⟩)))"
using assms prv_eql_subst_trm2[OF _ _ _ _ prv_eql_neg_encF_N[OF assms],
of xx "PP (Var xx)"]
unfolding PP_def by auto

lemma prv_cnj_neg_encF_N_aux:
assumes "φ ∈ fmla" and "Fvars φ = {}" "χ ∈ fmla" "Fvars χ = {}"
and "prv (neg (cnj χ (PP ⟨neg φ⟩)))"
shows"prv (neg (cnj χ (PP (encF N ⟨φ⟩))))"
using assms prv_eql_subst_trm3[OF _ _ _ _ prv_eql_neg_encF_N,
of xx "neg (cnj χ (PP (Var xx)))"]
unfolding PP_def by auto

theorem jeroslow_godel_second:
assumes consistent
shows "¬ prv jcons"
proof
assume *: "prv jcons"
define ψ where "ψ ≡ PP (encF N (Var xx))"
define t where "t ≡ tJ ψ"
have ψ[simp,intro]: "ψ ∈ fmla" "Fvars ψ = {xx}"
and t[simp,intro]: "t ∈ trm" "FvarsT t = {}"
unfolding ψ_def t_def by auto

have sPP[simp]: "subst (PP (encF N (Var xx))) ⟨PP (encF N t)⟩ xx =
PP (encF N ⟨PP (encF N t)⟩)"
unfolding PP_def by (subst subst_compose_eq_or) auto
have sPP2[simp]: "subst (PP (encF N (Var xx))) t xx = PP (encF N t)"
unfolding PP_def by (subst subst_compose_eq_or) auto
have 00: "PP (encF N t) = inst ψ t" unfolding ψ_def inst_def PP_def
by (subst subst_compose_eq_or) auto

define φ where "φ ≡ φJ ψ"
have [simp]: "φ ∈ fmla" "Fvars φ = {}" unfolding φ_def by auto
have **: "prv (eql t ⟨φ⟩)"
unfolding 00 φ_def
using φJ_def diagonalization inst_def t_def by auto
have φ: "φ = PP (encF N t)" unfolding φ_def φJ_def t_def ψ_def
using sPP2 ψ_def t_def by blast
have 1: "prv (imp φ (PP ⟨φ⟩))" using SHBL3[of "encF N t"]
using 00 φJ_def φ_def ψ_def inst_def t_def by auto
have eqv_φ: "prv (eqv φ (PP (encF N ⟨φ⟩)))"  using diagonalization
by (metis "00" sPP φJ_def φ_def ψ ψ_def diagonalization inst_def t_def)
have 2: "prv (imp φ (PP (encF N ⟨φ⟩)))"
using prv_cnjEL[OF _ _ eqv_φ[unfolded eqv_def]] by auto
have "prv (imp (PP (encF N ⟨φ⟩)) φ)"
using prv_cnjER[OF _ _ eqv_φ[unfolded eqv_def]] by auto
from  prv_prv_imp_trans[OF _ _ _ prv_imp_neg_encF_N_aux this]
have 22: "prv (imp (PP ⟨neg φ⟩) φ)" by auto
have 3: "prv (imp φ (cnj (PP ⟨φ⟩) (PP (encF N ⟨φ⟩))))"
by (rule prv_imp_cnj[OF _ _ _ 1 2]) (auto simp: φ_def)
have 4: "prv (neg (cnj (PP ⟨φ⟩) (PP (encF N ⟨φ⟩))))"
using prv_allE[OF _ _ _ *[unfolded jcons_def], of "⟨φ⟩"]
have 5: "prv (neg φ)"
unfolding neg_def
by (rule prv_prv_imp_trans[OF _ _ _ 3 4[unfolded neg_def]]) auto
hence "prv (PP ⟨neg φ⟩)" using
HBL1_PP[OF _ _ 5] by auto
hence "prv φ" using prv_imp_mp[OF _ _ 22] by auto
with 5 assms show False unfolding consistent_def3 by auto
qed

subsection ‹A variant of the Second Incompleteness Theorem›

the conclusion of the theorem to the standard formulation
of "does not prove its own consistency" at the expense of two
additional derivability-like conditions, HBL4 and WHBL2.›

theorem jeroslow_godel_second_standardCon:
assumes consistent
and HBL4: "⋀φ1 φ2. {φ1,φ2} ⊆ fmla ⟹ Fvars φ1 = {} ⟹ Fvars φ2 = {} ⟹
prv (imp (cnj (PP ⟨φ1⟩) (PP ⟨φ2⟩)) (PP ⟨cnj φ1 φ2⟩))"
and WHBL2: "⋀φ1 φ2. {φ1,φ2} ⊆ fmla ⟹ Fvars φ1 = {} ⟹ Fvars φ2 = {} ⟹
prv (imp φ1 φ2) ⟹ prv (imp (PP ⟨φ1⟩) (PP ⟨φ2⟩))"
shows "¬ prv (neg (PP ⟨fls⟩))"
proof
assume *:  "prv (neg (PP ⟨fls⟩))"
define ψ where "ψ ≡ PP (encF N (Var xx))"
define t where "t ≡ tJ ψ"
have ψ[simp,intro]: "ψ ∈ fmla" "Fvars ψ = {xx}"
and t[simp,intro]: "t ∈ trm" "FvarsT t = {}"
unfolding ψ_def t_def by auto

have [simp]: "subst (PP (encF N (Var xx))) ⟨PP (encF N t)⟩ xx =
PP (encF N ⟨PP (encF N t)⟩)"
unfolding PP_def by (subst subst_compose_eq_or) auto
have [simp]: "subst (PP (encF N (Var xx))) t xx = PP (encF N t)"
unfolding PP_def by (subst subst_compose_eq_or) auto
have 00: "PP (encF N t) = inst ψ t" unfolding ψ_def inst_def PP_def
by (subst subst_compose_eq_or) auto

define φ where "φ = PP (encF N t)"
have [simp]: "φ ∈ fmla" "Fvars φ = {}" unfolding φ_def by auto
have **: "prv (eql t ⟨PP (encF N t)⟩)"
unfolding 00 by (simp add: diagonalization t_def)
have 1: "prv (imp φ (PP ⟨φ⟩))" using SHBL3[of "encF N t"]
by (auto simp: φ_def)
have 2: "prv (imp φ (PP (encF N ⟨φ⟩)))"
using prv_eql_subst_trm2[OF xx _  _ _ **, of "PP (encF N (Var xx))"]
by (auto simp: φ_def)
have "prv (imp (PP (encF N ⟨φ⟩)) φ)"
using prv_eql_subst_trm_rev2[OF xx _  _ _ **, of "PP (encF N (Var xx))"]
by (auto simp: φ_def)
from prv_prv_imp_trans[OF _ _ _ prv_imp_neg_encF_N_aux this]
have 22: "prv (imp (PP ⟨neg φ⟩) φ)" by auto
have 3: "prv (imp φ (cnj (PP ⟨φ⟩) (PP (encF N ⟨φ⟩))))"
by (rule prv_imp_cnj[OF _ _ _ 1 2]) (auto simp: φ_def)

― ‹This is the modification from the proof of @{thm jeroslow_godel_second}:›
have 41: "prv (imp (cnj (PP ⟨φ⟩) (PP ⟨neg φ⟩)) (PP ⟨cnj φ (neg φ)⟩))"
using HBL4[of φ "neg φ"] by auto
have "prv (imp (cnj φ (neg φ)) (fls))"
from WHBL2[OF _ _ _ this]
have 42: "prv (imp (PP ⟨cnj φ (neg φ)⟩) (PP ⟨fls⟩))" by auto
from prv_prv_imp_trans[OF _ _ _ 41 42]
have "prv (imp (cnj (PP ⟨φ⟩) (PP ⟨neg φ⟩)) (PP ⟨fls⟩))" by auto
from prv_prv_imp_trans[OF _ _ _ this *[unfolded neg_def]]
have "prv (neg (cnj (PP ⟨φ⟩) (PP ⟨neg φ⟩)))"
unfolding neg_def by auto
from prv_cnj_neg_encF_N_aux[OF _ _ _ _ this]
have 4: "prv (neg (cnj (PP ⟨φ⟩) (PP (encF N ⟨φ⟩))))" by auto
― ‹End modification›

have 5: "prv (neg φ)"
unfolding neg_def
by (rule prv_prv_imp_trans[OF _ _ _ 3 4[unfolded neg_def]]) auto
hence "prv (PP ⟨neg φ⟩)" using HBL1_PP[OF _ _ 5] by auto
hence "prv φ" using prv_imp_mp[OF _ _ 22] by auto
with 5 assms show False unfolding consistent_def3 by auto
qed

text ‹Next we perform a formal analysis of some connection between the
above theorems' hypotheses.›

definition noContr :: bool where
"noContr ≡ ∀ φ ∈ fmla. Fvars φ = {} ⟶ prv (neg (cnj (PP ⟨φ⟩) (PP ⟨neg φ⟩)))"

lemma jcons_noContr:
assumes j: "prv jcons"
shows "noContr"
unfolding noContr_def proof safe
fix φ assume φ[simp]: "φ ∈ fmla" "Fvars φ = {}"
have [simp]: "subst (PP (encF N (Var xx))) ⟨φ⟩ xx =
PP (encF N ⟨φ⟩)"
unfolding PP_def by (simp add: subst_compose_same)
note j = allE_id[OF _ _ j[unfolded jcons_def], simplified]
have 0: "prv (neg (cnj (PP ⟨φ⟩)
(PP (encF N ⟨φ⟩))))"
(is "prv (neg (cnj (PP ⟨φ⟩) ?j))")
using prv_subst[OF _ _ _ j, of xx "⟨φ⟩"] by simp
have 1: "prv (imp (PP ⟨neg φ⟩) ?j)"
using prv_eql_neg_encF_N[of φ, simplified]
using prv_imp_neg_encF_N_aux by auto
have 2: "prv (imp (cnj (PP ⟨φ⟩) (PP ⟨neg φ⟩))
(cnj (PP ⟨φ⟩) ?j))"
using 0 1 by (simp add:  prv_cnj_mono prv_imp_refl)

have "prv (imp (cnj (PP ⟨φ⟩) (PP ⟨neg φ⟩))
(cnj (PP ⟨φ⟩) ?j))"
by (simp add: 2 prv_cnj_mono prv_imp_refl)
thus "prv (neg (cnj (PP ⟨φ⟩) (PP ⟨neg φ⟩)))" using 0
unfolding neg_def
by (elim prv_prv_imp_trans[rotated 3]) auto
qed

text ‹@{term noContr} is still stronger than the standard notion of proving own consistency:›

lemma noContr_implies_neg_PP_fls:
assumes "noContr"
shows "prv (neg (PP ⟨fls⟩))"
proof-
have "prv (neg (cnj (PP ⟨fls⟩) (PP ⟨neg fls⟩)))"
using assms unfolding noContr_def by auto
thus ?thesis
using Fvars_tru enc in_num tru_def PP PP_def fls imp HBL1 neg_def
prv_cnj_imp prv_fls prv_imp_com prv_imp_mp
by (metis Encode.enc HBL1_axioms HBL1_def)
qed

corollary jcons_implies_neg_PP_fls:
assumes "prv jcons"
shows "prv (neg (PP ⟨fls⟩))"
by (simp add: assms noContr_implies_neg_PP_fls jcons_noContr)

text ‹However, unlike @{term jcons}, which seems to be quite a bit stronger,
@{term noContr} is equivalent to the standard notion under a slightly
stronger assumption than our WWHBL2, namely, a binary version of that:›

lemma neg_PP_fls_implies_noContr:
assumes WWHBL22:
"⋀φ χ ψ. φ ∈ fmla ⟹ χ ∈ fmla ⟹ ψ ∈ fmla ⟹
Fvars φ = {} ⟹ Fvars χ = {} ⟹ Fvars ψ = {} ⟹
prv (imp φ (imp χ ψ)) ⟹ prv (imp (PP ⟨φ⟩) (imp (PP ⟨χ⟩) (PP ⟨ψ⟩)))"
assumes p: "prv (neg (PP ⟨fls⟩))"
shows "noContr"
unfolding noContr_def proof safe
fix φ assume φ[simp]: "φ ∈ fmla" "Fvars φ = {}"
have 0: "prv (imp φ (imp (neg φ) fls))"
have 1: "prv (imp (PP ⟨φ⟩) (imp (PP ⟨neg φ⟩) (PP ⟨fls⟩)))"
using WWHBL22[OF _ _ _ _ _ _ 0] by auto
show "prv (neg (cnj (PP ⟨φ⟩) (PP ⟨neg φ⟩)))" using 1 p
unfolding neg_def
by (elim prv_cnj_imp_monoR2[rotated 3, OF prv_prv_imp_trans[rotated 3]])
(auto intro!: prv_imp_monoL)
qed

end ― ‹context @{locale Jeroslow_Godel_Second}›

(*<*)
end
(*>*)
```