Theory Diagonalization

chapter ‹Diagonalization›

text ‹This theory proves abstract versions of the diagonalization lemma,
with both hard and soft substitution.›


section ‹Alternative Diagonalization via Self-Substitution›

(*<*)
theory Diagonalization imports Abstract_Representability
begin
(*>*)

text ‹
Assuming representability of the diagonal instance of the substitution function,
we prove the standard diagonalization lemma. More precisely, we show that it applies
to any logic that
-- embeds intuitionistic first-order logic over numerals
-- has a countable number of formulas
-- has formula self-substitution representable
›

context Repr_SelfSubst
begin

theorem diagonalization:
  assumes φ[simp,intro!]: "φ  fmla" "Fvars φ = {xx}"
  shows " ψ. ψ  fmla  Fvars ψ = {}  bprv (eqv ψ (subst φ ψ xx))"
proof-
  let ?phi = "λ t. subst φ t xx"
  define χ where "χ  exi yy (cnj (?phi (Var yy)) (SS (Var xx) (Var yy)))"
  have χ[simp,intro!]: "χ  fmla" unfolding χ_def by auto
  let ?chi = "λ t. subst χ t xx"
  define ψ where "ψ  ?chi χ"
  have ψ[simp,intro!]: "ψ  fmla" unfolding ψ_def by auto
  have [simp]: "Fvars χ = {xx}" unfolding χ_def by auto
  hence Fvars_ψ: "Fvars ψ = {}" unfolding ψ_def by auto
  have 1: "bprv (SS χ ψ)"
    using subst_implies_prv_SS[OF χ] unfolding ψ_def by simp
  have 2: "bprv (all yy' (
             imp (cnj (SS χ ψ)
                      (SS χ (Var yy')))
                 (eql ψ (Var yy'))))"
    using Fvars_ψ B.prv_allE[OF _ _ _ SS_unique, of χ "ψ"]
    by fastforce
  have 31: "bprv (all yy'
                     (imp (SS χ ψ)
                          (imp (SS χ (Var yy'))
                               (eql ψ (Var yy')))))"
    using B.prv_all_imp_cnj_rev[OF _ _ _ _ 2] by simp
  have 32: "bprv (imp (SS χ ψ)
                      (all yy' (imp (SS χ (Var yy'))
                                    (eql ψ (Var yy')))))"
    by (intro B.prv_all_imp[OF _ _ _ _ 31]) (auto simp: SS_def2)
  have 33: "bprv (all yy' (imp (SS χ (Var yy'))
                               (eql ψ (Var yy'))))"
    by (rule B.prv_imp_mp [OF _ _ 32 1]) auto
  have 3: "bprv (all yy (imp (SS χ (Var yy))
                             (eql ψ (Var yy))))"
    using B.all_subst_rename_prv[OF _ _ _ _ 33, of yy]
    by fastforce
  have 41: "bprv (imp (?phi ψ)
                      (cnj (?phi ψ)
                           (SS χ ψ)))"
    by (auto intro: in_num B.prv_imp_cnj B.prv_imp_refl B.prv_imp_triv[OF _ _ 1])
  have [simp]: "subst (subst φ ψ xx) ψ yy = subst φ ψ xx"
    by (intro subst_notIn) auto
  have [simp]: "subst (subst φ (Var yy) xx) ψ yy = subst φ ψ xx"
    by (intro subst_subst) auto
  have 42: "bprv (exi yy (imp (?phi ψ)
                              (cnj (?phi (Var yy))
                                   (SS χ (Var yy)))))"
    using 41 by (intro B.prv_exiI[of _ _ "ψ"]) auto
  have 4: "bprv (imp (?phi ψ) (?chi χ))"
    using B.prv_imp_exi[OF _ _ _ _ 42,simplified]
    by (subst χ_def) (auto simp add: subst_comp_num)
  have 50: "bprv (all yy (
          (imp (eql ψ (Var yy))
               (imp (?phi (Var yy))
                    (?phi ψ)))))"
    using B.prv_all_eql[of yy xx φ "ψ" "Var yy"] by simp
  have 51: "bprv (all yy (
          (imp (SS χ (Var yy))
               (imp (?phi (Var yy))
               (?phi ψ)))))" using B.prv_all_imp_trans[OF _ _ _ _ 3 50] by simp
  have 52: "bprv (all yy (
          (imp (cnj (?phi (Var yy))
                    (SS χ (Var yy)))
               (?phi ψ))))" using B.prv_all_imp_cnj[OF _ _ _ _ 51] by simp
  have 5: "bprv (imp (?chi χ) (?phi ψ))"
    using B.prv_exi_imp[OF _ _ _ _ 52,simplified]
    by (subst χ_def) (simp add: subst_comp_num)
  have 6: "bprv (eqv (?chi χ) (?phi ψ))"
    using B.prv_cnjI[OF _ _ 5 4] unfolding eqv_def by simp
  have 7: "bprv (eqv ψ (?phi ψ))" using 6 unfolding ψ_def .
  show ?thesis using ψ 7 Fvars_ψ by blast
qed

text ‹Making this existential into a function.›

definition diag :: "'fmla  'fmla" where
  "diag φ  SOME ψ. ψ  fmla  Fvars ψ = {}  bprv (eqv ψ (subst φ ψ xx))"

theorem diag_everything:
  assumes "φ  fmla" and "Fvars φ = {xx}"
  shows "diag φ  fmla  Fvars (diag φ) = {}  bprv (eqv (diag φ) (subst φ diag φ xx))"
  unfolding diag_def using someI_ex[OF diagonalization[OF assms]] .

lemmas diag[simp] = diag_everything[THEN conjunct1]
lemmas Fvars_diag[simp] = diag_everything[THEN conjunct2, THEN conjunct1]
lemmas bprv_diag_eqv = diag_everything[THEN conjunct2, THEN conjunct2]

end ― ‹context @{locale Repr_SelfSubst}


section ‹Alternative Diagonalization via Soft Self-Substitution›

context Repr_SelfSoftSubst
begin

theorem diagonalization:
  assumes φ[simp,intro!]: "φ  fmla" "Fvars φ = {xx}"
  shows " ψ. ψ  fmla  Fvars ψ = {}  bprv (eqv ψ (subst φ ψ xx))"
proof-
  let ?phi = "λ t. subst φ t xx"
  define χ where "χ  exi yy (cnj (?phi (Var yy)) (SS (Var xx) (Var yy)))"
  have χ[simp,intro!]: "χ  fmla" unfolding χ_def by auto
  let ?chi = "λ t. softSubst χ t xx"
  define ψ where "ψ  ?chi χ"
  have ψ[simp,intro!]: "ψ  fmla" unfolding ψ_def by auto
  have [simp]: "Fvars χ = {xx}" unfolding χ_def by auto
  hence Fvars_ψ: "Fvars ψ = {}" unfolding ψ_def by auto
  have 1: "bprv (SS χ ψ)"
    using softSubst_implies_prv_SS[OF χ] unfolding ψ_def by simp
  have 2: "bprv (all yy' (
             imp (cnj (SS χ ψ)
                      (SS χ (Var yy')))
                 (eql ψ (Var yy'))))"
    using Fvars_ψ B.prv_allE[OF _ _ _ SS_unique, of χ "ψ"]
    by fastforce
  have 31: "bprv (all yy'
                     (imp (SS χ ψ)
                          (imp (SS χ (Var yy'))
                               (eql ψ (Var yy')))))"
    using B.prv_all_imp_cnj_rev[OF _ _ _ _ 2] by simp
  have 32: "bprv (imp (SS χ ψ)
                     (all yy' (imp (SS χ (Var yy'))
                                   (eql ψ (Var yy')))))"
    by (intro B.prv_all_imp[OF _ _ _ _ 31]) (auto simp: SS_def2)
  have 33: "bprv (all yy' (imp (SS χ (Var yy'))
                              (eql ψ (Var yy'))))"
    by (rule B.prv_imp_mp [OF _ _ 32 1]) auto
  have 3: "bprv (all yy (imp (SS χ (Var yy))
                            (eql ψ (Var yy))))"
    using B.all_subst_rename_prv[OF _ _ _ _ 33, of yy]
    by fastforce
  have 41: "bprv (imp (?phi ψ)
                     (cnj (?phi ψ)
                          (SS χ ψ)))"
    by (auto intro: in_num B.prv_imp_cnj B.prv_imp_refl B.prv_imp_triv[OF _ _ 1])
  have [simp]: "subst (subst φ ψ xx) ψ yy = subst φ ψ xx"
    by (intro subst_notIn) auto
  have [simp]: "subst (subst φ (Var yy) xx) ψ yy = subst φ ψ xx"
    by (intro subst_subst) auto
  have 42: "bprv (exi yy (imp (?phi ψ)
                             (cnj (?phi (Var yy))
                                  (SS χ (Var yy)))))"
    using 41 by (intro B.prv_exiI[of _ _ "ψ"]) auto
  have 4: "bprv (imp (?phi ψ) (subst χ χ xx))"
    using B.prv_imp_exi[OF _ _ _ _ 42,simplified]
    by (subst χ_def) (auto simp add: subst_comp_num)
  moreover have "bprv (imp (subst χ χ xx) (?chi χ))" by (rule B.prv_subst_imp_softSubst) auto
  ultimately have 4: "bprv (imp (?phi ψ) (?chi χ))"
    by (rule B.prv_prv_imp_trans[rotated -2]) auto
  have 50: "bprv (all yy (
          (imp (eql ψ (Var yy))
               (imp (?phi (Var yy))
                    (?phi ψ)))))"
    using B.prv_all_eql[of yy xx φ "ψ" "Var yy"] by simp
  have 51: "bprv (all yy (
          (imp (SS χ (Var yy))
               (imp (?phi (Var yy))
               (?phi ψ)))))" using B.prv_all_imp_trans[OF _ _ _ _ 3 50] by simp
  have 52: "bprv (all yy (
          (imp (cnj (?phi (Var yy))
                    (SS χ (Var yy)))
               (?phi ψ))))" using B.prv_all_imp_cnj[OF _ _ _ _ 51] by simp
  have "bprv (imp (?chi χ) (subst χ χ xx))" by (rule B.prv_softSubst_imp_subst) auto
  moreover have "bprv (imp (subst χ χ xx) (?phi ψ))"
    using B.prv_exi_imp[OF _ _ _ _ 52,simplified]
    by (subst χ_def) (simp add: subst_comp_num)
  ultimately have 5: "bprv (imp (?chi χ) (?phi ψ))"
    by (rule B.prv_prv_imp_trans[rotated -2]) auto
  have 6: "bprv (eqv (?chi χ) (?phi ψ))"
    using B.prv_cnjI[OF _ _ 5 4] unfolding eqv_def by simp
  have 7: "bprv (eqv ψ (?phi ψ))" using 6 unfolding ψ_def .
  show ?thesis using ψ 7 Fvars_ψ by blast
qed

text ‹Making this existential into a function.›

definition diag :: "'fmla  'fmla" where
  "diag φ  SOME ψ. ψ  fmla  Fvars ψ = {}  bprv (eqv ψ (subst φ ψ xx))"

theorem diag_everything:
  assumes "φ  fmla" and "Fvars φ = {xx}"
  shows "diag φ  fmla  Fvars (diag φ) = {}  bprv (eqv (diag φ) (subst φ diag φ xx))"
  unfolding diag_def using someI_ex[OF diagonalization[OF assms]] .

lemmas diag[simp] = diag_everything[THEN conjunct1]
lemmas Fvars_diag[simp] = diag_everything[THEN conjunct2, THEN conjunct1]
lemmas prv_diag_eqv = diag_everything[THEN conjunct2, THEN conjunct2]

end ― ‹context @{locale Repr_SelfSoftSubst}

(*<*)
end
(*>*)