Theory Compactness

subsection‹Compactness›

theory Compactness
imports Sema
begin

lemma fin_sat_extend: "fin_sat S ⟹ fin_sat (insert F S) ∨ fin_sat (insert (❙¬F) S)"
proof (rule ccontr)
  assume fs: "fin_sat S"
  assume nfs: "¬ (fin_sat (insert F S) ∨ fin_sat (insert (❙¬ F) S))"
  from nfs obtain s1 where s1: "s1 ⊆ insert F S"       "finite s1" "¬sat s1" unfolding fin_sat_def by blast
  from nfs obtain s2 where s2: "s2 ⊆ insert (Not F) S" "finite s2" "¬sat s2" unfolding fin_sat_def by blast
  let ?u = "(s1 - {F}) ∪ (s2 - {Not F})"
  have "?u ⊆ S" "finite ?u" using s1 s2 by auto
  hence "sat ?u" using fs unfolding fin_sat_def by blast
  then obtain A where A: "∀F ∈ ?u. A ⊨ F" unfolding sat_def by blast
  have "A ⊨ F ∨ A ⊨ ❙¬F" by simp
  hence "sat s1 ∨ sat s2" using A unfolding sat_def by(fastforce intro!: exI[where x=A])
  thus False using s1(3) s2(3) by simp
qed

context
begin

lemma fin_sat_antimono: "fin_sat F ⟹ G ⊆ F ⟹ fin_sat G" unfolding fin_sat_def by simp
lemmas fin_sat_insert = fin_sat_antimono[OF _ subset_insertI]

primrec extender :: "nat ⇒ ('a :: countable) formula set ⇒ 'a formula set" where
"extender 0 S = S" |
"extender (Suc n) S = (
  let r = extender n S; 
  rt = insert (from_nat n) r;
  rf = insert (❙¬(from_nat n)) r
  in if fin_sat rf then rf else rt
)"

private lemma extender_fin_sat: "fin_sat S ⟹ fin_sat (extender n S)"
proof(induction n arbitrary: S)
  case (Suc n)
  note mIH = Suc.IH[OF Suc.prems]
  show ?case proof(cases "fin_sat (insert (Not (from_nat n)) (extender n S))")
    case True thus ?thesis by simp
  next
    case False
    hence "fin_sat (insert ((from_nat n)) (extender n S))" using mIH fin_sat_extend by auto
    thus ?thesis by(simp add: Let_def)
  qed
qed simp

definition "extended S = ⋃{extender n S|n. True}"

lemma extended_max: "F ∈ extended S ∨ Not F ∈ extended S"
proof -
  obtain n where [simp]: "F = from_nat n" by (metis from_nat_to_nat)
  have "F ∈ extender (Suc n) S ∨ Not F ∈ extender (Suc n) S" by(simp add: Let_def)
  thus ?thesis unfolding extended_def by blast
qed

private lemma extender_Sucset: "extender k S ⊆ extender (Suc k) S" by(force simp add: Let_def)
private lemma extender_deeper: "F ∈ extender k S ⟹ k ≤ l ⟹ F ∈ extender l S" using extender_Sucset le_Suc_eq
  by(induction l) (auto simp del: extender.simps)
private lemma extender_subset: "S ⊆ extender k S"
proof -
  from extender_deeper[OF _ le0] have "F ∈ extender 0 Sa ⟹ F ∈ extender l Sa" for Sa l F .
  thus ?thesis by auto
qed

lemma extended_fin_sat: 
  assumes "fin_sat S"
  shows  "fin_sat (extended S)"
proof -
  have assm: "⟦s ⊆ extender n S; finite s⟧ ⟹ sat s" for s n
    using extender_fin_sat[OF assms] unfolding fin_sat_def by presburger
  hence "sat s" if su: "s ⊆ ⋃{extender n S |n. True}" and fin: "finite s" for s proof -
    { fix x assume e: "x ∈ s"
      with su have "x ∈ ⋃{extender n S |n. True}" by blast
      hence "∃n. x ∈ extender n S" unfolding Union_eq by blast }
    hence "∀x ∈ s. ∃n. x ∈ extender n S" by blast
    from finite_set_choice[OF fin this] obtain f where cf: "∀x∈s. x ∈ extender (f x) S" ..
    have "∃k. s ⊆ ⋃{extender n S |n. n ≤ k}" proof(intro exI subsetI)
      fix x assume e: "x ∈ s"
      with cf have "x ∈ extender (f x) S" ..
      hence "x ∈ extender (Max (f ` s)) S" by(elim extender_deeper; simp add: e fin)
      thus "x ∈ ⋃{extender n S |n. n ≤ Max (f ` s)}" by blast
    qed
    moreover have "⋃{extender n S |n. n ≤ k} = extender k S" for k proof(induction k) 
      case (Suc k)
      moreover have "⋃{extender n S |n. n ≤ Suc k} = ⋃{extender n S |n. n ≤ k} ∪ extender (Suc k) S" 
        unfolding Union_eq le_Suc_eq
        using le_Suc_eq by(auto simp del: extender.simps)
      ultimately show ?case using extender_Sucset by(force simp del: extender.simps)
    qed simp
    ultimately show "sat s" using assm fin by auto
  qed
  thus ?thesis unfolding extended_def fin_sat_def by presburger
qed

lemma extended_superset: "S ⊆ extended S" unfolding extended_def using extender.simps(1) by blast

lemma extended_complem:
  assumes fs: "fin_sat S"
  shows "(F ∈ extended S) ≠ (Not F ∈ extended S)"
proof -
  note fs = fs[THEN extended_fin_sat]
  show ?thesis proof(cases "F ∈ extended S")
    case False with extended_max show ?thesis by blast
  next
    case True have "Not F ∉ extended S" proof 
      assume False: "Not F ∈ extended S"
      with True have "{F, Not F} ⊆ extended S" by blast
      moreover have "finite {F, Not F}" by simp
      ultimately have "sat {F, Not F}" using fs unfolding fin_sat_def by blast
      thus False unfolding sat_def by simp
    qed
    with True show ?thesis by blast
  qed
qed

lemma not_fin_sat_extended_UNIV: fixes S :: "'a :: countable formula set" assumes "¬fin_sat S" shows "extended S = UNIV" 
text‹Note that this crucially depends on the fact that we check \emph{first} whether adding @{term "❙¬F"} makes the set not satisfiable, 
  and add @{term F} otherwise \emph{without any further checks}.
  The proof of compactness does (to the best of my knowledge) depend on neither of these two facts.›
proof -
  from assms[unfolded fin_sat_def, simplified] obtain s :: "'a :: countable formula set"
    where "finite s" "¬ sat s" by clarify
  from this(2)[unfolded sat_def, simplified] have "∃x∈s. ¬ A ⊨ x" for A ..
  have nfs: "¬fin_sat (insert x (extender n S))" for n x 
    apply(rule notI)
    apply(drule fin_sat_insert)
    apply(drule fin_sat_antimono)
     apply(rule extender_subset)
    apply(erule notE[rotated])
    apply(fact assms)
  done
  have "x ∈ ⋃{extender n S |n. True}" for x proof cases
    assume "x ∈ S" thus ?thesis by (metis extended_def extended_superset insert_absorb insert_subset)
  next
    assume "x ∉ S"
    have "x ∈ extender (Suc (to_nat x)) S" 
      unfolding extender.simps Let_def
      unfolding if_not_P[OF nfs] by simp
    thus ?thesis by blast
  qed
  thus ?thesis unfolding extended_def by auto
qed

lemma extended_tran: "S ⊆ T ⟹ extended S ⊆ extended T"
text‹This lemma doesn't hold: think of making S empty and inserting a formula into T s.t. it can never be satisfied simultaneously with the first 
non-tautological formula in the extension S. Showing that this is possible is not worth the effort, since we can't influence the ordering of formulae.
But we showed it anyway.›
oops
lemma extended_not_increasing: "∃S T. fin_sat S ∧ fin_sat T ∧ ¬ (S ⊆ T ⟶ extended S ⊆ extended (T :: 'a :: countable formula set))"
proof -
  have ex_then_min: "∃x :: nat. P x ⟹ P (LEAST x. P x)" for P using LeastI2_wellorder by auto
  define P where "P x = (let F = (from_nat x :: 'a formula) in (∃A. ¬ A ⊨ F) ∧ (∃ A. A ⊨ F))" for x
  define x where "x = (LEAST n. P n)"
  hence "∃n. P n" unfolding P_def Let_def by(auto intro!: exI[where x="to_nat (Atom undefined :: 'a formula)"])
  from ex_then_min[OF this] have Px: "P x" unfolding x_def .
  have lessx: "n < x ⟹ ¬ P n" for n unfolding x_def using not_less_Least by blast
  let ?S = "{} :: 'a formula set" let ?T = "{from_nat x :: 'a formula}"
  have s: "fin_sat ?S" "fin_sat ?T" using Px unfolding P_def fin_sat_def sat_def Let_def by fastforce+
  have reject: "Q A ⟹ ∀A. ¬ Q A ⟹ False" for A Q by simp
  have "y ≤ x ⟹ F ∈ extender y ?S ⟹ ⊨ F" for F y
  proof(induction y arbitrary: F)
    case (Suc y)
    have *: "F ∈ extender y {} ⟹ ⊨ F" for F :: "'a formula" using Suc.IH Suc.prems(1) by auto
    let ?Y = "from_nat y :: 'a formula"
    have ex: "(∀A. ¬ A ⊨ ?Y) ∨ ⊨ ?Y" unfolding formula_semantics.simps by (meson P_def Suc.prems(1) Suc_le_lessD lessx)
    have 1: "∀A. ¬ A ⊨ ?Y" if "fin_sat (Not ?Y ▹ extender y ?S)"
    proof -
      note[[show_types]]
      from that have "∃A. A ⊨ Not ?Y" unfolding fin_sat_def sat_def  by(elim allE[where x="{Not ?Y}"]) simp
      hence "¬⊨ ?Y" by simp
      hence "∀A. ¬ A ⊨ ?Y" using ex by argo
      thus ?thesis by simp
    qed
    have 2: "¬ fin_sat (Not ?Y ▹ extender y ?S) ⟹ ⊨ ?Y"
    proof(erule contrapos_np)
      assume "¬ ⊨ ?Y"
      hence "∀A. ¬ A ⊨ ?Y" using ex by argo
      hence "⊨ ❙¬ ?Y" by simp
      thus "fin_sat (❙¬ ?Y ▹ extender y ?S)" unfolding fin_sat_def sat_def
        by(auto intro!: exI[where x="λ_ :: 'a. False"] dest!: rev_subsetD[rotated] *)
    qed
    show ?case using Suc.prems(2) by(simp add: Let_def split: if_splits; elim disjE; simp add: * 1 2)
  qed simp
  hence "fin_sat (❙¬ (from_nat x) ▹ extender x ?S)" using Px unfolding P_def Let_def
    by (clarsimp simp: fin_sat_def sat_def) (insert formula_semantics.simps(3), blast)
  hence "Not (from_nat x) ∈ extender (Suc x) ?S" by(simp)
  hence "Not (from_nat x) ∈ extended ?S" unfolding extended_def by blast
  moreover have "Not (from_nat x) ∉ extended ?T" using extended_complem extended_superset s(2) by blast
  ultimately show ?thesis using s by blast
qed

private lemma not_in_extended_FE: "fin_sat S ⟹ (¬sat (insert (Not F) G)) ⟹ F ∉ extended S ⟹ G ⊆ extended S ⟹ finite G ⟹ False"
proof(goal_cases)
  case 1
  hence "Not F ∈ extended S" using extended_max by blast
  thus False using 1 extended_fin_sat fin_sat_def
    by (metis Diff_eq_empty_iff finite.insertI insert_Diff_if)
qed
  
lemma extended_id: "extended (extended S) = extended S" 
  using extended_complem extended_fin_sat extended_max extended_superset not_fin_sat_extended_UNIV 
  by(intro equalityI[rotated] extended_superset) blast
  
(* This would be nicer, though… 
inductive_set extended_set :: "form set ⇒ form set" for S where
"F ∈ S ⟹ F ∈ extended_set S" |
"fin_sat (insert F (extended_set S)) ∨ F ∈ extended_set S ⟹ F ∈ extended_set S"
but it can't work, as extended is not increasing (?) *)
  
lemma ext_model:
  assumes r: "fin_sat S"
  shows "(λk. Atom k ∈ extended S) ⊨ F ⟷ F ∈ extended S"
proof -
  note fs = r[THEN extended_fin_sat]
  have Elim: "F ∈ S ∧ G ∈ S ⟹ {F,G} ⊆ S" "F ∈ S ⟹ {F} ⊆ S" for F G S by simp+
  show ?thesis
  proof(induction F)
    case Atom thus ?case by(simp)
  next
    case Bot
    have False if "⊥ ∈ extended S" proof -
      have "finite {⊥}" by simp
      moreover from that have "{⊥} ⊆ extended S" by simp
      ultimately have "∃A. A ⊨ ⊥" using fs unfolding fin_sat_def sat_def
        by(elim allE[of _ "{⊥}"]) simp
      thus False by simp
    qed
    thus ?case by auto
  next
    case (Not F)
    moreover have "A ⊨ F ≠ A ⊨ ❙¬F" for A F by simp
    ultimately show ?case using extended_complem[OF r] by blast
  next
    case (And F G)
    have "(F ∈ extended S ∧ G ∈ extended S) = (F ❙∧ G ∈ extended S)" proof -
      have *: "¬sat {❙¬ (F ❙∧ G), F, G}" "¬sat {❙¬ F, (F ❙∧ G)}" "¬sat {❙¬ G, (F ❙∧ G)}" unfolding sat_def by auto
      show ?thesis by(intro iffI; rule ccontr) (auto intro: *[THEN not_in_extended_FE[OF r]])
    qed
    thus ?case by(simp add: And) 
  next
    case (Or F G)
    have "(F ∈ extended S ∨ G ∈ extended S) = (F ❙∨ G ∈ extended S)" proof -
      have "¬sat {❙¬(F ❙∨ G), F}" "¬sat {❙¬(F ❙∨ G), G}" unfolding sat_def by auto
      from this[THEN not_in_extended_FE[OF r]] have 1: "⟦F ∈ extended S ∨ G ∈ extended S; F ❙∨ G ∉ extended S⟧ ⟹ False" by auto
      have "¬sat {❙¬F, ❙¬G, F ❙∨ G}" unfolding sat_def by auto
      hence 2: "⟦F ❙∨ G ∈ extended S; F ∉ extended S; G ∉ extended S⟧ ⟹ False" using extended_max not_in_extended_FE[OF r] by fastforce
      show ?thesis by(intro iffI; rule ccontr) (auto intro: 1 2)
    qed
    thus ?case by(simp add: Or)
  next
    case (Imp F G)
    have "(F ∈ extended S ⟶ G ∈ extended S) = (F ❙→ G ∈ extended S)" proof -
      have "¬sat {❙¬G, F, F ❙→ G}" unfolding sat_def by auto
      hence 1: "⟦F ❙→ G ∈ extended S; F ∈ extended S; G ∉ extended S⟧ ⟹ False" using extended_max not_in_extended_FE[OF r] by blast
      have "¬sat {❙¬F,❙¬(F ❙→ G)}" unfolding sat_def by auto
      hence 2: "⟦F ❙→ G ∉ extended S; F ∉ extended S⟧ ⟹ False" using extended_max not_in_extended_FE[OF r] by blast
      have "¬sat {❙¬(F ❙→ G),G}" unfolding sat_def by auto
      hence 3: "⟦F ❙→ G ∉ extended S; G ∈ extended S⟧ ⟹ False" using extended_max not_in_extended_FE[OF r] by blast
      show ?thesis by(intro iffI; rule ccontr) (auto intro: 1 2 3)
    qed
    thus ?case by(simp add: Imp)
  qed
qed

theorem compactness:
  fixes S :: "'a :: countable formula set"
  shows "sat S ⟷ fin_sat S" (is "?l = ?r")
proof
  assume ?l thus ?r unfolding sat_def fin_sat_def by blast
next
  assume r: ?r
  note ext_model[OF r, THEN iffD2]
  hence "∀F∈S. (λk. Atom k ∈ extended S) ⊨ F" using extended_superset by blast
  thus ?l unfolding sat_def by blast
qed

corollary compact_entailment:
  fixes F :: "'a :: countable formula"
  assumes fent: "Γ ⊫ F"
  shows "∃Γ'. finite Γ' ∧ Γ' ⊆ Γ ∧ Γ' ⊫ F"
proof -
  have ND_sem:  "Γ ⊫ F ⟷ ¬sat (insert (❙¬F) Γ)" 
    for Γ F unfolding sat_def entailment_def by auto
  obtain Γ' where 0: "finite Γ'" "Γ' ⊫ F" "Γ' ⊆ Γ" proof(goal_cases)
    from fent[unfolded ND_sem compactness] have "¬ fin_sat (insert (❙¬ F) Γ)" .
    from this[unfolded fin_sat_def] obtain s where s: "s ⊆ insert(❙¬F) Γ" "finite s" "¬sat s" by blast
    have 2: "finite (s - {❙¬ F})" using s by simp
    have 3: "s - {❙¬ F} ⊫ F" unfolding ND_sem using s(3) unfolding sat_def by blast
    have 4: "s - {❙¬ F} ⊆ Γ" using s by blast
    case 1 from 2 3 4 show ?case by(intro 1[of "s - {Not F}"])
  qed
  thus ?thesis by blast
qed
  
corollary compact_to_formula:
  fixes F :: "'a :: countable formula"
  assumes fent: "Γ ⊫ F"
  obtains Γ' where "set Γ' ⊆ Γ" "⊨ (❙⋀Γ') ❙→ F"
proof goal_cases
  case 1
  from compact_entailment[OF assms]
  obtain Γ' where Γ': "finite Γ' ∧ Γ' ⊆ Γ ∧ Γ' ⊫ F" ..
  then obtain Γ'' where "Γ' = set Γ''" using finite_list by auto
  with Γ' show thesis by(intro 1)  (blast, simp add: entailment_def)
qed

end
    
end