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 fχ[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
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 fχ[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
end