Theory PMLinHOL_shallow_minimal_Loeb_tests

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

―‹Löb axiom: with the minimal shallow embedding automated reasoning tools are still partly responsive›
lemma Loeb1: "∀φ. ⊨⇧m □⇧m( □⇧mφ ⊃⇧mφ) ⊃⇧m □⇧mφ" nitpick[card 𝗐=1,card 𝒮=1] oops ―‹nitpick: Counterexample.›
lemma Loeb2: "(conversewf R ∧ transitive R) ⟶(∀φ. ⊨⇧m □⇧m(□⇧mφ ⊃⇧mφ) ⊃⇧m □⇧mφ)" ―‹sh: Proof found› oops
lemma Loeb3: "(conversewf R ∧ transitive R) ⟵ (∀φ. ⊨⇧m □⇧m(□⇧mφ ⊃⇧mφ) ⊃⇧m □⇧mφ)" ―‹sh: No Proof› oops
lemma Loeb3a: "conversewf R ⟵ (∀φ. ⊨⇧m □⇧m(□⇧mφ ⊃⇧mφ) ⊃⇧m □⇧mφ)" unfolding DefM by blast
lemma Loeb3b: "transitive R ⟵ (∀φ. ⊨⇧m □⇧m(□⇧mφ ⊃⇧mφ) ⊃⇧m □⇧mφ)" ―‹sledgehammer: No Proof› oops
lemma Loeb3c: "irreflexive R ⟵ (∀φ. ⊨⇧m □⇧m(□⇧mφ ⊃⇧mφ) ⊃⇧m □⇧mφ)" ―‹sledgehammer: Proof found› oops
end