Theory Propositional_Proof_Systems.Consistency

subsection‹Consistency›

text‹We follow the proofs by Melvin Fitting~\<^cite>‹"fitting1990first"›.›
theory Consistency
imports Sema
begin

definition "Hintikka S ≡ (
  ⊥ ∉ S
∧ (∀k. Atom k ∈ S ⟶ ❙¬ (Atom k) ∈ S ⟶ False)
∧ (∀F G. F ❙∧ G ∈ S ⟶ F ∈ S ∧ G ∈ S)
∧ (∀F G. F ❙∨ G ∈ S ⟶ F ∈ S ∨ G ∈ S)
∧ (∀F G. F ❙→ G ∈ S ⟶ ❙¬F ∈ S ∨ G ∈ S)
∧ (∀F. ❙¬ (❙¬F) ∈ S ⟶ F ∈ S)
∧ (∀F G. ❙¬(F ❙∧ G) ∈ S ⟶ ❙¬ F ∈ S ∨ ❙¬ G ∈ S)
∧ (∀F G. ❙¬(F ❙∨ G) ∈ S ⟶ ❙¬ F ∈ S ∧ ❙¬ G ∈ S)
∧ (∀F G. ❙¬(F ❙→ G) ∈ S ⟶ F ∈ S ∧ ❙¬ G ∈ S)
)"

lemma "Hintikka {Atom 0 ❙∧ ((❙¬ (Atom 1)) ❙→ Atom 2), ((❙¬ (Atom 1)) ❙→ Atom 2), Atom 0, ❙¬(❙¬ (Atom 1)), Atom 1}"
  unfolding Hintikka_def by simp

theorem Hintikkas_lemma:
  assumes H: "Hintikka S"
  shows "sat S"
proof -
  from H[unfolded Hintikka_def]
  have H': "⊥ ∉ S" 
    "Atom k ∈ S ⟹ ❙¬ (Atom k) ∈ S ⟹ False"
    "F ❙∧ G ∈ S ⟹ F ∈ S ∧ G ∈ S"
    "F ❙∨ G ∈ S ⟹ F ∈ S ∨ G ∈ S"
    "F ❙→ G ∈ S ⟹ ❙¬F ∈ S ∨ G ∈ S"
    "❙¬ (❙¬ F) ∈ S ⟹ F ∈ S"
    "❙¬ (F ❙∧ G) ∈ S ⟹ ❙¬ F ∈ S ∨ ❙¬ G ∈ S"
    "❙¬ (F ❙∨ G) ∈ S ⟹ ❙¬ F ∈ S ∧ ❙¬ G ∈ S"
    "❙¬ (F ❙→ G) ∈ S ⟹ F ∈ S ∧ ❙¬ G ∈ S"
    for k F G by blast+
  let ?M = "λk. Atom k ∈ S"
  have "(F ∈ S ⟶ (?M ⊨ F)) ∧ (❙¬ F ∈ S ⟶ (¬(?M ⊨ F)))" for F
    by(induction F) (auto simp: H'(1) dest!: H'(2-))
  thus ?thesis unfolding sat_def by blast
qed

definition "pcp C ≡ (∀S ∈ C.
  ⊥ ∉ S
∧ (∀k. Atom k ∈ S ⟶ ❙¬ (Atom k) ∈ S ⟶ False)
∧ (∀F G. F ❙∧ G ∈ S ⟶ F ▹ G ▹ S ∈ C)
∧ (∀F G. F ❙∨ G ∈ S ⟶ F ▹ S ∈ C ∨ G ▹ S ∈ C)
∧ (∀F G. F ❙→ G ∈ S ⟶ ❙¬F ▹ S ∈ C ∨ G ▹ S ∈ C)
∧ (∀F. ❙¬ (❙¬F) ∈ S ⟶ F ▹ S ∈ C)
∧ (∀F G. ❙¬(F ❙∧ G) ∈ S ⟶ ❙¬ F ▹ S ∈ C ∨ ❙¬ G ▹ S ∈ C)
∧ (∀F G. ❙¬(F ❙∨ G) ∈ S ⟶ ❙¬ F ▹ ❙¬ G ▹ S ∈ C)
∧ (∀F G. ❙¬(F ❙→ G) ∈ S ⟶ F ▹ ❙¬ G ▹ S ∈ C)
)"

(* just some examples *)
lemma "pcp {}" "pcp {{}}" "pcp {{Atom 0}}" by (simp add: pcp_def)+
lemma "pcp {{(❙¬ (Atom 1)) ❙→ Atom 2},
   {((❙¬ (Atom 1)) ❙→ Atom 2), ❙¬(❙¬ (Atom 1))},
  {((❙¬ (Atom 1)) ❙→ Atom 2), ❙¬(❙¬ (Atom 1)),  Atom 1}}" by (auto simp add: pcp_def)

text‹Fitting uses uniform notation~\<^cite>‹"smullyan1963unifying"› for the definition of @{const pcp}. 
We try to mimic this, more to see whether it works than because it is ultimately necessary.›
(* It does help a bit, occasionally. *)
    
inductive Con :: "'a formula => 'a formula => 'a formula => bool" where
"Con (And F G) F G" |
"Con (Not (Or F G)) (Not F) (Not G)" |
"Con (Not (Imp F G)) F (Not G)" |
"Con (Not (Not F)) F F"

inductive Dis :: "'a formula => 'a formula => 'a formula => bool" where
"Dis (Or F G) F G" |
"Dis (Imp F G) (Not F) G" |
"Dis (Not (And F G)) (Not F) (Not G)" |
"Dis (Not (Not F)) F F"

(* note that *)
lemma "Con (Not (Not F)) F F" "Dis (Not (Not F)) F F" by(intro Con.intros Dis.intros)+
(* i.e. ❙¬❙¬ is both Conjunctive and Disjunctive. I saw no reason to break this symmetry. *)

lemma con_dis_simps:
  "Con a1 a2 a3 = (a1 = a2 ❙∧ a3 ∨ (∃F G. a1 = ❙¬ (F ❙∨ G) ∧ a2 = ❙¬ F ∧ a3 = ❙¬ G) ∨ (∃G. a1 = ❙¬ (a2 ❙→ G) ∧ a3 = ❙¬ G) ∨ a1 = ❙¬ (❙¬ a2) ∧ a3 = a2)"
  "Dis a1 a2 a3 = (a1 = a2 ❙∨ a3 ∨ (∃F G. a1 = F ❙→ G ∧ a2 = ❙¬ F ∧ a3 = G) ∨ (∃F G. a1 = ❙¬ (F ❙∧ G) ∧ a2 = ❙¬ F ∧ a3 = ❙¬ G) ∨ a1 = ❙¬ (❙¬ a2) ∧ a3 = a2)"
  by(simp_all add: Con.simps Dis.simps)

lemma Hintikka_alt: "Hintikka S = (
  ⊥ ∉ S
∧ (∀k. Atom k ∈ S ⟶ ❙¬ (Atom k) ∈ S ⟶ False)
∧ (∀F G H. Con F G H ⟶ F ∈ S ⟶ G ∈ S ∧ H ∈ S)
∧ (∀F G H. Dis F G H ⟶ F ∈ S ⟶ G ∈ S ∨ H ∈ S)
)"  
  apply(simp add: Hintikka_def con_dis_simps)
  apply(rule iffI)
    (* simp only: ∅ loops. :( *)
   subgoal by blast
  subgoal by safe metis+
done

lemma pcp_alt: "pcp C = (∀S ∈ C.
  ⊥ ∉ S
∧ (∀k. Atom k ∈ S ⟶ ❙¬ (Atom k) ∈ S ⟶ False)
∧ (∀F G H. Con F G H ⟶ F ∈ S ⟶ G ▹ H ▹ S ∈ C)
∧ (∀F G H. Dis F G H ⟶ F ∈ S ⟶ G ▹ S ∈ C ∨ H ▹ S ∈ C)
)"
  apply(simp add: pcp_def con_dis_simps)
  apply(rule iffI; unfold Ball_def; elim all_forward)
  by (auto simp add: insert_absorb split: formula.splits)
  
definition "subset_closed C ≡ (∀S ∈ C. ∀s⊆S. s ∈ C)"
definition "finite_character C ≡ (∀S. S ∈ C ⟷ (∀s ⊆ S. finite s ⟶ s ∈ C))"

lemma ex1: "pcp C ⟹ ∃C'. C ⊆ C' ∧ pcp C' ∧ subset_closed C'"
proof(intro exI[of _ "{s . ∃S ∈ C. s ⊆ S}"] conjI)
  let ?E = "{s. ∃S∈C. s ⊆ S}"
  show "C ⊆ ?E" by blast
  show "subset_closed ?E" unfolding subset_closed_def by blast
  assume C: ‹pcp C›
  show "pcp ?E" using C unfolding pcp_alt
    by (intro ballI conjI; simp; meson insertI1 rev_subsetD subset_insertI subset_insertI2)
qed

lemma sallI: "(⋀s. s ⊆ S ⟹ P s) ⟹ ∀s ⊆ S. P s" by simp 

lemma ex2: 
  assumes fc: "finite_character C"
  shows "subset_closed C"
  unfolding subset_closed_def
proof (intro ballI sallI)
  fix s S
  assume e: ‹S ∈ C› and s: ‹s ⊆ S›
  hence *: "t ⊆ s ⟹ t ⊆ S" for t by simp
  from fc have "t ⊆ S ⟹ finite t ⟹ t ∈ C" for t unfolding finite_character_def using e by blast
  hence "t ⊆ s ⟹ finite t ⟹ t ∈ C" for t using * by simp
  with fc show ‹s ∈ C› unfolding finite_character_def by blast
qed

lemma
  assumes C: "pcp C"
  assumes S: "subset_closed C"
  shows ex3: "∃C'. C ⊆ C' ∧ pcp C' ∧ finite_character C'"
proof(intro exI[of _ "C ∪ {S. ∀s ⊆ S. finite s ⟶ s ∈ C}"] conjI)
  let ?E = " {S. ∀s ⊆ S. finite s ⟶ s ∈ C}"
  show "C ⊆ C ∪ ?E" by blast
  from S show "finite_character (C ∪ ?E)" unfolding finite_character_def subset_closed_def by blast
  note C'' = C[unfolded pcp_alt, THEN bspec]
    
  (* uniform notation. what did I learn? only slightly more elegant… *)
  have CON: "G ▹ H ▹ S ∈ C ∪ {S. ∀s⊆S. finite s ⟶ s ∈ C}" if si: "⋀s. ⟦s⊆S; finite s⟧ ⟹ s ∈ C" and
    un: "Con F G H" and el: " F ∈ S" for F G H S proof -
    have k: "∀s ⊆ S. finite s ⟶ F ∈ s ⟶ G ▹ H ▹ s ∈ C"
      using si un C'' by simp
    have "G ▹ H ▹ S ∈ ?E"
      unfolding mem_Collect_eq Un_iff proof safe
      fix s
      assume "s ⊆ G ▹ H ▹ S" and f: "finite s"
      hence "F ▹ (s - {G,H}) ⊆ S" using el by blast
      with k f have "G ▹ H ▹ F ▹ (s - {G,H}) ∈ C" by simp
      hence "F ▹ G ▹ H ▹ s ∈ C" using insert_absorb by fastforce
      thus "s ∈ C" using S unfolding subset_closed_def by fast  
    qed
    thus "G ▹ H ▹ S ∈ C ∪ ?E" by simp
  qed
  have DIS: "G ▹ S ∈ C ∪ {S. ∀s⊆S. finite s ⟶ s ∈ C} ∨ H ▹ S ∈ C ∪ {S. ∀s⊆S. finite s ⟶ s ∈ C}" 
    if si: "⋀s. s⊆S ⟹ finite s ⟹ s ∈ C" and un: "Dis F G H" and el: "F ∈ S"
    for F G H S proof -
    have l: "∃I∈{G, H}. I ▹ s1 ∈ C ∧ I ▹ s2 ∈ C" 
      if "s1 ⊆ S" "finite s1" "F ∈ s1" 
         "s2 ⊆ S" "finite s2" "F ∈ s2" for s1 s2
    proof -
      let ?s = "s1 ∪ s2"
      have "?s ⊆ S" "finite ?s" using that by simp_all 
      with si have "?s ∈ C" by simp
      moreover have "F ∈ ?s" using that by simp
      ultimately have "∃I∈{G,H}. I ▹ ?s ∈ C"
        using C'' un by simp
      thus "∃I∈{G,H}. I ▹ s1 ∈ C ∧ I ▹ s2 ∈ C"
        by (meson S[unfolded subset_closed_def, THEN bspec] insert_mono sup.cobounded2 sup_ge1)
    qed
    have m: "⟦s1 ⊆ S; finite s1; F ∈ s1; G ▹ s1 ∉ C; s2 ⊆ S; finite s2; F ∈ s2; H ▹ s2 ∉ C⟧ ⟹ False" for s1 s2
      using l by blast
    have "False" if "s1 ⊆ S" "finite s1" "G ▹ s1 ∉ C" "s2 ⊆ S" "finite s2" "H ▹ s2 ∉ C" for s1 s2
    proof -
      have *: "F ▹ s1 ⊆ S" "finite (F ▹ s1)" "F ∈ F ▹ s1" if  "s1 ⊆ S" "finite s1" for s1
        using that el by simp_all
      have  "G ▹ F ▹ s1 ∉ C" "H ▹ F ▹ s2 ∉ C" 
        by (meson S insert_mono subset_closed_def subset_insertI that(3,6))+
      from m[OF *[OF that(1-2)] this(1) *[OF that(4-5)] this(2)]
      show False .
    qed
    hence "G ▹ S ∈ ?E ∨ H ▹ S ∈ ?E"
      unfolding mem_Collect_eq Un_iff
      by (metis (no_types, lifting) finite_Diff insert_Diff si subset_insert_iff)
    thus "G ▹ S ∈ C ∪ ?E ∨ H ▹ S ∈ C ∪ ?E" by blast
  qed
    
  (* this proof does benefit from uniform notation a bit. Before it was introduced,
     the subclaims CON, DIS had to be stated as *)  
  have CON': "⋀f2 g2 h2 F2 G2 S2. ⟦⋀s. ⟦s ∈ C; h2 F2 G2 ∈ s⟧ ⟹ f2 F2 ▹ s ∈ C ∨ g2 G2 ▹ s ∈ C; 
                                   ∀s⊆S2. finite s ⟶ s ∈ C; h2 F2 G2 ∈ S2; False⟧
      ⟹ f2 F2 ▹ S2 ∈ C ∪ {S. ∀s⊆S. finite s ⟶ s ∈ C} ∨ g2 G2 ▹ S2 ∈ C ∪ {S. ∀s⊆S. finite s ⟶ s ∈ C}" 
    by fast
  (* (without the False, obviously). The proof of the subclaim does not change gravely, 
      but the f2 g2 h2 have to be instantiated manually upon use (with, e.g., id Not (λF G. ❙¬(F ❙→ G))),
      and there were multiple working instantiations. Generally not as beautiful. *)

  show "pcp (C ∪ ?E)" unfolding pcp_alt
    apply(intro ballI conjI; elim UnE; (unfold mem_Collect_eq)?)
           subgoal using C'' by blast
          subgoal using C'' by blast
         subgoal using C'' by (simp;fail)
        subgoal by (meson C'' empty_subsetI finite.emptyI finite_insert insert_subset subset_insertI)
       subgoal using C'' by simp
      subgoal using CON by simp
     subgoal using C'' by blast
    subgoal using DIS by simp
  done
qed

primrec pcp_seq where
"pcp_seq C S 0 = S" |
"pcp_seq C S (Suc n) = (
  let Sn = pcp_seq C S n; Sn1 = from_nat n ▹ Sn in
  if Sn1 ∈ C then Sn1 else Sn
)"

lemma pcp_seq_in: "pcp C ⟹ S ∈ C ⟹ pcp_seq C S n ∈ C"
proof(induction n)
  case (Suc n)
  hence "pcp_seq C S n ∈ C" by simp
  thus ?case by(simp add: Let_def)
qed simp
  
lemma pcp_seq_mono: "n ≤ m ⟹ pcp_seq C S n ⊆ pcp_seq C S m"
proof(induction m)
  case (Suc m)
  thus ?case by(cases "n = Suc m"; simp add: Let_def; blast)
qed simp

lemma pcp_seq_UN: "⋃{pcp_seq C S n|n. n ≤ m} = pcp_seq C S m"
proof(induction m)
  case (Suc m)
  have "{f n |n. n ≤ Suc m} = f (Suc m) ▹ {f n |n. n ≤ m}" for f using le_Suc_eq by auto
  hence "{pcp_seq C S n |n. n ≤ Suc m} = pcp_seq C S (Suc m) ▹ {pcp_seq C S n |n. n ≤ m}" .
  hence "⋃{pcp_seq C S n |n. n ≤ Suc m} = ⋃{pcp_seq C S n |n. n ≤ m} ∪ pcp_seq C S (Suc m)" by auto
  thus ?case using Suc pcp_seq_mono by blast
qed simp
  
lemma wont_get_added: "(F :: ('a :: countable) formula) ∉ pcp_seq C S (Suc (to_nat F)) ⟹ F ∉ pcp_seq C S (Suc (to_nat F) + n)"
text‹We don't necessarily have @{term "n = to_nat (from_nat n)"}, so this doesn't hold.›
oops

definition "pcp_lim C S ≡ ⋃{pcp_seq C S n|n. True}"
  
lemma pcp_seq_sub: "pcp_seq C S n ⊆ pcp_lim C S"
  unfolding pcp_lim_def by(induction n; blast)
    
lemma pcp_lim_inserted_at_ex: "x ∈ pcp_lim C S ⟹ ∃k. x ∈ pcp_seq C S k"
  unfolding pcp_lim_def by blast

lemma pcp_lim_in:
  assumes c: "pcp C"
  and el: "S ∈ C"
  and sc: "subset_closed C"
  and fc: "finite_character C"
  shows "pcp_lim C S ∈ C" (is "?cl ∈ C")
proof -
  from pcp_seq_in[OF c el, THEN allI] have "∀n. pcp_seq C S n ∈ C" .
  hence "∀m. ⋃{pcp_seq C S n|n. n ≤ m} ∈ C" unfolding pcp_seq_UN .
  
  have "∀s ⊆ ?cl. finite s ⟶ s ∈ C"
  proof safe
    fix s :: "'a formula set"
    have "pcp_seq C S (Suc (Max (to_nat ` s))) ⊆ pcp_lim C S" using pcp_seq_sub by blast
    assume ‹finite s› ‹s ⊆ pcp_lim C S›
    hence "∃k. s ⊆ pcp_seq C S k" 
    proof(induction s rule: finite_induct) 
      case (insert x s)
      then obtain k1 where "s ⊆ pcp_seq C S k1" by blast
      moreover obtain k2 where "x ∈ pcp_seq C S k2"
        by (meson pcp_lim_inserted_at_ex insert.prems insert_subset)
      ultimately have "x ▹ s ⊆ pcp_seq C S (max k1 k2)"
        by (meson pcp_seq_mono dual_order.trans insert_subset max.bounded_iff order_refl subsetCE)
      thus ?case by blast
    qed simp
    with pcp_seq_in[OF c el] sc
    show "s ∈ C" unfolding subset_closed_def by blast
  qed
  thus "?cl ∈ C" using fc unfolding finite_character_def by blast
qed
  
lemma cl_max:
  assumes c: "pcp C"
  assumes sc: "subset_closed C"
  assumes el: "K ∈ C"
  assumes su: "pcp_lim C S ⊆ K"
  shows "pcp_lim C S = K" (is ?e)
proof (rule ccontr)
  assume ‹¬?e›
  with su have "pcp_lim C S ⊂ K" by simp
  then obtain F where e: "F ∈ K" and ne: "F ∉ pcp_lim C S" by blast
  from ne have "F ∉ pcp_seq C S (Suc (to_nat F))" using pcp_seq_sub by fast
  hence 1: "F ▹ pcp_seq C S (to_nat F) ∉ C" by (simp add: Let_def split: if_splits)
  have "F ▹ pcp_seq C S (to_nat F) ⊆ K" using pcp_seq_sub e su by blast
  hence "F ▹ pcp_seq C S (to_nat F) ∈ C" using sc unfolding subset_closed_def using el by blast
  with 1 show False ..
qed

lemma cl_max':
  assumes c: "pcp C"
  assumes sc: "subset_closed C"
  shows "F ▹ pcp_lim C S ∈ C ⟹ F ∈ pcp_lim C S"
    "F ▹ G ▹ pcp_lim C S ∈ C ⟹ F ∈ pcp_lim C S ∧ G ∈ pcp_lim C S"
using cl_max[OF assms] by blast+

lemma pcp_lim_Hintikka:
  assumes c: "pcp C"
  assumes sc: "subset_closed C"
  assumes fc: "finite_character C"
  assumes el: "S ∈ C"
  shows "Hintikka (pcp_lim C S)"
proof -
  let ?cl = "pcp_lim C S"
  have "?cl ∈ C" using pcp_lim_in[OF c el sc fc] .
  from c[unfolded pcp_alt, THEN bspec, OF this]
  have d: "⊥ ∉ ?cl"
    "Atom k ∈ ?cl ⟹ ❙¬ (Atom k) ∈ ?cl ⟹ False"
    "Con F G H ⟹ F ∈ ?cl ⟹ G ▹ H ▹ ?cl ∈ C"
    "Dis F G H ⟹ F ∈ ?cl ⟹ G ▹ ?cl ∈ C ∨ H ▹ ?cl ∈ C"
  for k F G H by blast+
  have
    "Con F G H ⟹ F ∈ ?cl ⟹ G ∈ ?cl ∧ H ∈ ?cl"
    "Dis F G H ⟹ F ∈ ?cl ⟹ G ∈ ?cl ∨ H ∈ ?cl"
    for F G H
    by(auto dest: d(3-) cl_max'[OF c sc])
  with d(1,2) show ?thesis unfolding Hintikka_alt by fast
qed
  
theorem pcp_sat: ― ‹model existence theorem›
  fixes S :: "'a :: countable formula set"
  assumes c: "pcp C"
  assumes el: "S ∈ C"
  shows "sat S"
proof -
  note [[show_types]]
  from c obtain Ce where "C ⊆ Ce" "pcp Ce" "subset_closed Ce" "finite_character Ce" using ex1[where 'a='a] ex2[where 'a='a] ex3[where 'a='a]
    by (meson dual_order.trans ex2)
  have "S ∈ Ce" using ‹C ⊆ Ce› el ..
  with pcp_lim_Hintikka ‹pcp Ce› ‹subset_closed Ce› ‹finite_character Ce›
  have  "Hintikka (pcp_lim Ce S)" .
  with Hintikkas_lemma have "sat (pcp_lim Ce S)" .
  moreover have "S ⊆ pcp_lim Ce S" using pcp_seq.simps(1) pcp_seq_sub by fast
  ultimately show ?thesis unfolding sat_def by fast
qed
(* This and Hintikka's lemma are the only two where we need semantics. 
   Still, I don't think it's meaningful to separate those two into an extra theory. *)

end