Theory Consistency

theory Consistency
  imports Soundness
begin

section ‹Consistency›

text ‹‹NK› is consistent, and the proof stays within Isabelle/HOL and needs only
  ‹Soundness›.  A concrete ‹Σ›-standard model over finite domains
  is exhibited --- so the class ‹ℳ⇘βfb⇙› is non-empty --- whence by soundness ‹NK› does
  not derive ‹❙⊥›, and no sentence is derivable together with its negation. Since ‹NK›
  carries no axiom of infinity it admits finite models, so neither an infinite carrier nor a
  set-theoretic meta-theory is needed, and the parameter type stays unconstrained.  The
  statement is purely syntactic --- non-derivability of ‹❙⊥› in the calculus --- with a
  standard model as its witness; that witness lies in the larger class ‹ℳ⇘βfb⇙› only
  because soundness is proved there.

  The model is built once, for every finite size ‹k > 0› of the individual domain and with a
  parameter interpretation that separates any prescribed family of at most ‹k› parameters.
  Consistency needs only the one-element instance ‹k = 1›; the arbitrarily large instances
  feed the compactness route to the inequation scheme in ‹NK_Infinity›.›

subsection ‹A parametric family of finite standard models›

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

datatype ival = VI nat | VB bool | VF "(ival × ival) list"

fun en :: "nat ⇒ ty ⇒ ival list" where
  "en k ι = map VI [0..<k]"
| "en k 𝗈 = [VB True, VB False]"
| "en k (σ ❙⇒ τ) = map (λvs. VF (zip (en k σ) vs))
                       (List.n_lists (length (en k σ)) (en k τ))"

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

fun cAp :: "ival ⇒ ival ⇒ ival" where
  "cAp (VF G) x = (case map_of G x of Some y ⇒ y | None ⇒ VB False)"
| "cAp v x = VB False"

definition cLm :: "nat ⇒ ty ⇒ (ival ⇒ ival) ⇒ ival" where
 "cLm k σ h ≡ VF (zip (en k σ) (map h (en k σ)))"

lemma en_nonempty: "0 < k ⟹ en k τ ≠ []"
proof (induction τ)
  case Ind then show ?case by simp
next
  case Bool then show ?case by simp
next
  case (Fun σ τ)
  have "replicate (length (en k σ)) (hd (en k τ)) ∈ set (List.n_lists
      (length (en k σ)) (en k τ))"
      using Fun by (auto simp: set_n_lists)
  thus ?case by auto
qed

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

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

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

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

lemma cAp_dom: "cD k (σ ❙⇒ τ) f ⟹ cD k σ a ⟹ cD k τ (cAp f a)"
proof -
  assume "cD k (σ ❙⇒ τ) f" and a: "cD k σ a"
  then obtain vs where vs: "length vs = length (en k σ)" "∀x ∈ set vs. cD k τ x"
    and f: "f = VF (zip (en k σ) vs)" unfolding cD_fun by blast
  obtain b where "map_of (zip (en k σ) 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 k (σ ❙⇒ τ) f" and g: "cD k (σ ❙⇒ τ) g"
      and ag: "⋀a. cD k σ a ⟹ cAp f a = cAp g a"
    shows "f = g"
proof -
  obtain vs where vs: "length vs = length (en k σ)" and fv: "f = VF (zip (en k σ) vs)"
    using f unfolding cD_fun by blast
  obtain ws where ws: "length ws = length (en k σ)" and gw: "g = VF (zip (en k σ) ws)"
    using g unfolding cD_fun by blast
  have "vs ! i = ws ! i" if i: "i < length (en k σ)" for i
  proof -
    have d: "cD k σ (en k σ ! 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 k σ ! i) = vs ! i"
      using map_of_zip_nth[OF vs[symmetric] distinct_en iv] fv by simp
    moreover have "cAp g (en k σ ! 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

subsection ‹Parameters (with prescribed distinctions), assignment, and the model›

text ‹The logical constants need not be built by hand: the frame just constructed is a
  @{locale lambda_universe} (theory ‹Semantics›), so negation, disjunction, quantification, equality
  and description come from that interface --- description by definite description
  (‹THE›), so no Hilbert choice enters the model construction.  The parameter
  interpretation is prescribed by an index map ‹ix›: parameter ‹p› denotes the individual
  ‹VI (ix p)› at type ‹ι› (and a canonical value elsewhere), so that parameters with
  distinct indices denote distinct individuals.›

definition cJv :: "nat ⇒ ('p ⇒ nat) ⇒ 'p ⇒ ty ⇒ ival" where
  "cJv k ix p σ ≡ (if σ = ι then VI (ix p) else hd (en k σ))"

definition cXi :: "nat ⇒ nat ⇒ ty ⇒ ival" where "cXi k n σ ≡ hd (en k σ)"

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

lemma hd_en_dom: "0 < k ⟹ cD k σ (hd (en k σ))" by (simp add: cD_def en_nonempty)

theorem concrete_lambda_universe:
  assumes k: "0 < k" and ix: "⋀p. ix p < k"
  shows "lambda_universe (cD k) cAp (cLm k) (VB True) (VB False)
           (cJv k ix :: 'p ⇒ ty ⇒ ival)"
proof
  show "⋀σ τ h a. (⋀d. cD k σ d ⟹ cD k τ (h d)) ⟹ cD k σ a ⟹ cAp (cLm k σ h) a = h a"
    by simp
  show "⋀σ τ h. (⋀d. cD k σ d ⟹ cD k τ (h d)) ⟹ cD k (σ ❙⇒ τ) (cLm k σ h)"
    by (rule cLm_dom)
  show "⋀σ τ f a. cD k (σ ❙⇒ τ) f ⟹ cD k σ a ⟹ cD k τ (cAp f a)" by (rule cAp_dom)
  show "⋀σ τ g h. cD k (σ ❙⇒ τ) g ⟹ cD k (σ ❙⇒ τ) h ⟹
         (⋀a. cD k σ a ⟹ cAp g a = cAp h a) ⟹ g = h" by (rule cAp_ext)
  show "VB True ≠ VB False" by simp
  show "⋀a. cD k 𝗈 a ⟷ a = VB True ∨ a = VB False" by (rule cD_bool)
  show "⋀p σ. cD k σ (cJv k ix p σ)"
    unfolding cJv_def using k ix hd_en_dom by (auto simp: cD_def)
qed

lemmas concrete_standard_model =
  lambda_universe.is_standard_model[OF concrete_lambda_universe]

subsection ‹Consistency of ‹NK››

text ‹Consistency of ‹NK› (the deep embedding): ‹❙⊥› is not derivable --- by soundness
  (BKK Theorem 7.3) it would have to be ‹υ›-true in the one-element instance ‹k = 1› of the
  finite model, contradicting BKK Lemma 3.43. The argument uses only soundness and one finite
  model; it needs neither the completeness development nor an infinite carrier.›

theorem nk_consistent: "¬ (⊢ (❙⊥ :: 'p tm))"
proof
  assume d: "⊢ (❙⊥ :: 'p tm)"
  define k :: nat where "k = 1"
  have kpos: "0 < k" by (simp add: k_def)
  interpret U: lambda_universe "cD k" cAp "cLm k" "VB True" "VB False"
    "cJv k (λ_. 0) :: 'p ⇒ ty ⇒ ival"
    by (rule concrete_lambda_universe[OF kpos]) (simp add: k_def)
  interpret standard_model "cD k" cAp "cLm k" "VB True" "VB False"
    U.Ngv U.Dsv U.Iv U.Ev U.Piv "cJv k (λ_. 0) :: 'p ⇒ ty ⇒ ival"
    by (rule U.is_standard_model)
  have xi: "bkkA.asg (cXi k)" by (simp add: bkkA.asg_def cXi_def hd_en_dom[OF kpos])
  have "con ({} :: 'p tm set)" by (rule model_con[OF xi]) simp
  thus False using d by (simp add: con_def)
qed

text ‹No formula 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 ‹The same, in the ‹con›sistency terminology of BKK Definition 7.4 (‹con› lives in
  ‹Calculus›): the empty set is consistent.  This theory imports only ‹Soundness›, so the
  dependency graph shows that consistency is independent of the completeness development.›

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

end