Theory PMLinHOL_shallow_Loeb_tests


theory PMLinHOL_shallow_Loeb_tests (* Christoph Benzmüller, 2025 *)
  imports PMLinHOL_shallow 
begin

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