Theory PMLinHOL_shallow_minimal_tests

subsection‹Tests with the minimal shallow embedding›

theory PMLinHOL_shallow_minimal_tests (* Christoph Benzmüller, 2025 *)
  imports PMLinHOL_shallow_minimal
begin 

―‹Hilbert calculus: proving that the schematic axioms and rules implied by the embedding›
lemma H1: "⊨⇧^m φ ⊃⇧^m (ψ ⊃⇧^m φ)" by auto
lemma H2: "⊨⇧^m (φ ⊃⇧^m (ψ ⊃⇧^m γ)) ⊃⇧^m ((φ ⊃⇧^m ψ) ⊃⇧^m (φ ⊃⇧^m γ)) " by auto
lemma H3: "⊨⇧^m (¬⇧^mφ⊃⇧^m ¬⇧^mψ) ⊃⇧^m (ψ ⊃⇧^m φ)" by auto
lemma MP: "⊨⇧^m φ ⟹ ⊨⇧^m (φ⊃⇧^m ψ) ⟹ ⊨⇧^m ψ" by auto

―‹Reasoning with the Hilbert calculus: interactive and fully automated›
lemma HCderived1: "⊨⇧^m (φ ⊃⇧^m φ)" ―‹sledgehammer(HC1 HC2 HC3 MP) returns: by (metis HC1 HC2 MP)›
  proof -
    have 1: "⊨⇧^m φ ⊃⇧^m ((ψ ⊃⇧^m φ) ⊃⇧^m φ)" using H1 by auto 
    have 2: "⊨⇧^m (φ ⊃⇧^m ((ψ ⊃⇧^m φ) ⊃⇧^m φ)) ⊃⇧^m ((φ ⊃⇧^m (ψ ⊃⇧^m φ)) ⊃⇧^m (φ ⊃⇧^m φ))" using H2 by auto 
    have 3: "⊨⇧^m (φ ⊃⇧^m (ψ ⊃⇧^m φ)) ⊃⇧^m (φ ⊃⇧^m φ)" using 1 2 MP by meson
    have 4: "⊨⇧^m φ ⊃⇧^m (ψ⊃⇧^m φ)" using H1 by auto 
    thus ?thesis using 3 4 MP by meson 
  qed

lemma HCderived2: "⊨⇧^m φ ⊃⇧^m (¬⇧^mφ⊃⇧^m ψ) " by (metis H1 H2 H3 MP) 
lemma HCderived3: "⊨⇧^m (¬⇧^mφ⊃⇧^m φ) ⊃⇧^m φ" by (metis H1 H2 H3 MP) 
lemma HCderived4: "⊨⇧^m (φ ⊃⇧^m ψ) ⊃⇧^m (¬⇧^mψ ⊃⇧^m ¬⇧^mφ) " by auto

―‹Modal logic: the schematic necessitation rule and distribution axiom are implied›
lemma Nec: "⊨⇧^m φ ⟹ ⊨⇧^m □⇧^mφ" by (smt DefM)
lemma Dist:"⊨⇧^m □⇧^m(φ ⊃⇧^m ψ) ⊃⇧^m (□⇧^mφ ⊃⇧^m □⇧^mψ) " by auto

―‹Correspondence theory: correct statements› 
lemma cM:"reflexive R ⟷ (∀φ. ⊨⇧^m □⇧^mφ ⊃⇧^m φ)" by auto
lemma cBa: "symmetric R ⟶ (∀φ. ⊨⇧^m φ ⊃⇧^m □⇧^m◇⇧^mφ)" by auto 
lemma cBb: "symmetric R ⟵ (∀φ. ⊨⇧^m φ ⊃⇧^m □⇧^m◇⇧^mφ)" by (metis DefM)
lemma c4a: "transitive R ⟶ (∀φ. ⊨⇧^m □⇧^mφ ⊃⇧^m □⇧^m(□⇧^mφ))" by (smt DefM)
lemma c4b: "transitive R ⟵ (∀φ. ⊨⇧^m □⇧^mφ ⊃⇧^m □⇧^m(□⇧^mφ))" by auto

―‹Correspondence theory: incorrect statements› 
lemma "reflexive R ⟶ (∀φ. ⊨⇧^m □⇧^mφ ⊃⇧^m □⇧^m(□⇧^mφ))" nitpick[card 𝗐=3,show_all] oops ―‹nitpick: Counterexample›

―‹Simple, incorrect validity statements›
lemma "⊨⇧^m φ ⊃⇧^m □⇧^mφ" nitpick[card 𝗐=2, card 𝒮= 1] oops ―‹nitpick: Counterexample: modal collapse not implied›
lemma "⊨⇧^m □⇧^m( □⇧^mφ ⊃⇧^m□⇧^mψ) ∨⇧^m □⇧^m( □⇧^mψ ⊃⇧^m□⇧^mφ)" nitpick[card 𝗐=3] oops ―‹nitpick: Counterexample› 
lemma "⊨⇧^m (◇⇧^m(□⇧^m φ)) ⊃⇧^m□⇧^m(◇⇧^m φ)" nitpick[card 𝗐=2] oops ―‹nitpick: Counterexample› 

―‹Implied axiom schemata in S5›
lemma KB: "symmetric R ⟶ (∀φ ψ.⊨⇧^m (◇⇧^m(□⇧^mφ)) ⊃⇧^m□⇧^m(◇⇧^mφ))" by auto
lemma K4B: "symmetric R ∧ transitive R ⟶ (∀φ ψ. ⊨⇧^m □⇧^m( □⇧^mφ ⊃⇧^m□⇧^mψ) ∨⇧^m □⇧^m( □⇧^mψ ⊃⇧^m□⇧^mφ))" by (smt DefM)
end