Theory HintikkaTheory

(* 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  HintikkaTheory
  imports MaximalSet 


begin 
(*>*)
section   ‹ Hintikka Theorem  ›

text ‹
The formalization of Hintikka's lemma is by induction on the structure of the formulas in a Hintikka set $H$ by applying the technical theorem {\tt hintikkaP\_model\_aux}. This theorem applies a series of lemmas to address the evaluation of all possible cases of formulas in $H$. Indeed,   considering the Boolean evaluation $IH$ that maps all propositional letters in $H$ to true and all other letters to false, the most interesting cases of the inductive proof are those related to implicational formulas in $H$ and the negation of arbitrary formulas in $H$. These cases are not straightforward since implicational and negation formulas are not considered in the definition of Hintikka sets. For an implicational formula, say $F_1 \longrightarrow F_2$, it is necessary to prove that if it belongs to $H$, its evaluation by $IH$ is true. Also, whenever  $\neg(F_1 \longrightarrow F_2)$ belongs to $H$ its evaluation is false. The proof is obtained by relating such formulas, respectively, with $\beta$ and $\alpha$ formulas (case P6). The second interesting case is the one related to arbitrary negations. In this case, it is proved that if $\neg F$ belongs to $H$, its evaluation by $IH$ is true, and in the case that $\neg\neg F$ belongs to $H$, its evaluation by $IH$ is also true (Case P7).
›




definition hintikkaP :: "'b formula set ⇒ bool" where 
  "hintikkaP H = ((∀P. ¬ (atom P ∈ H ∧ (¬.atom P) ∈ H)) ∧
                 FF ∉ H ∧ (¬.TT) ∉ H ∧
                 (∀F. (¬.¬.F) ∈ H ⟶ F ∈ H) ∧
                 (∀F. ((FormulaAlfa F) ∧ F ∈ H) ⟶ 
                      ((Comp1 F) ∈ H ∧ (Comp2 F) ∈ H)) ∧
                 (∀F. ((FormulaBeta F) ∧ F ∈ H) ⟶ 
                      ((Comp1 F) ∈ H ∨ (Comp2 F) ∈ H)))"
    

fun IH :: "'b formula set  ⇒ 'b ⇒ v_truth" where
  "IH H P = (if atom P ∈ H then Ttrue else Ffalse)"


(*<*)
primrec f_size :: "'b formula ⇒ nat" where
  "f_size FF = 1"
| "f_size TT = 1"
| "f_size (atom P) = 1" 
| "f_size (¬. F) = (f_size F) + 1" 
| "f_size (F ∧. G) = (f_size F) + (f_size G) + 1"
| "f_size (F ∨. G) = (f_size F) + (f_size G) + 1"             
| "f_size (F →. G) = (f_size F) + (f_size G) + 1"

lemma pf_size: "0 < f_size F"
by (induct F) auto
(*>*)


(*<*)

(*>*)

lemma case_P1:
assumes hip1: "hintikkaP H" and
hip2: "∀G. (G, FF) ∈ measure f_size ⟶
(G ∈ H ⟶ t_v_evaluation (IH H) G = Ttrue) ∧ ((¬.G) ∈ H  ⟶ t_v_evaluation (IH H) (¬.G)= Ttrue)"
shows "(FF ∈ H ⟶ t_v_evaluation (IH H) FF = Ttrue) ∧ ((¬.FF) ∈ H ⟶ t_v_evaluation (IH H) (¬.FF)=Ttrue)" 
(*<*)          
proof(rule conjI)
  show "(FF ∈ H ⟶  t_v_evaluation (IH H) FF = Ttrue)"
  proof -
    have "FF ∉ H" using hip1 by (unfold hintikkaP_def) auto
    thus "FF ∈ H ⟶ t_v_evaluation (IH H) FF = Ttrue" by simp 
  qed 
  next  
  show "(¬.FF) ∈ H ⟶ t_v_evaluation (IH H) (¬.FF)=Ttrue" 
  proof -
    have "t_v_evaluation (IH H) (¬.FF)= Ttrue" by(simp add: v_negation_def)
    thus ?thesis by simp
  qed
qed 
(*>*)
text‹ ›  
lemma case_P2:
assumes hip1: "hintikkaP H" and
hip2: "∀G. (G, TT) ∈ measure f_size ⟶
(G ∈ H ⟶ t_v_evaluation (IH H) G = Ttrue) ∧ ((¬.G) ∈ H  ⟶ t_v_evaluation (IH H) (¬.G)= Ttrue)"                 
shows 
"(TT ∈ H ⟶ t_v_evaluation (IH H) TT = Ttrue) ∧ ((¬.TT) ∈ H ⟶ t_v_evaluation (IH H) (¬.TT)=Ttrue)"
(*<*)  
proof(rule conjI)
  show "TT ∈ H ⟶ t_v_evaluation (IH H) TT = Ttrue"
  by simp
  next
  show "(¬.TT) ∈ H ⟶ t_v_evaluation (IH H) (¬.TT)=Ttrue" 
  proof -         
    have "(¬.TT) ∉ H" using hip1 by (unfold hintikkaP_def) auto
    thus "(¬.TT) ∈ H  ⟶ t_v_evaluation (IH H) (¬.TT)=Ttrue" 
    by simp
  qed
qed
(*>*)
text‹ ›
lemma case_P3:
assumes hip1: "hintikkaP H" and
hip2: "∀G. (G, atom P) ∈ measure f_size ⟶
(G ∈ H ⟶ t_v_evaluation (IH H) G = Ttrue) ∧ ((¬.G) ∈ H  ⟶ t_v_evaluation (IH H) (¬.G)= Ttrue)"     
shows "(atom P ∈ H  ⟶ t_v_evaluation (IH H) (atom P) = Ttrue) ∧
((¬.atom P) ∈ H ⟶ t_v_evaluation (IH H) (¬.atom P) = Ttrue)"
(*<*)
proof(rule conjI)
  show "(atom P)  ∈ H ⟶ t_v_evaluation (IH H) (atom P) = Ttrue" by simp
  next
  show "(¬.atom P) ∈ H ⟶ t_v_evaluation (IH H) (¬.atom P) = Ttrue" 
  proof(rule conjI impI)
    assume h1: "¬.atom P ∈ H"
    show "t_v_evaluation (IH H) (¬.atom P) = Ttrue"    
    proof -
      have "∀p. ¬ (atom p ∈ H ∧ (¬.atom p) ∈ H)"
      using hip1 conjunct1 by(unfold hintikkaP_def)
      hence "atom P ∉ H" using h1 by auto
      hence "t_v_evaluation (IH H) (atom P) = Ffalse" by simp
      thus ?thesis by(simp add: v_negation_def)
    qed
  qed
qed
(*>*)
text‹ ›
lemma case_P4:
assumes hip1: "hintikkaP H" and
hip2: "∀G. (G, F1 ∧. F2) ∈ measure f_size ⟶ 
(G ∈ H ⟶ t_v_evaluation (IH H) G = Ttrue) ∧ ((¬.G) ∈ H  ⟶ t_v_evaluation (IH H) (¬.G) = Ttrue)"   
shows "((F1 ∧. F2) ∈ H ⟶ t_v_evaluation (IH H) (F1 ∧. F2) = Ttrue) ∧
((¬.(F1 ∧. F2)) ∈ H ⟶ t_v_evaluation (IH H) (¬.(F1 ∧. F2)) = Ttrue)"
(*<*)
proof(rule conjI)                               
  show "((F1 ∧. F2) ∈ H ⟶ t_v_evaluation (IH H) (F1 ∧. F2) = Ttrue)"    
  proof(rule conjI impI)
    assume h2: "(F1 ∧. F2) ∈ H" 
    show  "t_v_evaluation (IH H) (F1 ∧. F2) = Ttrue"
    proof - 
      have "FormulaAlfa (F1 ∧. F2)" by simp 
      hence "Comp1 (F1 ∧. F2) ∈ H ∧ Comp2 (F1 ∧. F2) ∈ H"
      using hip1 h2 by(auto simp add: hintikkaP_def)         
      hence "F1 ∈ H" and "F2 ∈ H" by(unfold Comp1_def, unfold Comp2_def, auto)
      moreover     
      have "(F1, F1 ∧. F2) ∈ measure f_size" and
      "(F2, F1 ∧. F2) ∈ measure f_size"
      by auto
      hence "(F1 ∈ H ⟶ t_v_evaluation (IH H) F1 = Ttrue)" and
      "(F2 ∈ H ⟶ t_v_evaluation (IH H) F2 = Ttrue)" 
      using hip2 by auto      
      ultimately
      have "t_v_evaluation (IH H) F1 = Ttrue" and "t_v_evaluation (IH H) F2 = Ttrue"
      by auto
      thus ?thesis by (simp add: v_conjunction_def)      
    qed 
  qed
  next
  show "¬.(F1 ∧. F2) ∈ H ⟶ t_v_evaluation (IH H)  (¬.(F1 ∧. F2)) = Ttrue" 
  proof(rule impI)
    assume h2: "(¬.(F1 ∧. F2)) ∈ H" 
    show "t_v_evaluation (IH H) (¬.(F1 ∧. F2)) = Ttrue"
    proof - 
      have "FormulaBeta (¬.(F1 ∧. F2))" by simp 
      hence "Comp1 (¬.(F1 ∧. F2)) ∈ H ∨ Comp2 (¬.(F1 ∧. F2)) ∈ H"
      using hip1 h2 by(auto simp add: hintikkaP_def)              
      hence "(¬.F1) ∈ H ∨ (¬.F2) ∈ H" by(unfold Comp1_def, unfold Comp2_def, auto)
      thus ?thesis
      proof(rule disjE)
        assume "(¬.F1) ∈ H"
        moreover        
        have "(¬.F1, (F1 ∧. F2)) ∈ measure f_size" using pf_size by simp         
        hence "(¬.F1) ∈ H ⟶ t_v_evaluation (IH H) (¬.F1) = Ttrue" 
        using hip2 by simp    
        ultimately 
        have 1: "t_v_evaluation (IH H) (¬.F1) = Ttrue" by simp       
        hence "t_v_evaluation (IH H) F1 = Ffalse" using NegationValues2 by auto                  
        thus "t_v_evaluation (IH H) (¬.(F1 ∧. F2)) = Ttrue" 
        by (simp add: v_negation_def, simp add: v_conjunction_def)          next  
        assume "(¬.F2) ∈ H"
        moreover 
        have "(¬.F2, (F1 ∧. F2)) ∈ measure f_size" using pf_size by simp
        hence " (¬.F2) ∈ H ⟶ t_v_evaluation (IH H) (¬.F2)= Ttrue" 
        using hip2 by simp    
        ultimately 
        have 1: "t_v_evaluation (IH H) (¬.F2) = Ttrue" by simp
        hence "t_v_evaluation (IH H) F2 = Ffalse" using NegationValues2 by auto          
        thus "t_v_evaluation (IH H) (¬.(F1 ∧. F2)) = Ttrue"
        by (simp add: v_negation_def, simp add: v_conjunction_def)                
      qed 
    qed
  qed
qed
(*>*)
text‹ ›      
lemma case_P5:
assumes hip1: "hintikkaP H" and
hip2: "∀G. (G, F1 ∨. F2) ∈ measure f_size ⟶
(G ∈ H ⟶ t_v_evaluation (IH H) G = Ttrue) ∧ ((¬.G) ∈ H  ⟶ t_v_evaluation (IH H) (¬.G) = Ttrue)"             
shows "((F1 ∨. F2) ∈ H ⟶ t_v_evaluation (IH H) (F1 ∨. F2) = Ttrue) ∧
((¬.(F1 ∨. F2)) ∈ H ⟶ t_v_evaluation (IH H) (¬.(F1 ∨. F2)) = Ttrue)"
(*<*)
proof(rule conjI) 
  show "(F1 ∨. F2) ∈ H ⟶ t_v_evaluation (IH H) (F1 ∨. F2) = Ttrue"
  proof(rule conjI impI)
    assume h2: "(F1  ∨. F2) ∈ H" 
    show "t_v_evaluation (IH H) (F1 ∨. F2) = Ttrue"
    proof -     
      have "FormulaBeta (F1 ∨.F2)" by simp 
      hence "Comp1 (F1 ∨.F2) ∈ H ∨ Comp2 (F1 ∨.F2) ∈ H"
      using hip1 h2 by(auto simp add: hintikkaP_def)              
      hence "F1 ∈ H ∨ F2 ∈ H" by(unfold Comp1_def, unfold Comp2_def, auto)     
      thus ?thesis
      proof(rule disjE)
        assume "F1 ∈ H"
        moreover         
        have "(F1, F1 ∨. F2) ∈ measure f_size" by simp
        hence "(F1 ∈ H ⟶  t_v_evaluation (IH H) F1 = Ttrue)" 
        using hip2 by simp    
        ultimately 
        have "t_v_evaluation (IH H) F1 = Ttrue" by simp
        thus "t_v_evaluation (IH H) (F1 ∨. F2) = Ttrue" by (simp add: v_disjunction_def)   
        next  
        assume "F2 ∈ H"
        moreover        
        have "(F2, (F1 ∨. F2)) ∈ measure f_size" by simp
        hence "F2 ∈ H ⟶  t_v_evaluation (IH H) F2 =Ttrue" 
        using hip2 by simp    
        ultimately 
        have "t_v_evaluation (IH H) F2 = Ttrue" by simp
        thus "t_v_evaluation (IH H) (F1 ∨. F2) = Ttrue" by (simp add: v_disjunction_def)            
      qed 
    qed
  qed
  next
  show "(¬.(F1 ∨. F2)) ∈ H ⟶
  t_v_evaluation (IH H) (¬.(F1 ∨. F2)) = Ttrue"
  proof(rule impI)
    assume h2: "(¬.(F1  ∨. F2)) ∈ H" 
    show "t_v_evaluation (IH H) (¬.(F1  ∨. F2)) = Ttrue"
    proof -
      have "FormulaAlfa(¬.(F1 ∨. F2))" by simp 
      hence "Comp1 (¬.(F1 ∨. F2)) ∈ H ∧ Comp2 (¬.(F1 ∨. F2)) ∈ H"
      using hip1 h2 by(auto simp add: hintikkaP_def)              
      hence "¬.F1 ∈ H ∧ ¬.F2 ∈ H" by(unfold Comp1_def, unfold Comp2_def, auto) 
      hence "(¬.F1) ∈ H" and "(¬.F2) ∈ H" by auto
      moreover     
      have "(¬.F1, F1 ∨. F2) ∈ measure f_size" and
     "(¬.F2, F1 ∨. F2) ∈ measure f_size" using pf_size
      by auto
      hence "((¬.F1) ∈ H ⟶ t_v_evaluation (IH H) (¬.F1) = Ttrue)" and
           "((¬.F2) ∈ H ⟶ t_v_evaluation (IH H) (¬.F2) = Ttrue)" 
      using hip2 by auto      
      ultimately
      have 1: "t_v_evaluation (IH H) (¬.F1) = Ttrue" and
           2: "t_v_evaluation (IH H) (¬.F2) = Ttrue" by auto
      have "t_v_evaluation (IH H) F1 = Ffalse" using 1 NegationValues2 by auto              
      moreover
      have "t_v_evaluation (IH H) F2 = Ffalse" using 2 NegationValues2 by auto      
      ultimately   
      show  "t_v_evaluation (IH H) (¬.(F1 ∨. F2)) = Ttrue"
      by (simp add: v_disjunction_def, simp add: v_negation_def)      
    qed 
  qed
qed
(*>*)
text‹ ›
lemma case_P6:
assumes hip1: "hintikkaP H" and 
hip2: "∀G. (G, F1  →. F2) ∈ measure f_size ⟶
(G ∈ H ⟶ t_v_evaluation (IH H) G = Ttrue) ∧ ((¬.G) ∈ H  ⟶ t_v_evaluation (IH H) (¬.G) = Ttrue)"           
shows "((F1  →. F2) ∈ H ⟶ t_v_evaluation (IH H) (F1  →. F2) = Ttrue) ∧
((¬.(F1  →. F2)) ∈ H ⟶ t_v_evaluation (IH H) (¬.(F1  →. F2)) = Ttrue)"
(*<*)
proof(rule conjI impI)+
  assume h2: "(F1 →.F2) ∈ H"
  show " t_v_evaluation (IH H) (F1 →. F2) = Ttrue"
  proof -    
    have "FormulaBeta (F1 →. F2)" by simp  
    hence "Comp1(F1 →. F2) ∈ H ∨ Comp2 (F1 →. F2)∈ H" 
    using hip1 h2 by(auto simp add: hintikkaP_def) 
    hence "(¬.F1) ∈ H ∨ F2 ∈ H" by(unfold Comp1_def, unfold Comp2_def, auto) 
    thus " t_v_evaluation (IH H) (F1 →. F2) = Ttrue"
    proof(rule disjE)           
      assume "(¬.F1) ∈ H"             
      moreover
      have "(¬.F1, F1  →. F2) ∈ measure f_size" using pf_size by auto 
      hence " (¬.F1) ∈ H ⟶  t_v_evaluation (IH H) (¬.F1) = Ttrue" 
      using hip2 by simp
      ultimately
      have 1: "t_v_evaluation (IH H) (¬.F1) = Ttrue" by simp
      hence "t_v_evaluation (IH H) F1 = Ffalse" using NegationValues2 by auto       
      thus "t_v_evaluation (IH H) (F1 →. F2) = Ttrue"  by(simp add: v_implication_def)
      next
      assume "F2 ∈ H"
      moreover       
      have "(F2, F1  →. F2) ∈ measure f_size" by simp
      hence "(F2 ∈ H ⟶  t_v_evaluation (IH H) F2 = Ttrue)" 
      using hip2 by simp    
      ultimately 
      have "t_v_evaluation (IH H) F2 = Ttrue" by simp
      thus "t_v_evaluation (IH H) (F1 →. F2) = Ttrue" by(simp add: v_implication_def)
    qed
  qed
  next
  show "(¬.(F1 →. F2)) ∈ H ⟶        
        t_v_evaluation (IH H) (¬.(F1 →. F2)) = Ttrue"
  proof(rule impI)
    assume h2: "(¬.(F1 →. F2)) ∈ H"
    show "t_v_evaluation (IH H) (¬.(F1 →. F2)) = Ttrue"
    proof -                      
      have "FormulaAlfa (¬.(F1 →. F2))" by auto
      hence "Comp1(¬.(F1 →. F2)) ∈ H ∧ Comp2(¬.(F1 →. F2))∈ H"
      using hip1 h2 by (auto simp add: hintikkaP_def)   
      hence "F1 ∈ H ∧ (¬.F2) ∈ H" by(unfold Comp1_def, unfold Comp2_def, auto)                        
      moreover
      have "(F1, F1  →. F2) ∈ measure f_size" and
      "(¬.F2, F1  →. F2) ∈ measure f_size" using pf_size
      by auto
      hence "F1 ∈ H ⟶ t_v_evaluation (IH H) F1 = Ttrue"
      and "(¬.F2) ∈ H ⟶ t_v_evaluation (IH H) (¬.F2) = Ttrue"
      using hip2 by auto   
      ultimately
      have "t_v_evaluation (IH H) F1 = Ttrue" 
      and
     "t_v_evaluation (IH H) (¬.F2) = Ttrue"  by auto 
      thus       
     "t_v_evaluation (IH H) (¬.(F1 →. F2)) = Ttrue" by(simp add: v_implication_def)
    qed
  qed
qed
(*>*)
text‹ ›
lemma case_P7:
assumes hip1: "hintikkaP H" and
hip2: "∀G. (G, (¬.form)) ∈ measure f_size ⟶ 
(G ∈ H ⟶ t_v_evaluation (IH H) G = Ttrue) ∧ ((¬.G) ∈ H  ⟶ t_v_evaluation (IH H) (¬.G) = Ttrue)"            
shows "((¬.form) ∈ H ⟶ t_v_evaluation (IH H) (¬.form) = Ttrue) ∧
((¬.(¬.form)) ∈ H ⟶ t_v_evaluation (IH H) (¬.(¬.form)) = Ttrue)"
(*<*)
proof(intro conjI)       
  show  "¬.form ∈ H ⟶ t_v_evaluation (IH H) (¬.form) = Ttrue"
  proof(rule impI)
    assume h1: "(¬.form) ∈ H"     
    moreover
    have "(form, (¬.form)) ∈ measure f_size" by simp
    hence "((¬.form) ∈ H ⟶
           t_v_evaluation (IH H) (¬.form)= Ttrue)" 
    using hip2 by simp
    ultimately
    show "t_v_evaluation (IH H) (¬.form) = Ttrue" using h1 by simp
  qed
  next     
  show "(¬.¬.form) ∈ H ⟶ t_v_evaluation (IH H) (¬.¬.form) = Ttrue" 
  proof(rule impI)
    assume h2: "(¬.¬.form) ∈ H"         
    have "∀Z. (¬.¬.Z) ∈ H ⟶ Z ∈ H" using hip1 
    by(unfold hintikkaP_def) blast
    hence "(¬.¬.form) ∈ H ⟶ form ∈ H" by simp    
    hence "form ∈ H" using h2 by simp   
    moreover
    have "(form, (¬.form)) ∈ measure f_size" by simp
    hence "form ∈ H ⟶ t_v_evaluation (IH H) form = Ttrue" 
    using hip2 by simp
    ultimately
    have "t_v_evaluation (IH H) form = Ttrue" by simp
    thus  "t_v_evaluation (IH H) (¬.¬.form) = Ttrue" using h2 by (simp add: v_negation_def)
  qed
qed
(*>*)

theorem hintikkaP_model_aux: 
  assumes hip: "hintikkaP H"
  shows "(F ∈ H ⟶  t_v_evaluation (IH H) F = Ttrue) ∧ 
                    ((¬.F) ∈ H ⟶ t_v_evaluation (IH H) (¬.F) = Ttrue)" 
proof (rule wf_induct [where r="measure f_size" and a=F])    
  show "wf(measure f_size)" by simp
next
  fix F  
  assume hip1: "∀G. (G, F) ∈ measure f_size ⟶
                    (G ∈ H ⟶ t_v_evaluation (IH H) G = Ttrue) ∧
                    ((¬.G) ∈ H  ⟶ t_v_evaluation (IH H) (¬.G) = Ttrue)"         
  show "(F ∈ H ⟶ t_v_evaluation (IH H) F = Ttrue) ∧
        ((¬.F) ∈ H ⟶ t_v_evaluation (IH H) (¬.F) = Ttrue)"
  proof (cases F)    
    assume "F=FF"   
    thus ?thesis using case_P1 hip hip1 by simp
  next 
    assume "F=TT" 
    thus ?thesis using case_P2 hip hip1 by auto
  next
    fix P 
    assume "F = atom P"
    thus ?thesis using hip hip1 case_P3[of H P] by simp
  next
    fix F1  F2
    assume "F= (F1 ∧. F2)"
    thus ?thesis using hip hip1 case_P4[of H F1 F2] by simp
  next
    fix F1 F2
    assume "F= (F1 ∨. F2)"
    thus ?thesis using hip hip1 case_P5[of H F1 F2] by simp
  next
    fix F1 F2
    assume "F= (F1 →. F2)"
    thus ?thesis using hip hip1 case_P6[of H F1 F2] by simp
  next
    fix F1
    assume "F=(¬.F1)"
    thus ?thesis using hip hip1 case_P7[of H F1] by simp    
  qed
qed


corollary ModeloHintikkaPa: 
  assumes "hintikkaP H" and "F ∈ H"  
  shows "t_v_evaluation (IH H) F = Ttrue"
  using assms hintikkaP_model_aux by auto 


corollary ModeloHintikkaP: 
  assumes "hintikkaP H"
  shows "(IH H) model H"
proof (unfold model_def)
  show "∀F∈H. t_v_evaluation (IH H) F = Ttrue"
  proof (rule ballI)
    fix F
    assume "F ∈ H"
    thus "t_v_evaluation (IH H) F = Ttrue" using assms ModeloHintikkaPa  by auto
  qed 
qed 


corollary Hintikkasatisfiable:
  assumes "hintikkaP H"
  shows "satisfiable H"
using assms ModeloHintikkaP
by (unfold satisfiable_def, auto)
 
(*<*)
end
(*>*)