Theory MaximalHintikka

(* 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  *)

(*<*)
theory MaximalHintikka
imports HintikkaTheory   
begin
(*>*)

section    ‹Maximal Hintikka  ›
text   ‹This theory formalises maximality of Hintikka sets according to Smullyan's textbook \cite{Smullyan}. Specifically, following \cite{Fitting} (page 55) this theory formalises 
the fact that if $\mathcal {C}$ is a propositional consistence property closed by subsets, and $M$ 
a maximal set belonging to $\mathcal{C}$ then $M$ is a Hintikka set.
› 


lemma ext_hintikkaP1:
  assumes  hip1: "consistenceP 𝒞" and hip2: "M ∈ 𝒞"
  shows   "∀p. ¬ (atom p ∈ M ∧ (¬.atom p) ∈ M)"
(*<*)
proof -
  show ?thesis using hip1 hip2 by(unfold consistenceP_def) simp 
qed
(*>*)

text ‹ ›

lemma ext_hintikkaP2: 
  assumes hip1: "consistenceP 𝒞" and hip2: "M ∈ 𝒞"  
  shows "FF ∉ M"
(*<*)
proof -
  show ?thesis using hip1 hip2 by(unfold consistenceP_def) simp 
qed
(*>*)

text ‹ ›

lemma ext_hintikkaP3:
  assumes  hip1: "consistenceP 𝒞" and hip2: "M ∈ 𝒞"  
  shows "(¬.TT) ∉ M"
(*<*)
proof -
  show ?thesis using hip1 hip2 by(unfold consistenceP_def) simp
qed
(*>*)

text ‹ ›

lemma ext_hintikkaP4:
  assumes  hip1: "consistenceP 𝒞" and hip2: "maximal M 𝒞" and hip3: "M ∈ 𝒞"  
  shows "∀F. (¬.¬.F) ∈ M ⟶ F ∈ M" 
(*<*)
proof (rule allI impI)+  
  fix F 
  assume h1: "(¬.¬.F) ∈ M"
  show "F ∈ M"
  proof -   
    have "(¬.¬.F) ∈ M ⟶ M ∪ {F} ∈ 𝒞"
      using hip1 hip3 by (unfold consistenceP_def) simp    
    hence "M ∪ {F} ∈ 𝒞" using h1 by simp  
    moreover 
    have  "∀M'∈𝒞. M ⊆ M' ⟶ M = M'" using hip2 by (unfold maximal_def)
    moreover
    have "M ⊆ M ∪ {F}" by auto
    ultimately
    have "M = M ∪ {F}" by auto 
    thus "F ∈ M" by auto
  qed
qed
(*>*)

text ‹ ›

lemma ext_hintikkaP5:
  assumes hip1: "consistenceP 𝒞" and hip2: "maximal M 𝒞" and hip3: "M ∈ 𝒞"  
  shows "∀F. (FormulaAlfa F) ∧ F ∈ M ⟶ (Comp1 F ∈ M ∧ Comp2 F ∈ M)"
(*<*)      
proof (rule allI impI)+  
  fix F 
  assume h1: "(FormulaAlfa F) ∧ F ∈ M"
  show "Comp1 F ∈ M ∧ Comp2 F ∈ M"
  proof -
    have "(FormulaAlfa F) ∧ F ∈ M ⟶ M ∪ {Comp1 F, Comp2 F} ∈ 𝒞"
      using hip1 hip3 by (unfold consistenceP_def) simp
    hence  "M ∪ {Comp1 F, Comp2 F} ∈ 𝒞" using h1 by simp
    moreover
    have "∀M'∈𝒞. M ⊆ M' ⟶ M = M'" using hip2 by (unfold maximal_def) 
    moreover
    have "M ⊆ M ∪ {Comp1 F, Comp2 F}" by auto
    ultimately     
    have "M = M ∪ {Comp1 F, Comp2 F}"  by simp     
    thus "Comp1 F ∈ M ∧ Comp2 F ∈ M" by auto
  qed
qed
(*>*)

text ‹ ›

lemma ext_hintikkaP6:
  assumes hip1: "consistenceP 𝒞" and hip2: "maximal M 𝒞" and  hip3: "M ∈ 𝒞"  
  shows "∀F. (FormulaBeta F) ∧ F ∈ M ⟶ Comp1 F ∈ M ∨ Comp2 F ∈ M" 
(*<*)     
proof (rule allI impI)+  
  fix F 
  assume h1: "(FormulaBeta F) ∧ F ∈ M"
  show "Comp1 F ∈ M ∨ Comp2 F ∈ M"
  proof -    
    have "(FormulaBeta F) ∧ F ∈ M ⟶ M ∪ {Comp1 F} ∈ 𝒞 ∨ M ∪ {Comp2 F} ∈ 𝒞"
      using hip1 hip3 by (unfold consistenceP_def) simp
    hence  "M ∪ {Comp1 F} ∈ 𝒞 ∨ M ∪ {Comp2 F} ∈ 𝒞" using h1 by simp
    thus ?thesis
    proof (rule disjE)
      assume "M ∪ {Comp1 F} ∈ 𝒞"
      moreover  
      have "∀M'∈𝒞. M ⊆ M' ⟶ M = M'" using hip2 by (unfold maximal_def)
      moreover
      have "M ⊆ M ∪ {Comp1 F}" by auto
      ultimately
      have "M = M ∪ {Comp1 F}" by simp
      hence "Comp1 F ∈ M" by auto
      thus "Comp1 F ∈ M ∨ Comp2 F ∈ M" by simp
    next 
      assume "M ∪ {Comp2 F} ∈ 𝒞"
      moreover  
      have "∀M'∈𝒞. M ⊆ M' ⟶ M = M'" using hip2 by (unfold maximal_def)
      moreover
      have "M ⊆ M ∪ {Comp2 F}" by auto
      ultimately
      have "M = M ∪ {Comp2 F}" by simp
      hence "Comp2 F ∈ M" by auto
      thus "Comp1 F ∈ M ∨ Comp2 F ∈ M" by simp
    qed
  qed
qed
(*>*)


theorem MaximalHintikkaP:
  assumes hip1: "consistenceP 𝒞" and hip2: "maximal M 𝒞" and  hip3: "M ∈ 𝒞"
  shows "hintikkaP M"
proof (unfold hintikkaP_def)     
  show "(∀P. ¬ (atom P ∈ M ∧ ¬.atom P ∈ M)) ∧
        FF ∉ M ∧
        ¬.TT ∉ M ∧
        (∀F. ¬.¬.F ∈ M ⟶ F ∈ M) ∧
        (∀F. FormulaAlfa F ∧ F ∈ M ⟶ Comp1 F ∈ M ∧ Comp2 F ∈ M) ∧
        (∀F. FormulaBeta F ∧ F ∈ M ⟶ Comp1 F ∈ M ∨ Comp2 F ∈ M)"
    using ext_hintikkaP1[OF hip1 hip3] 
          ext_hintikkaP2[OF hip1 hip3] 
          ext_hintikkaP3[OF hip1 hip3] 
          ext_hintikkaP4[OF hip1 hip2 hip3]
          ext_hintikkaP5[OF hip1 hip2 hip3] 
          ext_hintikkaP6[OF hip1 hip2 hip3]         
    by blast
qed   
   
(*<*)         
end
(*<*)