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;
   Last modified: 29 Sep, 2025
  *)

(*<*)
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   (in consistProp) ext_HintikkaP1:
  assumes   hip: "M ∈ 𝒞"
  shows   "∀p. ¬ (atom p ∈ M ∧ (¬.atom p) ∈ M)"
(*<*)
proof -
  show ?thesis using hip by (simp add: cond_consistP)  
qed
(*>*)

text ‹ ›

lemma  (in consistProp) ext_HintikkaP2: 
  assumes hip: "M ∈ 𝒞"  
  shows "⊥. ∉ M"
(*<*)
proof -
  show ?thesis using hip by (simp add: cond_consistP2) 
qed
(*>*)

text ‹ ›

lemma  (in consistProp) ext_HintikkaP3:
  assumes  hip: "M ∈ 𝒞"  
  shows "(¬.⊤.) ∉ M"
(*<*)
proof -
  show ?thesis using hip by (simp add: cond_consistP2)
qed
(*>*)

text ‹ ›

lemma  (in consistProp) ext_HintikkaP4:
  assumes  hip1: "maximal M 𝒞" and hip2: "M ∈ 𝒞"  
  shows "∀F. (¬.¬.F) ∈ M ⟶ F ∈ M"
 (* by (metis (no_types, opaque_lifting) Un_insert_right consistProp_axioms consistProp_def consistenceEq
      consistenceP1_def hip1 hip2 insertI1 maximal_def subset_insertI sup_bot.right_neutral) *)
(*<*)
proof (rule allI impI)+  
  fix F 
  assume h1: "(¬.¬.F) ∈ M"
  show "F ∈ M"
  proof -   
    have "(¬.¬.F) ∈ M ⟶ M ∪ {F} ∈ 𝒞"
    proof -
      have "consistenceP 𝒞"
        using consistProp_axioms consistProp_def consistenceEq by blast  
      then show ?thesis
        by (simp add: consistenceEq consistenceP_def hip2)
    qed
    hence "M ∪ {F} ∈ 𝒞" using h1 by simp  
    moreover 
    have  "∀ M'∈ 𝒞. M ⊆ M' ⟶ M = M'" using hip1 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. (FormulaAlpha F) ∧ F ∈ M ⟶ (Comp1 F ∈ M ∧ Comp2 F ∈ M)"
(*<*)      
proof (rule allI impI)+  
  fix F 
  assume h1: "(FormulaAlpha F) ∧ F ∈ M"
  show "Comp1 F ∈ M ∧ Comp2 F ∈ M"
  proof -
    have "(FormulaAlpha F) ∧ F ∈ M ⟶ M ∪ {Comp1 F, Comp2 F} ∈ 𝒞"
      using hip1 hip3 consistenceEq consistenceP_def by auto
    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 (simp add: consistenceEq consistenceP_def) 
    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  (in consistProp) MaximalHintikkaP:
  assumes  hip1: "maximal M 𝒞" and  hip2: "M ∈ 𝒞"
  shows "HintikkaP M"
(*  by (metis consistProp_axioms consistProp_def ext_HintikkaP1 ext_HintikkaP2 ext_HintikkaP3
      ext_HintikkaP4 ext_HintikkaP5 ext_HintikkaP6 HintikkaEq HintikkaP1_def hip1 hip2)*)
proof-
  have "(∀P. ¬ (atom P ∈ M ∧ ¬.atom P ∈ M)) ∧
        ⊥. ∉ M ∧
        ¬.⊤. ∉ M ∧
        (∀F. ¬.¬.F ∈ M ⟶ F ∈ M) ∧
        (∀F. FormulaAlpha F ∧ F ∈ M ⟶ Comp1 F ∈ M ∧ Comp2 F ∈ M) ∧
        (∀F. FormulaBeta F ∧ F ∈ M ⟶ Comp1 F ∈ M ∨ Comp2 F ∈ M)"
    by (meson consistProp_axioms consistenceEq ext_HintikkaP1 ext_HintikkaP2 ext_HintikkaP3 
        ext_HintikkaP4 ext_HintikkaP5 ext_HintikkaP6 hip1 hip2)
  thus ?thesis
    using HintikkaEq HintikkaP_def by auto
qed   
  
(*<*)         
end
(*>*)