Theory PMLinHOL_deep_Loeb_tests


theory PMLinHOL_deep_Loeb_tests     (* Christoph Benzmüller, 2025 *)
  imports PMLinHOL_deep 
begin 

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