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 ― ‹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 "φ"]
  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)

  ― ‹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))"
    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
  ― ‹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))"
    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 ― ‹context @{locale Jeroslow_Godel_Second}

(*<*)
end
(*>*)