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
reported in our CADE 2019 paper~\<^cite>‹"DBLP:conf/cade/0001T19"›.
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
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 "⟨φ⟩"]
by (simp add: φ ψ_def)
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›
text ‹This variant (also discussed in our CADE 2019 paper~\<^cite>‹"DBLP:conf/cade/0001T19"›) strengthens
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)
have 41: "prv (imp (cnj (PP ⟨φ⟩) (PP ⟨neg φ⟩)) (PP ⟨cnj φ (neg φ)⟩))"
using HBL4[of φ "neg φ"] by auto
have "prv (imp (cnj φ (neg φ)) (fls))"
by (simp add: prv_cnj_imp_monoR2 prv_imp_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
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))"
by (simp add: prv_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
end