Theory Closedness

(* 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: 29 Sep, 2025
*)

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

definition AtomPredicate where
     "AtomPredicate P X at = (¬ (P X (atom at) ∧ P X (¬. atom at)))"

definition ConstPredicate where 
  "ConstPredicate P X = (¬ P X ⊥. ∧ ¬ P X (¬. ⊤.))"

definition DNegPredicate where
    "DNegPredicate P Q X F = (P X (¬. ¬. F) ⟶ Q X F)"

definition AlphaPredicate where
    "AlphaPredicate P Q X F = (FormulaAlpha F ∧ P X F ⟶ Q X (Comp1 F) (Comp2 F))"

definition BetaPredicate where
    "BetaPredicate P Q X F = (FormulaBeta F ∧ P X F ⟶ Q X (Comp1 F) (Comp2 F))"

definition ClosedPredicate where
    "ClosedPredicate H P QDNeg QAlpha QBeta =
                    ((∀ at. AtomPredicate P H at) ∧
                    (ConstPredicate P H) ∧  
                    (∀F. DNegPredicate P QDNeg H F) ∧
                    (∀F. AlphaPredicate P QAlpha H F) ∧
                    (∀F. BetaPredicate P QBeta H F))"

(* definition consistenceP :: "'b formula set set ⇒ bool" where
    "consistenceP 𝒞 =
       (∀S. S ∈ 𝒞 ⟶ ClosedPredicate S
            (λ S' F . F ∈ S')
            (λ S' F . S' ∪ {F} ∈ 𝒞)
            (λ S' F G . S' ∪ {F, G} ∈ 𝒞)
            (λ S' F G . S' ∪ {F} ∈ 𝒞 ∨ S' ∪ {G} ∈ 𝒞))" *)

locale consistProp = 
fixes 𝒞  :: "'b formula set set"
assumes " (∀S. S ∈ 𝒞 ⟶ ClosedPredicate S
            (λ S' F . F ∈ S')
            (λ S' F . S' ∪ {F} ∈ 𝒞)
            (λ S' F G . S' ∪ {F, G} ∈ 𝒞)
            (λ S' F G . S' ∪ {F} ∈ 𝒞 ∨ S' ∪ {G} ∈ 𝒞))" 

definition consistenceP :: "'b formula set set ⇒ bool" where
  "consistenceP 𝒞 = 
     (∀S. S ∈ 𝒞 ⟶ (∀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}∈𝒞)))"     

lemma consistenceEq : "consistProp C = consistenceP C"
    unfolding consistProp_def consistenceP_def ClosedPredicate_def
    AtomPredicate_def ConstPredicate_def DNegPredicate_def AlphaPredicate_def
    BetaPredicate_def by simp

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

unbundle no trancl_syntax

definition closure_subset :: "'a set set ⇒ 'a set set" (‹_⇧+›[1000] 1000) where
  "𝒞⇧+ = {S. ∃S' ∈ 𝒞. S ⊆ S'}"

lemma closed_subset: "𝒞 ⊆ 𝒞⇧+"
proof -
  { fix S
    assume "S ∈ 𝒞" 
    moreover 
    have "S ⊆ S" by simp
    ultimately
    have "S ∈ 𝒞⇧+"
      by (unfold closure_subset_def, auto) }
  thus ?thesis by auto
qed 

lemma closed_closed: "subset_closed (𝒞⇧+)"
proof -
 { fix S T
   assume "S ∈ 𝒞⇧+" and "T ⊆ S"
   obtain S1 where "S1 ∈ 𝒞" and "S ⊆ S1" using `S ∈ 𝒞⇧+` 
     by (unfold closure_subset_def, auto)
   have "T ⊆ S1" using `T ⊆ S` and `S ⊆ S1`  by simp
   hence "T ∈ 𝒞⇧+" using `S1 ∈ 𝒞` 
     by (unfold closure_subset_def, auto)}
 thus ?thesis by (unfold subset_closed_def, auto) 
qed 

lemma (in consistProp) cond_consistP :
  assumes  "T ∈ 𝒞" and "S ⊆ T"  
  shows "(∀P. ¬(atom P ∈ S ∧ (¬.atom P) ∈ S))"
(*<*) 
proof (rule allI)+  
  fix P 
  show "¬(atom P  ∈ S ∧ (¬.atom P) ∈ S)"
  proof -
    have "¬(atom P ∈ T ∧ (¬.atom P) ∈ T)"
      using AtomPredicate_def ClosedPredicate_def assms(1) consistProp_axioms
          consistProp_def 
      by (metis (lifting))
    thus "¬(atom P ∈ S ∧ (¬.atom P) ∈ S)" using `S ⊆ T` by auto
  qed
qed 
(*>*)

lemma  (in consistProp) cond_consistP2:
  assumes  "T ∈ 𝒞" and "S ⊆ T"   
  shows "⊥. ∉ S ∧ (¬.⊤.)∉ S"
(*<*)
proof -
  have "⊥. ∉ T ∧ (¬.⊤.)∉ T"
  proof -
    have "consistenceP 𝒞"
      using consistProp_axioms consistProp_def
      by (simp add: consistenceEq) 
    then show ?thesis
      by (simp add: ClosedPredicate_def ConstPredicate_def assms(1) consistenceP_def)
  qed 
  thus "⊥. ∉ S ∧ (¬.⊤.)∉ S" using `S ⊆ T` by auto
qed
(*>*)

lemma  (in consistProp) cond_consistP3:
  assumes "T ∈ 𝒞" and "S ⊆ T"   
  shows "∀F. (¬.¬.F) ∈ S ⟶ S ∪ {F} ∈ 𝒞⇧+"
proof(rule allI) 
(*<*)       
  fix F
  show "(¬.¬.F) ∈ S ⟶  S ∪ {F} ∈ 𝒞⇧+"
  proof (rule impI)
    assume "(¬.¬.F) ∈ S"
    hence "(¬.¬.F) ∈ T" using `S ⊆ T` by auto   
    hence "T ∪ {F} ∈ 𝒞" using `T ∈ 𝒞`
    proof -
      have "consistenceP 𝒞"
        using consistProp_axioms consistProp_def
        using consistenceEq by blast 
      then show ?thesis
        by (simp add: ‹¬.¬.F ∈ T› assms(1) consistenceP_def)
    qed
    moreover 
    have "S ∪ {F} ⊆  T ∪ {F}" using `S ⊆ T` by auto
    ultimately   
    show "S ∪ {F} ∈ 𝒞⇧+"
      by (auto simp add: closure_subset_def)
  qed
qed
(*>*)

lemma  (in consistProp) cond_consistP4:
  assumes "T ∈ 𝒞" and "S ⊆ T" 
  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 ∈ T" using `S ⊆ T` by auto 
    hence  "T ∪ {Comp1 F, Comp2 F} ∈ 𝒞"
    proof -
      have "consistenceP 𝒞"
        using consistProp_axioms consistProp_def
        by (simp add: consistenceEq) 
      then show ?thesis
        using ‹F ∈ T› ‹FormulaAlpha F ∧ F ∈ S› assms(1) consistenceP_def by blast
    qed  
    moreover
    have "S ∪ {Comp1 F, Comp2 F} ⊆ T ∪ {Comp1 F, Comp2 F}" 
      using `S ⊆ T` by auto
    ultimately
    show  "S ∪ {Comp1 F, Comp2 F} ∈ 𝒞⇧+" 
      by (auto simp add: closure_subset_def)
  qed
qed
(*>*)
text‹ ›
lemma  (in consistProp) cond_consistP5:
  assumes "T ∈ 𝒞" and "S ⊆ T" 
  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 ∈ T" using `S ⊆ T` by auto 
    hence "T ∪ {Comp1 F} ∈ 𝒞 ∨ T ∪ {Comp2 F} ∈ 𝒞" 
      using `FormulaBeta F` and `T ∈ 𝒞`
    proof -
      show ?thesis
        using ‹F ∈ T› ‹FormulaBeta F› assms(1) consistProp_axioms consistProp_def consistenceEq
              consistenceP_def by fastforce 
    qed
    moreover
    have "S ∪ {Comp1 F} ⊆ T ∪ {Comp1 F}" and "S ∪ {Comp2 F} ⊆ T ∪ {Comp2 F}" 
      using `S ⊆ T` by auto
    ultimately
    show "S ∪ {Comp1 F} ∈ 𝒞⇧+ ∨ S ∪ {Comp2 F} ∈ 𝒞⇧+"
      by(auto simp add: closure_subset_def)
  qed
qed
(*>*)

theorem  (in consistProp) closed_consistenceP:
  shows "consistenceP (𝒞⇧+)"
  by (smt (verit, ccfv_SIG) closure_subset_def consistProp.cond_consistP consistProp.cond_consistP2 consistProp.cond_consistP3
      consistProp.cond_consistP4 consistProp.cond_consistP5 consistProp_axioms consistenceP_def mem_Collect_eq)

(*<*)
end
(*>*)