Theory Jeroslow_Original

section ‹A Formalization of Jeroslow's Original Argument›

(*<*)
theory Jeroslow_Original imports
"Syntax_Independent_Logic.Pseudo_Term"
Abstract_Jeroslow_Encoding
begin
(*>*)

subsection ‹Preliminaries›

text ‹The First Derivability Condition was stated using a formula
with free variable @{term xx}, whereas the pseudo-term theory employs a different variable,
inp. The distinction is of course immaterial, because we can perform
a change of variable in the instantiation:›

context HBL1
begin

text ‹Changing the variable (from @{term xx} to @{term inp}) in the provability predicate:›
definition "Pinp ≡ subst P (Var inp) xx"
lemma PP_Pinp: "t ∈ trm ⟹ PP t = instInp Pinp t"
unfolding PP_def Pinp_def instInp_def by auto

text ‹A version of HBL1 that uses the @{term inp} variable:›
lemma HBL1_inp:
"φ ∈ fmla ⟹ Fvars φ = {} ⟹ prv φ ⟹ prv (instInp Pinp ⟨φ⟩)"
unfolding Pinp_def instInp_def by (auto intro: HBL1)

end ― ‹context @{locale HBL1 }›


subsection ‹Jeroslow-style diagonalization›

locale Jeroslow_Diagonalization =
Deduct_with_False_Disj_Rename
  var trm fmla Var FvarsT substT Fvars subst
  eql cnj imp all exi
  fls
  dsj
  num
  prv
+
Encode
  var trm fmla Var FvarsT substT Fvars subst
  num
  enc
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
and enc ("⟨_⟩")
+
fixes F :: "('trm ⇒ 'trm) set"
  and encF :: "('trm ⇒ 'trm) ⇒ 'fmla"
  and N :: "'trm ⇒ 'trm"
  and ssap :: "'fmla ⇒ 'trm ⇒ 'trm"
assumes
― ‹For the members @{term f} of @{term F}, we will only care about their action on numerals,
and we assume that they send numerals to numerals.›
F[simp,intro!]: "⋀ f n. f ∈ F ⟹ n ∈ num ⟹ f n ∈ num"
and
encF[simp,intro!]: "⋀ f. f ∈ F ⟹ encF f ∈ ptrm (Suc 0)"
and
N[simp,intro!]: "N ∈ F"
and
ssap[simp]: "⋀φ. φ ∈ fmla ⟹ Fvars φ = {inp} ⟹ ssap φ ∈ F"
and
ReprF: "⋀f n. f ∈ F ⟹ n ∈ num ⟹ prveqlPT (instInp (encF f) n) (f n)"
and
CapN: "⋀φ. φ ∈ fmla ⟹ Fvars φ = {} ⟹ N ⟨φ⟩ = ⟨neg φ⟩"
and
CapSS: ― ‹We consider formulas @{term ψ} of one variable, called @{term inp}:›
"⋀ ψ f. ψ ∈ fmla ⟹ Fvars ψ = {inp} ⟹ f ∈ F ⟹
    ssap ψ ⟨encF f⟩ = ⟨instInpP ψ 0 (instInp (encF f) ⟨encF f⟩)⟩"
begin

lemma encF_fmla[simp,intro!]: "⋀ f. f ∈ F ⟹ encF f ∈ fmla"
by auto

lemma enc_trm: "φ ∈ fmla ⟹ ⟨φ⟩ ∈ trm"
by auto

definition τJ :: "'fmla ⇒ 'fmla" where
"τJ ψ ≡ instInp (encF (ssap ψ)) (⟨encF (ssap ψ)⟩)"

definition φJ :: "'fmla ⇒ 'fmla" where
"φJ ψ ≡ instInpP ψ 0 (τJ ψ)"

lemma τJ[simp]:
assumes "ψ ∈ fmla" and "Fvars ψ = {inp}"
shows "τJ ψ ∈ ptrm 0"
unfolding τJ_def apply(rule instInp)
using assms by auto

lemma τJ_fmla[simp]:
assumes "ψ ∈ fmla" and "Fvars ψ = {inp}"
shows "τJ ψ ∈ fmla"
using τJ[OF assms] unfolding ptrm_def by auto

lemma FvarsT_τJ[simp]:
assumes "ψ ∈ fmla" and "Fvars ψ = {inp}"
shows "Fvars (τJ ψ) = {out}"
using τJ[OF assms] unfolding ptrm_def by auto

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

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

lemma diagonalization:
assumes ψ[simp]: "ψ ∈ fmla" and [simp]: "Fvars ψ = {inp}"
shows "prveqlPT (τJ ψ) ⟨instInpP ψ 0 (τJ ψ)⟩ ∧
       prv (eqv (φJ ψ) (instInp ψ ⟨φJ ψ⟩))"
proof
  define f where "f ≡ ssap ψ"
  have f[simp]: "f ∈ F" unfolding f_def using assms by auto
  have ff: "f ⟨encF f⟩ = ⟨instInpP ψ 0 (τJ ψ)⟩"
  using assms unfolding f_def τJ_def by (intro CapSS) auto

  show "prveqlPT (τJ ψ) ⟨instInpP ψ 0 (τJ ψ)⟩"
  using ReprF[OF f, of "⟨encF f⟩"]
  unfolding τJ_def[of ψ, unfolded f_def[symmetric],symmetric] ff[symmetric]
  by auto
  from prveqlPT_prv_instInp_eqv_instInpP[OF ψ, of "τJ ψ", OF _ _ _ _ this,
           unfolded φJ_def[symmetric]]
  show "prv (eqv (φJ ψ) (instInp ψ ⟨φJ ψ⟩))"
  by auto
qed

end ― ‹context @{locale Jeroslow_Diagonalization}›


subsection ‹Jeroslow's Second Incompleteness Theorem›

text ‹We follow Jeroslow's pseudo-term-based development of the
Second Incompleteness Theorem and point out the location in the proof that
implicitly uses an unstated assumption: the fact that, for certain two provably
equivalent formulas @{term φ} and @{term φ'}, it is provable that
the provability of the encoding of @{term φ'} implies
the provability of the encoding of @{term φ}. ›

locale Jeroslow_Godel_Second =
Jeroslow_Diagonalization
  var trm fmla Var FvarsT substT Fvars subst
  eql cnj imp all exi
  fls
  dsj
  num
  prv
  enc
  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 dsj
and num
and prv
and enc ("⟨_⟩")
and P
and F encF N ssap
+
assumes
SHBL3: "⋀τ. τ ∈ ptrm 0 ⟹ prv (imp (instInpP Pinp 0 τ) (instInp Pinp ⟨instInpP Pinp 0 τ⟩))"
begin


text ‹Consistency formula a la Jeroslow:›
definition jcons :: "'fmla" where
"jcons ≡ all xx (neg (cnj (instInp Pinp (Var xx))
                           (instInpP Pinp 0 (instInp (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 Pinp[simp,intro!]: "Pinp ∈ fmla"
and Fvars_Pinp[simp]: "Fvars Pinp = {inp}"
unfolding Pinp_def by auto

lemma ReprF_combineWith_CapN:
assumes "φ ∈ fmla" and "Fvars φ = {}"
shows "prveqlPT (instInp (encF N) ⟨φ⟩) ⟨neg φ⟩"
using assms unfolding CapN[symmetric, OF assms] by (intro ReprF) auto

theorem jeroslow_godel_second:
assumes consistent
― ‹Assumption that is not stated by Jeroslow, but seems to be needed:›
assumes unstated:
        "let ψ = instInpP Pinp (Suc 0) (encF N);
             τ = τJ ψ;
             φ = instInpP (instInpP Pinp (Suc 0) (encF N)) 0 τ;
             φ' = instInpP Pinp 0 (instInpP (encF N) 0 τ)
         in prv (imp (instInp Pinp ⟨φ'⟩) (instInp Pinp ⟨φ⟩))"
shows "¬ prv jcons"
proof
  assume *: "prv jcons"

  define ψ where "ψ ≡ instInpP Pinp (Suc 0) (encF N)"
  define τ where "τ ≡ τJ ψ"
  define φ where "φ ≡ φJ ψ"
  have ψ[simp,intro]: "ψ ∈ fmla" "Fvars ψ = {inp}"
  unfolding ψ_def by auto
  have τ[simp,intro]: "τ ∈ ptrm 0" "τ ∈ fmla" "Fvars τ = {out}"
    unfolding τ_def by auto
  have [simp]: "φ ∈ fmla" "Fvars φ = {}" unfolding φ_def by auto

  define eNτ where "eNτ ≡ instInpP (encF N) 0 τ"
  have eNτ[simp]: "eNτ ∈ ptrm 0" "eNτ ∈ fmla" "Fvars eNτ = {out}"
   unfolding eNτ_def by auto
  define φ' where "φ' ≡ instInpP Pinp 0 eNτ"
  have [simp]: "φ' ∈ fmla" "Fvars φ' = {}" unfolding φ'_def by auto

  have φφ': "prv (imp φ φ')" and φ'φ: "prv (imp φ' φ)" and φeφ': "prv (eqv φ φ')"
   unfolding φ_def φJ_def φ'_def eNτ_def τ_def[symmetric] unfolding ψ_def
   using prv_instInpP_compose[of Pinp "encF N" τ] by auto

  from diagonalization[OF ψ]
  have "prveqlPT τ ⟨instInpP ψ 0 τ⟩" and **: "prv (eqv φ (instInp ψ ⟨φ⟩))"
  unfolding τ_def[symmetric] φ_def[symmetric] by auto
  have "**1": "prv (imp φ (instInp ψ ⟨φ⟩))" "prv (imp (instInp ψ ⟨φ⟩) φ)"
   using prv_imp_eqvEL[OF _ _ **] prv_imp_eqvER[OF _ _ **] by auto

  from SHBL3[OF eNτ(1)]
  have "prv (imp (instInpP Pinp 0 eNτ) (instInp Pinp ⟨instInpP Pinp 0 eNτ⟩))" .
  hence "prv (imp φ' (instInp Pinp ⟨φ'⟩))" unfolding φ'_def .
  from prv_prv_imp_trans[OF _ _ _ φφ' this]
  have 0: "prv (imp φ (instInp Pinp ⟨φ'⟩))" by auto

  note unr = unstated[unfolded Let_def
    φ_def[unfolded φJ_def τ_def[symmetric], symmetric] ψ_def[symmetric]
      τ_def[symmetric] eNτ_def[symmetric] φ'_def[symmetric] φJ_def]

  have 1: "prv (imp φ (instInp Pinp ⟨φ⟩))"
  apply(nrule r: nprv_prvI)
  apply(nrule r: nprv_impI)
  apply(nrule r: nprv_addLemmaE[OF unr])
  apply(nrule r: nprv_addImpLemmaE[OF 0])
  apply(nrule r: nprv_clear3_3)
  by (simp add: nprv_clear2_2 prv_nprv1I unr)

  have 2: "prv (imp φ (cnj (instInp Pinp ⟨φ⟩)
                           (instInp ψ ⟨φ⟩)))"
  apply(nrule r: nprv_prvI)
  apply(nrule r: nprv_impI)
  apply(nrule r: nprv_cnjI)
  subgoal apply(nrule r: nprv_addImpLemmaE[OF 1]) .
  subgoal apply(nrule r: nprv_addImpLemmaE[OF "**1"(1)]) . .

  define z where "z ≡ Variable (Suc (Suc 0))"
  have z_facts[simp]: "z ∈ var" "z ≠ xx" "z ∉ Fvars Pinp"
    "out ≠ z ∧ z ≠ out" "inp ≠ z ∧ z ≠ inp"
   unfolding z_def by auto

  have 30: "subst (instInpP Pinp 0 (instInp (encF N) (Var xx))) ⟨φ⟩ xx =
            instInpP Pinp 0 (instInp (encF N) ⟨φ⟩)"
  unfolding z_def[symmetric] instInp_def instInpP_def Let_def
  by (variousSubsts4 auto
        s1: subst_compose_diff s2: subst_subst
        s3: subst_notIn[of _ _ xx] s4: subst_compose_diff)
  have 31: "subst (instInp Pinp (Var xx)) ⟨φ⟩ xx =
            instInp Pinp ⟨φ⟩" unfolding instInp_def by auto
  have [simp]: "instInp (instInpP Pinp (Suc 0) (encF N)) ⟨φ⟩ =
           instInpP Pinp 0 (instInp (encF N) ⟨φ⟩)"
  by (auto simp: instInp_instInpP ψ_def)

  have 3: "prv (neg (cnj (instInp Pinp ⟨φ⟩)
                         (instInp ψ ⟨φ⟩)))"
  apply(nrule r: nprv_prvI)
  apply(nrule r: nprv_addLemmaE[OF *, unfolded jcons_def])
  apply(rule nprv_allE0[of _ _ _ "⟨φ⟩"], auto)
  unfolding 30 31
  apply(nrule r: nprv_clear2_2)
  apply(nrule r: nprv_negI)
  apply(nrule r: nprv_negE0)
  apply(nrule r: nprv_clear2_2)
  apply(nrule r: nprv_cnjE0)
  apply(nrule r: nprv_clear3_3)
  apply(nrule r: nprv_cnjI)
  apply(nrule r: nprv_clear2_1)
  unfolding ψ_def
  apply(nrule r: nprv_hyp) .

  have ***: "prv (neg φ)"
  apply(nrule r: nprv_prvI)
  apply(nrule r: nprv_negI)
  apply(nrule r: nprv_addImpLemmaE[OF 2])
  apply(nrule r: nprv_addLemmaE[OF 3])
  apply(nrule r: nprv_negE0) .

  have 4: "prv (instInp Pinp ⟨neg φ⟩)" using HBL1_inp[OF _ _ ***] by auto

  have 5: "prveqlPT (instInp (encF N) ⟨φ⟩) ⟨neg φ⟩"
    using ReprF_combineWith_CapN[of φ] by auto

  have [simp]: "instInp (encF N) ⟨φ⟩ ∈ ptrm 0" using instInp by auto

  have 6: "prv (instInpP Pinp 0 (instInp (encF N) ⟨φ⟩))"
  apply(nrule r: nprv_prvI)
  apply(nrule r: nprv_addLemmaE[OF 4])
  apply(nrule r: prveqlPT_nprv_instInpP_instInp[OF _ _ _ _ _ 5]) .

  note lem = "**1"(2)[unfolded ψ_def]
  have "prv φ"
  apply(nrule r: nprv_prvI)
  apply(nrule r: nprv_addLemmaE[OF 6])
  apply(nrule r: nprv_addImpLemmaE[OF lem]) .

  from this *** ‹consistent› show False unfolding consistent_def3 by auto
qed

end ― ‹context @{locale Jeroslow_Godel_Second}›

(*<*)
end
(*>*)