Theory PMLinHOL_deep_further_tests


theory PMLinHOL_deep_further_tests
  imports PMLinHOL_deep_tests  
begin  

―‹Implied modal principle›
lemma K_Dia: "⊨⇧^d (□⇧^d(φ ⊃⇧^d ψ)) ⊃⇧^d ((◇⇧^dφ) ⊃⇧^d ◇⇧^dψ)" by auto  

―‹Example 6.10 of Sider (2009) Logic for Philosophy›
lemma T1a: "⊨⇧^d □⇧^dp⇧^d ⊃⇧^d ((◇⇧^dq⇧^d) ⊃⇧^d ◇⇧^d(p⇧^d ∧⇧^d q⇧^d))" by auto  ―‹fast automation in meta-logic HOL›
lemma T1b: "⊨⇧^d □⇧^dp⇧^d ⊃⇧^d ((◇⇧^dq⇧^d) ⊃⇧^d ◇⇧^d(p⇧^d ∧⇧^d q⇧^d))" ―‹alternative interactive proof in modal object logic K›   
  proof -  
    have 1: "⊨⇧^d p⇧^d ⊃⇧^d (q⇧^d ⊃⇧^d (p⇧^d ∧⇧^d q⇧^d))" unfolding AndD_def using H1 H2 H3 MP by metis
    have 2: "⊨⇧^d □⇧^d(p⇧^d ⊃⇧^d (q⇧^d ⊃⇧^d (p⇧^d ∧⇧^d q⇧^d)))" using 1 Nec by metis
    have 3: "⊨⇧^d □⇧^dp⇧^d ⊃⇧^d □⇧^d(q⇧^d ⊃⇧^d (p⇧^d ∧⇧^d q⇧^d))" using 2 Dist MP by metis
    have 4: "⊨⇧^d (□⇧^d(q⇧^d ⊃⇧^d (p⇧^d ∧⇧^d q⇧^d))) ⊃⇧^d ((◇⇧^dq⇧^d) ⊃⇧^d ◇⇧^d(p⇧^d ∧⇧^d q⇧^d))"   using K_Dia by metis
    have 5: "⊨⇧^d □⇧^dp⇧^d ⊃⇧^d ((◇⇧^dq⇧^d) ⊃⇧^d ◇⇧^d(p⇧^d ∧⇧^d q⇧^d))"  using 3 4 H1 H2 MP by metis 
    thus ?thesis . 
  qed
end