Theory PMLinHOL_shallow_minimal_Loeb_tests


theory PMLinHOL_shallow_minimal_Loeb_tests  
  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