Theory ModelExistence

(* 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 ModelExistence
imports FormulaEnumeration
begin
(*>*)
section    ‹ Model Existence Theorem  ›

text   ‹ This theory formalises the Model Existence Theorem according to Smullyan's textbook \cite{Smullyan} as presented by Fitting in \cite{Fitting}.  ›


theorem  ExtensionCharacterFiniteP:
  shows "𝒞 ⊆ 𝒞⇧⁺⇧^-" 
  and "finite_character_property (𝒞⇧⁺⇧^-)" 
  and "consistenceP 𝒞 ⟶ consistenceP (𝒞⇧⁺⇧^-)"  
proof -  
show "𝒞 ⊆ 𝒞⇧⁺⇧^-"
  proof -
    have "𝒞 ⊆ 𝒞⇧⁺" using closed_subset by auto    
    also
    have "... ⊆ 𝒞⇧⁺⇧^-"
    proof -
      have "subset_closed (𝒞⇧⁺)" using closed_closed by auto     
      thus ?thesis using finite_character_subset  by auto
    qed
    finally show ?thesis by simp
  qed
next
  show "finite_character_property (𝒞⇧⁺⇧^-)" using finite_character by auto
next
  show "consistenceP 𝒞 ⟶ consistenceP (𝒞⇧⁺⇧^-)"
  proof -
    have "∀F. subset_closed (F::'a formula set set)⇧⁺"
      by (simp add: closed_closed)
    then show ?thesis
      by (simp add: consistProp.cfinite_consistenceP consistProp.closed_consistenceP consistenceEq)
  qed 
qed
 
lemma ExtensionConsistenteP1:
  assumes h: "enumeration g"
  and h1: "consistenceP 𝒞" 
  and h2: "S ∈ 𝒞" 
  shows "S ⊆ MsucP S (𝒞⇧⁺⇧^-) g" 
  and "maximal (MsucP S (𝒞⇧⁺⇧^-)  g) (𝒞⇧⁺⇧^-)" 
  and "MsucP S  (𝒞⇧⁺⇧^-)  g ∈ 𝒞⇧⁺⇧^-" 

proof -  
  have "consistenceP (𝒞⇧⁺⇧^-)"
    using h1 closed_closed consistProp.cfinite_consistenceP consistProp.closed_consistenceP consistenceEq by blast
  moreover   
  have "finite_character_property (𝒞⇧⁺⇧^-)"
    by (simp add: finite_character)
  moreover
  have "S ∈ 𝒞⇧⁺⇧^-"
    using h2  closed_closed closed_subset finite_character_subset h2 by blast 
  ultimately
  show "S ⊆ MsucP S (𝒞⇧⁺⇧^-) g" 
    and "maximal (MsucP S (𝒞⇧⁺⇧^-) g) (𝒞⇧⁺⇧^-)" 
    and "MsucP S (𝒞⇧⁺⇧^-) g ∈ 𝒞⇧⁺⇧^-"
    using h ConsistentExtensionP[of "𝒞⇧⁺⇧^-"] by auto
qed
  
theorem  Hintikka:  
  assumes h0:"enumeration g" and h1: "consistenceP 𝒞" and h2: "S ∈ 𝒞"
  shows "HintikkaP (MsucP S (𝒞⇧⁺⇧^-) g)"
(*  using ExtensionCharacterFinitoP(3) ExtensionConsistenteP1(2,3) consistProp.MaximalHintikkaP
    consistProp.intro h0 h1 h2 by blast *)
proof -
  have 1: "consistenceP (𝒞⇧⁺⇧^-)" 
  using h1
  using closed_closed consistProp.cfinite_consistenceP consistProp.closed_consistenceP consistenceEq by blast
  have 2: "subset_closed (𝒞⇧⁺⇧^-)"
  proof -
    have "finite_character_property (𝒞⇧⁺⇧^-)" 
      using finite_character by blast  
    thus "subset_closed (𝒞⇧⁺⇧^-)" by (rule finite_character_closed)
  qed 
  have 3: "maximal (MsucP S (𝒞⇧⁺⇧^-) g) (𝒞⇧⁺⇧^-)" 
    and 4: "MsucP S (𝒞⇧⁺⇧^-) g ∈ 𝒞⇧⁺⇧^-" 
    using ExtensionConsistenteP1[OF h0 h1 h2] by auto
  show ?thesis
    using "1" "3" "4" consistProp.MaximalHintikkaP consistProp.intro consistenceEq by blast  
qed 


theorem  ExistenceModelP:
  assumes h0: "enumeration g"
  and h1: "consistenceP 𝒞" 
  and h2: "S ∈ 𝒞" 
  and h3: "F ∈ S"
  shows "t_v_evaluation (IH (MsucP S (𝒞⇧⁺⇧^-) g)) F" 
proof- (*rule ModelHintikkaPa*)     
  have 1: "HintikkaProp (MsucP S (𝒞⇧⁺⇧^-) g)"
    using h0 and h1 and h2 Hintikka HintikkaEq
    by metis
  have 2: "F ∈ MsucP S (𝒞⇧⁺⇧^-) g"
    using h3  Max_subsetuntoP by auto 
  thus ?thesis using "1" "2" HintikkaProp.ModelHintikkaP
                      HintikkaEq model_def by blast
qed

theorem Theo_ExistenceModels:
  assumes h1: "∃g. enumeration (g:: nat ⇒ 'b formula)"  
  and h2: "consistenceP 𝒞" 
  and h3: "(S:: 'b formula set) ∈ 𝒞"
  shows "satisfiable S"
proof -
  obtain g where g: "enumeration (g:: nat ⇒ 'b formula)" 
    using h1 by auto
  { fix F
    assume hip: "F ∈ S"
    have  "t_v_evaluation (IH (MsucP S (𝒞⇧⁺⇧^-) g)) F" 
      using g h2 h3 ExistenceModelP hip by blast }
  hence "∀F∈S. t_v_evaluation (IH (MsucP S (𝒞⇧⁺⇧^-) g)) F" 
    by (rule ballI)
  hence "∃ I. ∀ F ∈ S. t_v_evaluation I F" by auto
  thus "satisfiable S" by(unfold satisfiable_def, unfold model_def)
qed 

corollary Satisfiable_SetP1:
  assumes h0:  "∃g. enumeration (g:: nat ⇒ 'b)"
  and h1: "consistenceP 𝒞"
  and h2: "(S:: 'b formula set) ∈ 𝒞"
  shows "satisfiable S"
proof -
  obtain g where g: "enumeration (g:: nat ⇒ 'b )" 
    using h0 by auto
  have "enumeration ((ΔP g):: nat ⇒ 'b formula)" using g  EnumerationFormulasP1 by auto
  hence  h'0: "∃g. enumeration (g:: nat ⇒ 'b formula)" by auto
  show ?thesis using Theo_ExistenceModels[OF h'0 h1 h2] by auto
qed

corollary Satisfiable_SetP2:
  assumes "consistenceP 𝒞" and "(S:: nat formula set) ∈ 𝒞"
  shows "satisfiable S"
  using  enum_nat assms Satisfiable_SetP1 by auto 
(*<*)
end
(*>*)