Theory Consistency

theory Consistency
  imports Completeness
begin

section ‹Consistency›

text ‹Consistency, in the typical variants: a concrete ‹Σ›-standard model over
  finite domains is exhibited (so the model class ‹ℳ⇘βfb⇙› is non-empty), whence by
  soundness ‹NK› does not derive ‹❙⊥›, and no sentence is derivable together with
  its negation.›

subsection ‹A concrete ‹Σ›-standard model over finite domains›

text ‹The carrier: an individual, the two truth values, and functions as finite graphs.
  With a one-element domain of individuals every domain ‹D⇘τ⇙› is finite, so the full
  function spaces of BKK Definition 3.5 are representable by graphs; ‹en τ› enumerates
  ‹D⇘τ⇙› without repetition.›

datatype mval = MI | MB bool | MF "(mval × mval) list"

fun en :: "ty ⇒ mval list" where
  "en ι = [MI]"
| "en 𝗈 = [MB True, MB False]"
| "en (σ ❙⇒ τ) = map (λvs. MF (zip (en σ) vs))
                     (List.n_lists (length (en σ)) (en τ))"

definition cD :: "ty ⇒ mval ⇒ bool" where "cD τ v ≡ v ∈ set (en τ)"

fun cAp :: "mval ⇒ mval ⇒ mval" where
  "cAp (MF G) x = (case map_of G x of Some y ⇒ y | None ⇒ MI)"
| "cAp v x = MI"

definition cLm :: "ty ⇒ (mval ⇒ mval) ⇒ mval" where
 "cLm σ h ≡ MF (zip (en σ) (map h (en σ)))"

lemma en_nonempty: "en τ ≠ []"
proof (induction τ)
  case (Fun σ τ)
  have "replicate (length (en σ)) (hd (en τ)) ∈ set (List.n_lists
      (length (en σ)) (en τ))" 
      using Fun.IH(2) by (auto simp: set_n_lists)
  thus ?case by auto
qed auto

lemma distinct_en: "distinct (en τ)"
proof (induction τ)
  case (Fun σ τ)
  have "inj_on (λvs. MF (zip (en σ) vs)) (set (List.n_lists (length (en σ)) (en τ)))"
  proof
    fix vs ws
    assume "vs ∈ set (List.n_lists (length (en σ)) (en τ))"
       and "ws ∈ set (List.n_lists (length (en σ)) (en τ))"
    hence "vs = map snd (zip (en σ) vs)" and
          "ws = map snd (zip (en σ) ws)"
      by (auto simp: set_n_lists)
    moreover assume "MF (zip (en σ) vs) = MF (zip (en σ) ws)"
    ultimately show "vs = ws" by simp
  qed
  thus ?case
    by (simp add: distinct_map distinct_n_lists Fun.IH(2))
qed simp_all

lemma cD_fun: "cD (σ ❙⇒ τ) v ⟷ (∃vs.
  length vs = length (en σ) ∧ (∀x ∈ set vs. cD τ x) ∧ v = MF (zip (en σ) vs))"
  by (auto simp: cD_def set_n_lists subset_iff)

lemma cAp_cLm [simp]: "cD σ a ⟹ cAp (cLm σ h) a = h a"
  by (simp add: cLm_def cD_def map_of_zip_map)

lemma cLm_dom: "(⋀d. cD σ d ⟹ cD τ (h d)) ⟹ cD (σ ❙⇒ τ) (cLm σ h)"
  unfolding cD_fun cLm_def
  by (rule exI[of _ "map h (en σ)"]) (auto simp: cD_def)

lemma cAp_dom: "cD (σ ❙⇒ τ) f ⟹ cD σ a ⟹ cD τ (cAp f a)"
proof -
  assume "cD (σ ❙⇒ τ) f" and a: "cD σ a"
  then obtain vs where vs: "length vs = length (en σ)" "∀x ∈ set vs. cD τ x"
    and f: "f = MF (zip (en σ) vs)" unfolding cD_fun by blast
  obtain b where "map_of (zip (en σ) vs) a = Some b" using a vs(1)
    unfolding cD_def by (metis map_of_zip_is_Some)
  moreover from this have "b ∈ set vs"
    by (metis map_of_SomeD set_zip_rightD)
  ultimately show ?thesis using vs(2) f by simp
qed

lemma cAp_ext:
  assumes f: "cD (σ ❙⇒ τ) f" and g: "cD (σ ❙⇒ τ) g"
      and ag: "⋀a. cD σ a ⟹ cAp f a = cAp g a"
    shows "f = g"
proof -
  obtain vs where vs: "length vs = length (en σ)" and fv: "f = MF (zip (en σ) vs)"  
    using f unfolding cD_fun by blast
  obtain ws where ws: "length ws = length (en σ)" and gw: "g = MF (zip (en σ) ws)" 
    using g unfolding cD_fun by blast
  have "vs ! i = ws ! i" if i: "i < length (en σ)" for i
  proof -
    have d: "cD σ (en σ ! i)" using i by (simp add: cD_def)
    have iv: "i < length vs" and iw: "i < length ws" using i vs ws
      by simp_all
    have "cAp f (en σ ! i) = vs ! i"
      using map_of_zip_nth[OF vs[symmetric] distinct_en iv] fv
      by simp
    moreover have "cAp g (en σ ! i) = ws ! i"
      using map_of_zip_nth[OF ws[symmetric] distinct_en iw] gw
      by simp
    ultimately show ?thesis using ag[OF d] by simp
  qed
  hence "vs = ws" using vs ws by (intro nth_equalityI) auto
  thus ?thesis using fv gw by simp
qed

text ‹The denotations of the logical constants, and a canonical parameter
    and assignment interpretation.›

definition cNg :: mval where "cNg ≡ cLm 𝗈 (λa. MB (a = MB False))"
definition cDs :: mval where
  "cDs ≡ cLm 𝗈 (λa. cLm 𝗈 (λb. MB (a = MB True ∨ b = MB True)))"
definition cPi :: "ty ⇒ mval" where
  "cPi σ ≡ cLm (σ ❙⇒ 𝗈) (λf. MB (∀d. cD σ d ⟶ cAp f d = MB True))"
definition cEv :: "ty ⇒ mval" where
  "cEv σ ≡ cLm σ (λa. cLm σ (λb. MB (a = b)))"
definition cIv :: "ty ⇒ mval" where
  "cIv σ ≡ cLm (σ ❙⇒ 𝗈)
    (λf. if ∃a. cD σ a ∧ (∀b. cD σ b ⟶ (cAp f b = MB True) = (b = a))
         then SOME a. cD σ a ∧ (∀b. cD σ b ⟶ (cAp f b = MB True) = (b = a))
         else hd (en σ))"

abbreviation cJv :: "'p ⇒ ty ⇒ mval" where "cJv p σ ≡ hd (en σ)"
abbreviation cXi :: "nat ⇒ ty ⇒ mval" where "cXi n σ ≡ hd (en σ)"

lemma cD_bool: "cD 𝗈 v ⟷ v = MB True ∨ v = MB False"
  by (simp add: cD_def)

lemma hd_en_dom: "cD σ (hd (en σ))" by (simp add: cD_def en_nonempty)

lemma cIv_desc:
  assumes f: "cD (σ ❙⇒ 𝗈) f" and a: "cD σ a"
      and sing: "∀b. cD σ b ⟶ (cAp f b = MB True) = (b = a)"
    shows "cAp (cIv σ) f = a"
proof -
  let ?P = "λx. cD σ x ∧ (∀b. cD σ b ⟶ (cAp f b = MB True) = (b = x))"
  have ex: "∃x. ?P x" using a sing by blast
  have "cAp (cIv σ) f = (SOME x. ?P x)"
    unfolding cIv_def using cAp_cLm[OF f] ex by simp
  moreover have "(SOME x. ?P x) = a"
  proof (rule someI2_ex[OF ex])
    fix x assume x: "?P x"
    have "cAp f a = MB True" using a sing by blast
    thus "x = a" using x a by blast
  qed
  ultimately show ?thesis by simp
qed

theorem concrete_standard_model:
  "standard_model cD cAp cLm (MB True) (MB False) cNg cDs cIv cEv cPi (cJv :: 'p ⇒ ty ⇒ mval)"
proof
  show ‹cD ((σ ❙⇒ 𝗈) ❙⇒ σ) (cIv σ)› for σ
    unfolding cIv_def
    by (rule cLm_dom) (auto simp: hd_en_dom intro: someI2_ex)
next
  fix a b
  assume 13: ‹cD 𝗈 a› ‹cD 𝗈 b›
  have inner: "cAp cDs d = cLm 𝗈 (λb. MB (d = MB True ∨ b = MB True))"
    if "cD 𝗈 d" for d unfolding cDs_def by (rule cAp_cLm[OF that])
  have ds: "cAp (cAp cDs d) e = MB (d = MB True ∨ e = MB True)"
    if d: "cD 𝗈 d" and e: "cD 𝗈 e" for d e unfolding inner[OF d]
    by (rule cAp_cLm[OF e])
  show ‹(cAp (cAp cDs a) b = MB True) = (a = MB True ∨ b = MB True)›
    unfolding ds[OF 13(1) 13(2)] by simp
qed(auto simp: cAp_ext cDs_def cIv_desc cEv_def cPi_def cNg_def cD_bool hd_en_dom
         intro!: cLm_dom cAp_dom)

subsection ‹Consistency of ‹NK››

text ‹The ‹Σ›-model predicate of the canonical construction, exported from the
  sublocale chain ‹standard_model ⊆ general_model ⊆ bkk_model›.›

lemma (in general_model) bkk_model_pred:
  "bkk_model Dm Ap (λξ A. ⦇A⦈⇘ξ⇙) (λa. a = Tv)" by intro_locales

text ‹Consistency of ‹NK› (the deep embedding): ‹❙⊥› is not derivable --- by soundness
  (BKK Theorem 7.3) it would have to be ‹υ›-true in the concrete model, contradicting
  BKK Lemma 3.43.›

theorem nk_consistent: "¬ (⊢ (❙⊥ :: 'p tm))"
proof
  assume d: "⊢ (❙⊥ :: 'p tm)"
  interpret standard_model cD cAp cLm "MB True" "MB False" cNg cDs cIv cEv cPi
                           "cJv :: 'p ⇒ ty ⇒ mval"
    by (rule concrete_standard_model)
  have xi: "bkkA.asg cXi" by (simp add: bkkA.asg_def hd_en_dom)
  have "den (❙⊥ :: 'p tm) cXi = MB True"
    using soundness_bkk[OF d bkk_model_pred xi] by simp
  thus False using bkk.vl_TF[OF xi] by simp
qed

text ‹No sentence is derivable together with its negation.›

theorem nk_not_both: assumes "⊢ (A :: 'p tm)" shows "¬⊢ ❙¬ A"
  using bprov.NegE[OF _ assms wff_FalseB] nk_consistent by blast

text ‹In the terminology of the completeness development: the empty set is consistent
  (BKK Definition 7.4).›

corollary con_empty: "con ({} :: 'p tm set)"
  unfolding con_def by (rule nk_consistent)

end