Theory FinitenessClosedCharProp

(* Formalization adapted from: 
   Fabián Fernando Serrano Suárez, "Formalización en Isar de la
   Meta-Lógica de Primer Orden." PhD thesis, 
   Departamento de Ciencias de la Computación e Inteligencia Artificial,
   Universidad de Sevilla, Spain, 2012.
   https://idus.us.es/handle/11441/57780.  In Spanish 
   Last modified: 11 Aug, 2025
 *)


(*<*)
theory FinitenessClosedCharProp 
imports Closedness 
begin
(*>*)

section  ‹ Finiteness Character Property  ›

text  ‹ This theory formalises the theorem that states that subset closed propositional consistency properties can be extended to satisfy the finite character property. 

The proof is by induction on the structure of propositional formulas based on the analysis of cases for the possible different types of formula in the sets of the collection of sets that hold the propositional consistency property. 
  ›

definition finite_character_property :: "'a set set ⇒ bool" where
  "finite_character_property 𝒞 = (∀S. S ∈ 𝒞 = (∀S'. finite S' ⟶ S' ⊆ S ⟶ S' ∈ 𝒞))"

theorem finite_character_closed: 
  assumes "finite_character_property 𝒞"
  shows "subset_closed 𝒞"
proof -  
  { fix S T
    assume "S ∈ 𝒞" and  "T ⊆ S"
    have "T ∈ 𝒞" using "finite_character_property_def"
    proof -
      { fix U             
        assume "finite U" and "U ⊆ T"
        have "U ∈ 𝒞"
        proof -
          have "U ⊆ S" using `U ⊆ T` and `T ⊆ S` by simp
          thus "U ∈ 𝒞" using `S ∈ 𝒞` and `finite U` and assms 
            by (unfold finite_character_property_def) blast
        qed} 
      thus ?thesis using assms by(unfold finite_character_property_def) blast
    qed }
  thus ?thesis  by(unfold  subset_closed_def) blast
qed     
    
definition closure_cfinite :: "'a set set ⇒ 'a set set" (‹_⇧-› [1000] 999) where
  "𝒞⇧- = {S. ∀S'. S' ⊆ S ⟶ finite S' ⟶ S' ∈ 𝒞}"

lemma finite_character_subset:
  assumes "subset_closed 𝒞"
  shows "𝒞 ⊆ 𝒞⇧-"
proof -
  { fix S
    assume "S ∈ 𝒞"
    have "S ∈ 𝒞⇧-" 
    proof -
      { fix S'
        assume "S' ⊆ S" and "finite S'"
        hence "S' ∈ 𝒞" using  `subset_closed 𝒞` and `S ∈ 𝒞`
          by (simp add: subset_closed_def)}
      thus ?thesis by (simp add: closure_cfinite_def) 
    qed}
  thus ?thesis by auto
qed

lemma finite_character: "finite_character_property (𝒞⇧-)"
proof (unfold finite_character_property_def)
  show "∀S. (S ∈ 𝒞⇧-) = (∀S'. finite S' ⟶ S' ⊆ S ⟶ S' ∈ 𝒞⇧-)"
  proof
    fix  S
    { assume  "S ∈ 𝒞⇧-"
      hence "∀S'. finite S' ⟶ S' ⊆ S ⟶ S' ∈ 𝒞⇧-" 
        by(simp add: closure_cfinite_def)} 
    moreover
    { assume "∀S'. finite S' ⟶ S' ⊆ S ⟶ S' ∈ 𝒞⇧-"
      hence  "S ∈ 𝒞⇧-" by(simp add: closure_cfinite_def)}
    ultimately
    show "(S ∈ 𝒞⇧-) = (∀S'. finite S' ⟶ S' ⊆ S ⟶ S' ∈ 𝒞⇧-)"
      by blast
  qed
qed
 
lemma  (in consistProp) cond_characterP1:
  assumes "subset_closed 𝒞" 
  and hip: "∀S'⊆S. finite S' ⟶ S' ∈ 𝒞"
  shows "(∀P. ¬(atom P ∈ S ∧ (¬.atom P) ∈ S))"
(*<*)
proof (rule allI)+  
  fix P t
  show "¬(atom P  ∈ S ∧ (¬.atom P) ∈ S)"
  proof (rule notI)
    assume "atom P ∈ S ∧ (¬.atom P) ∈ S"
    hence "{atom P , ¬.atom P} ⊆ S" by simp
    hence "{atom P, ¬.atom P} ∈ 𝒞" using hip by simp
    moreover
    have "∀S. S ∈ 𝒞 ⟶ (∀P ts. ¬(atom P ∈ S ∧ (¬.atom P) ∈ S))"
      by (simp add: cond_consistP)
    ultimately
    have "¬(atom P ∈ {atom P , ¬.atom P} ∧ 
          (¬.atom P) ∈ {atom P, ¬.atom P})"
      by auto 
    thus False by simp
  qed
qed  
(*>*)

lemma  (in consistProp) cond_characterP2:
  assumes  "subset_closed 𝒞" 
  and hip: "∀S'⊆S. finite S' ⟶ S' ∈ 𝒞"
  shows "⊥. ∉ S ∧ (¬.⊤.)∉ S"
(*<*)
proof -
  have "⊥. ∉ S"
  proof(rule notI)
    assume "⊥. ∈ S"
    hence "{⊥.} ⊆ S" by simp
    hence "{⊥.}∈ 𝒞" using hip by simp
    moreover
    have "∀S. S ∈ 𝒞 ⟶ ⊥. ∉ S" 
      by (simp add: cond_consistP2) 
    ultimately 
    have "⊥. ∉ {⊥.}" by auto    
    thus False by simp
  qed   
  moreover
  have "(¬.⊤.)∉ S"
  proof(rule notI)    
    assume "(¬.⊤.) ∈ S"
    hence "{¬.⊤.} ⊆ S" by simp
    hence "{¬.⊤.}∈ 𝒞" using hip by simp
    moreover
    have "∀S. S ∈ 𝒞 ⟶ (¬.⊤.) ∉ S" using cond_consistP2 by blast 
    ultimately 
    have "(¬.⊤.) ∉ {(¬.⊤.)}" by auto    
    thus False by simp
  qed
  ultimately show ?thesis by simp   
qed   
(*>*)
text‹ ›
lemma  (in consistProp) cond_characterP3:
  assumes  "subset_closed 𝒞" 
  and hip: "∀S'⊆S. finite S' ⟶ S' ∈ 𝒞"
  shows "∀F. (¬.¬.F) ∈ S ⟶  S ∪ {F} ∈ 𝒞⇧-"
(*<*)
proof (rule allI)        
  fix F
  show "(¬.¬.F) ∈ S ⟶  S ∪ {F} ∈ 𝒞⇧-"
  proof (rule impI)
    assume "(¬.¬.F) ∈ S"
    show "S ∪ {F} ∈ 𝒞⇧-"  
    proof (unfold closure_cfinite_def)
      show "S ∪ {F} ∈ {S. ∀S'⊆S. finite S' ⟶ S' ∈ 𝒞}"
      proof (rule allI impI CollectI)+
        fix S'
        assume "S' ⊆ S ∪ {F}" and "finite S'"  
        show "S' ∈ 𝒞"
        proof -          
          have "S' - {F} ∪ {¬.¬.F}  ⊆ S"  
            using `(¬.¬.F) ∈ S` and  `S'⊆ S ∪ {F}` by auto 
          moreover
          have 1: "finite (S' - {F} ∪ {¬.¬.F})" using `finite S'` by auto
          ultimately
          have "(S' - {F} ∪ {¬.¬.F}) ∈ 𝒞" using hip  by simp
          moreover
          have "(¬.¬.F) ∈ (S' - {F} ∪ {¬.¬.F})" by simp
          ultimately  
          have "(S' - {F} ∪ {¬.¬.F})∪ {F} ∈ 𝒞"
          proof -
            show ?thesis
              using ‹S' - {F} ∪ {¬.¬.F} ∈ 𝒞› consistProp_axioms consistProp_def consistenceEq consistenceP_def by fastforce
          qed
          moreover
          have "(S' - {F} ∪ {¬.¬.F})∪ {F} = (S' ∪ {¬.¬.F})∪ {F}"
            by auto
          ultimately 
          have "(S' ∪ {¬.¬.F})∪ {F} ∈ 𝒞" by simp
          moreover
          have  "S' ⊆ (S' ∪ {¬.¬.F})∪ {F}" by auto
          ultimately
          show "S'∈ 𝒞" using `subset_closed 𝒞` 
            by (simp add: subset_closed_def)
        qed
      qed
    qed
  qed
qed     
(*>*)

lemma cond_characterP4:
  assumes "consistenceP 𝒞" 
  and "subset_closed 𝒞" 
  and hip: "∀S'⊆S. finite S' ⟶ S' ∈ 𝒞"
  shows "(∀F. ((FormulaAlpha F) ∧ F ∈ S) ⟶ (S ∪ {Comp1 F, Comp2 F}) ∈ 𝒞⇧-)"
(*<*) 
proof (rule allI) 
  fix F 
  show "((FormulaAlpha F) ∧ F ∈ S) ⟶ S ∪ {Comp1 F, Comp2 F} ∈ 𝒞⇧-"
  proof (rule impI)
    assume "(FormulaAlpha F) ∧ F ∈ S"
    hence "(FormulaAlpha F)" and "F ∈ S" by auto
    show "S ∪ {Comp1 F, Comp2 F} ∈ 𝒞⇧-"  
    proof (unfold closure_cfinite_def)
      show "S ∪ {Comp1 F, Comp2 F} ∈ {S. ∀S'⊆S. finite S' ⟶ S' ∈ 𝒞}"
      proof (rule allI impI CollectI)+
        fix S'
        assume "S' ⊆ S ∪ {Comp1 F, Comp2 F}"  and  "finite S'"  
        show "S' ∈ 𝒞"
        proof -          
          have "S' - {Comp1 F, Comp2 F} ∪ {F}  ⊆ S"  
            using `F ∈ S` and  `S'⊆ S ∪ {Comp1 F, Comp2 F}` by auto 
          moreover
          have "finite (S' - {Comp1 F, Comp2 F} ∪ {F})" 
            using `finite S'` by auto
          ultimately
          have "(S' - {Comp1 F, Comp2 F} ∪ {F}) ∈ 𝒞" using hip  by simp
          moreover
          have "F ∈ (S' - {Comp1 F, Comp2 F} ∪ {F})" by simp
          ultimately  
          have "(S' - {Comp1 F, Comp2 F} ∪ {F}) ∪ {Comp1 F, Comp2 F} ∈ 𝒞" 
            using `consistenceP 𝒞` `FormulaAlpha F`  consistenceP_def
            by metis            
          moreover
          have "(S' - {Comp1 F, Comp2 F} ∪ {F}) ∪ {Comp1 F, Comp2 F} = 
                (S' ∪ {F}) ∪ {Comp1 F, Comp2 F}"
            by auto
          ultimately 
          have "(S' ∪ {F}) ∪ {Comp1 F, Comp2 F} ∈ 𝒞" by simp
          moreover
          have "S' ⊆ (S' ∪ {F}) ∪ {Comp1 F, Comp2 F}" by auto
          ultimately
          show "S'∈ 𝒞" using `subset_closed 𝒞` 
            by (simp add: subset_closed_def)
        qed
      qed
    qed
  qed
qed     
(*>*)

lemma cond_characterP5:
  assumes "consistenceP 𝒞" 
  and "subset_closed 𝒞" 
  and hip: "∀S'⊆S. finite S' ⟶ S' ∈ 𝒞"
  shows "∀F. FormulaBeta F ∧ F ∈ S ⟶ S ∪ {Comp1 F} ∈ 𝒞⇧- ∨ S ∪ {Comp2 F} ∈ 𝒞⇧-"
(*<*)
proof (rule allI) 
  fix F 
  show "FormulaBeta F ∧ F ∈ S ⟶ S ∪ {Comp1 F} ∈ 𝒞⇧- ∨ S ∪ {Comp2 F} ∈ 𝒞⇧-"
  proof (rule impI)
    assume "(FormulaBeta F) ∧ F ∈ S" 
    hence "FormulaBeta F" and "F ∈ S" by auto 
    show "S ∪ {Comp1 F} ∈ 𝒞⇧- ∨ S ∪ {Comp2 F} ∈ 𝒞⇧-"
    proof (rule ccontr)
      assume "¬(S ∪ {Comp1 F} ∈ 𝒞⇧- ∨ S ∪ {Comp2 F} ∈ 𝒞⇧-)"
      hence "S ∪ {Comp1 F} ∉ 𝒞⇧- ∧ S ∪ {Comp2 F} ∉ 𝒞⇧-" by simp    
      hence 1: "∃ S1. (S1 ⊆ S ∪ {Comp1 F} ∧ finite S1 ∧ S1 ∉ 𝒞)" 
        and 2: "∃ S2. (S2 ⊆ S ∪ {Comp2 F} ∧ finite S2 ∧ S2 ∉ 𝒞)"
        by (auto simp add: closure_cfinite_def) 
      obtain S1  where S1: "S1 ⊆ S ∪ {Comp1 F} ∧ finite S1 ∧ S1 ∉ 𝒞" 
        using 1 by auto
      obtain S2 where  S2: "S2 ⊆ S ∪ {Comp2 F} ∧ finite S2 ∧ S2 ∉ 𝒞" 
        using 2 by auto         
      have "(S1-{Comp1 F}) ∪ (S2-{Comp2 F}) ∪ {F} ⊆ S"
        using `F ∈ S` S1 S2 by auto
      moreover
      have "finite ((S1-{Comp1 F}) ∪ (S2-{Comp2 F}) ∪ {F})" 
        using S1 and S2 by simp
      ultimately
      have "(S1-{Comp1 F}) ∪ (S2-{Comp2 F}) ∪ {F} ∈ 𝒞" using hip by simp
      moreover
      have "F ∈ (S1-{Comp1 F}) ∪ (S2-{Comp2 F}) ∪ {F}" by simp    
      ultimately 
      have 3: "((S1-{Comp1 F}) ∪ (S2-{Comp2 F}) ∪ {F} ∪ {Comp1 F}) ∈ 𝒞 ∨ 
               ((S1-{Comp1 F}) ∪ (S2-{Comp2 F}) ∪ {F} ∪ {Comp2 F}) ∈ 𝒞"
        using `consistenceP 𝒞` `FormulaBeta F`  consistenceP_def
        by metis   
      hence "S1 ∈ 𝒞 ∨ S2 ∈ 𝒞"
      proof (cases)
        assume "((S1-{Comp1 F}) ∪ (S2-{Comp2 F}) ∪ {F} ∪ {Comp1 F}) ∈ 𝒞"
        moreover
        have "S1 ⊆ ((S1-{Comp1 F}) ∪ (S2-{Comp2 F}) ∪ {F} ∪ {Comp1 F})" 
          by auto       
        ultimately
        have "S1 ∈ 𝒞"  using `subset_closed 𝒞` 
          by (simp add: subset_closed_def) 
        thus ?thesis by simp
      next 
        assume "¬((S1-{Comp1 F}) ∪ (S2-{Comp2 F}) ∪ {F} ∪ {Comp1 F}) ∈ 𝒞"
        hence "((S1-{Comp1 F}) ∪ (S2-{Comp2 F}) ∪ {F} ∪ {Comp2 F}) ∈ 𝒞" 
          using 3 by simp
        moreover
        have "S2 ⊆ ((S1-{Comp1 F}) ∪ (S2-{Comp2 F}) ∪ {F} ∪ {Comp2 F})" 
          by auto       
        ultimately
        have "S2 ∈ 𝒞"  using `subset_closed 𝒞` 
          by (simp add: subset_closed_def) 
        thus ?thesis by simp
      qed
      thus False using S1 and S2 by simp
    qed
  qed
qed
(*>*)

theorem  (in consistProp) cfinite_consistenceP:
  assumes hip1: "subset_closed 𝒞" 
  shows "consistenceP (𝒞⇧-)"
(*  by (smt (verit, del_insts) closure_cfinite_def cond_characterP4 cond_characterP5
      consistProp.cond_characterP1 consistProp.cond_characterP2 consistProp.cond_characterP3
      consistProp_axioms consistProp_def consistenceEq consistenceP1_def hip1 mem_Collect_eq) *)
proof - 
  { fix S
    assume "S ∈ 𝒞⇧-" 
    hence hip2: "∀S'⊆S. finite S' ⟶ S' ∈ 𝒞" 
      by (simp add: closure_cfinite_def) 
    have "(∀P.  ¬(atom P ∈ S ∧ (¬.atom P) ∈ S)) ∧
          ⊥. ∉ S ∧ (¬.⊤.) ∉ S ∧
          (∀F. (¬.¬.F) ∈ S ⟶ S ∪ {F} ∈ 𝒞⇧-) ∧
          (∀F. ((FormulaAlpha F) ∧ F ∈ S) ⟶ (S ∪ {Comp1 F, Comp2 F}) ∈ 𝒞⇧-) ∧
          (∀F. ((FormulaBeta F) ∧ F ∈ S) ⟶ 
               (S ∪ {Comp1 F} ∈ 𝒞⇧-) ∨ (S ∪ {Comp2 F} ∈ 𝒞⇧-))"
      using cond_characterP1 cond_characterP2 cond_characterP3 cond_characterP4 cond_characterP5
        consistProp_axioms consistProp_def hip1 hip2
      by (smt (verit, ccfv_threshold) consistenceEq) 
  }
  thus ?thesis
    using consistenceEq consistenceP_def by blast
qed

(*<*)
end
(*>*)