Theory PMLinHOL_shallow_tests

subsection‹Tests with the maximal shallow embedding›

theory PMLinHOL_shallow_tests 
   imports PMLinHOL_shallow
begin

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

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

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

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

―‹Correspondence theory: correct statements› 
lemma cM:"reflexive R ⟷ (∀φ W V. ∀w:W. ⟨W,R,V⟩,w ⊨⇧^s □⇧^sφ ⊃⇧^s φ)" ―‹sledgehammer: Proof found› oops (**)
lemma cBa: "symmetric R ⟶ (∀φ W V. ∀w:W. ⟨W,R,V⟩,w ⊨⇧^s φ ⊃⇧^s □⇧^s(◇⇧^sφ))" by auto 
(**)lemma cBb: "symmetric R ⟵ (∀φ W V. ∀w:W. ⟨W,R,V⟩,w ⊨⇧^s φ ⊃⇧^s □⇧^s(◇⇧^sφ))" ―‹sledgehammer: No proof› oops
lemma c4a: "transitive R ⟶ (∀φ W V. ∀w:W. ⟨W,R,V⟩,w ⊨⇧^s □⇧^sφ ⊃⇧^s □⇧^s(□⇧^sφ))" by (smt (z3) DefS)
(**)lemma c4b: "transitive R ⟵ (∀φ W V. ∀w:W. ⟨W,R,V⟩,w ⊨⇧^s □⇧^sφ ⊃⇧^s □⇧^s(□⇧^sφ))" ―‹sledgehammer: No proof› oops

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

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

―‹Implied axiom schemata in S5›
lemma KB: "symmetric R ⟶ (∀φ ψ W V. ∀w:W. ⟨W,R,V⟩,w ⊨⇧^s (◇⇧^s(□⇧^sφ)) ⊃⇧^s□⇧^s(◇⇧^sφ))" by auto
lemma K4B: "symmetric R ∧ transitive R ⟶ (∀φ ψ W V. ∀w:W. ⟨W,R,V⟩,w ⊨⇧^s □⇧^s( □⇧^sφ ⊃⇧^s□⇧^sψ) ∨⇧^s □⇧^s( □⇧^sψ ⊃⇧^s□⇧^sφ))" by (smt (z3) DefS)
end