Theory PMLinHOL_shallow_further_tests


theory PMLinHOL_shallow_further_tests
  imports PMLinHOL_shallow_tests 
begin

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

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