Tree

theorem LO.Modal.Kripke.valid_on_FiniteTransitiveTreeClass_of_valid_on_TransitiveIrreflexiveFrameClass {φ : Formula ℕ} (h : TransitiveIrreflexiveFiniteFrameClass ⊧ φ) (T : FiniteTransitiveTree) : T.toFrame ⊧ φ

theorem LO.Modal.Kripke.satisfies_at_root_on_FiniteTransitiveTree {φ : Formula ℕ} (h : ∀ (T : FiniteTransitiveTree), T.toFrame ⊧ φ) (M : FiniteTransitiveTreeModel) : Formula.Kripke.Satisfies M.toModel M.root φ

theorem LO.Modal.Kripke.valid_on_TransitiveIrreflexiveFrameClass_of_satisfies_at_root_on_FiniteTransitiveTree {φ : Formula ℕ} : (∀ (M : FiniteTransitiveTreeModel), Formula.Kripke.Satisfies M.toModel M.root φ) → TransitiveIrreflexiveFiniteFrameClass ⊧ φ

theorem LO.Modal.Hilbert.GL.Kripke.iff_provable_satisfies_FiniteTransitiveTree {φ : Formula ℕ} : Hilbert.GL ⊢! φ ↔ ∀ (M : Kripke.FiniteTransitiveTreeModel), Formula.Kripke.Satisfies M.toModel M.root φ

theorem LO.Modal.Hilbert.GL.Kripke.iff_unprovable_exists_unsatisfies_FiniteTransitiveTree {φ : Formula ℕ} : Hilbert.GL ⊬ φ ↔ ∃ (M : Kripke.FiniteTransitiveTreeModel), ¬Formula.Kripke.Satisfies M.toModel M.root φ