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

(*<*)
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 ExtensionCharacterFinitoP:
  shows "𝒞 ⊆ 𝒞⁺⁻" 
  and "finite_character (𝒞⁺⁻)" 
  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 (𝒞⁺⁻)" using finite_character by auto
next
  show "consistenceP 𝒞 ⟶ consistenceP (𝒞⁺⁻)"
  proof(rule impI)   
    assume "consistenceP 𝒞"
    hence  "consistenceP (𝒞⁺)" using closed_consistenceP by auto      
    moreover
    have "subset_closed (𝒞⁺)" using  closed_closed by auto  
    ultimately 
    show "consistenceP (𝒞⁺⁻)" using cfinite_consistenceP
      by auto
  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 and ExtensionCharacterFinitoP by auto
  moreover   
  have "finite_character (𝒞⁺⁻)" using ExtensionCharacterFinitoP by auto
  moreover
  have "S ∈ 𝒞⁺⁻"
    using h2 and ExtensionCharacterFinitoP by auto    
  ultimately
  show "S ⊆ MsucP S (𝒞⁺⁻) g" 
    and "maximal (MsucP S (𝒞⁺⁻) g) (𝒞⁺⁻)" 
    and "MsucP S (𝒞⁺⁻) g ∈ 𝒞⁺⁻"
    using h ConsistentExtensionP[of "𝒞⁺⁻"] by auto
qed
  

theorem HintikkaP:  
  assumes h0:"enumeration g" and h1: "consistenceP 𝒞" and h2: "S ∈ 𝒞"
  shows "hintikkaP (MsucP S (𝒞⁺⁻) g)"
proof -
  have 1: "consistenceP (𝒞⁺⁻)" 
  using h1 ExtensionCharacterFinitoP by auto
  have 2: "subset_closed (𝒞⁺⁻)"
  proof -
    have "finite_character (𝒞⁺⁻)" 
      using ExtensionCharacterFinitoP by auto 
    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 and 2 and 3 and 4 and MaximalHintikkaP[of "𝒞⁺⁻"] by simp 
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 = Ttrue" 
proof (rule ModeloHintikkaPa)     
  show "hintikkaP (MsucP S (𝒞⁺⁻) g)"
    using h0 and h1 and h2 by(rule HintikkaP)
next
  show "F ∈ MsucP S (𝒞⁺⁻) g"
    using h3  Max_subsetuntoP by auto  
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 = Ttrue" 
      using g h2 h3 ExistenceModelP hip by blast }
  hence "∀F∈S. t_v_evaluation (IH (MsucP S (𝒞⁺⁻) g)) F = Ttrue" 
    by (rule ballI)
  hence "∃ I. ∀ F ∈ S. t_v_evaluation I F = Ttrue" 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
(*>*)