@[reducible, inline]

abbrev LO.Modal.Kripke.IsolatedFrameClass : FrameClass

Equations

• LO.Modal.Kripke.IsolatedFrameClass = {F : LO.Modal.Kripke.Frame | Isolated F.Rel}

Instances For

• LO.Modal.Hilbert.Ver.Kripke.complete
• LO.Modal.Hilbert.Ver.Kripke.sound

theorem LO.Modal.Kripke.IsolatedFrameClass.is_defined_by_Ver : IsolatedFrameClass.DefinedBy 𝗩𝗲𝗿

instance LO.Modal.Hilbert.Ver.Kripke.sound : Sound (Hilbert.Ver ℕ) Kripke.IsolatedFrameClass

instance LO.Modal.Hilbert.Ver.consistent : System.Consistent (Hilbert.Ver ℕ)

theorem LO.Modal.Hilbert.Kripke.canonicalFrame.is_isolated_of_subset_Ver {Ax : Set (Formula ℕ)} (h : 𝗩𝗲𝗿 ⊆ Ax) [System.Consistent (Hilbert.ExtK Ax)] : Isolated (canonicalFrame (Hilbert.ExtK Ax)).Rel

instance LO.Modal.Hilbert.Ver.Kripke.complete : Complete (Hilbert.Ver ℕ) Kripke.IsolatedFrameClass