@[reducible, inline]

abbrev LO.Kripke.IsolatedFrameClass : LO.Kripke.FrameClass

Equations

• LO.Kripke.IsolatedFrameClass F = Isolated F.Rel

theorem LO.Modal.Kripke.axiomVer_defines {α : Type u} {F : LO.Kripke.Frame} : F#α ⊧* 𝗩𝗲𝗿 ↔ F ∈ LO.Kripke.IsolatedFrameClass

instance LO.Modal.Kripke.axiomVer_definability {α : Type u} : 𝔽(𝗩𝗲𝗿).DefinedBy LO.Kripke.IsolatedFrameClass

Equations

• LO.Modal.Kripke.axiomVer_definability = { define := ⋯, nonempty := LO.Modal.Kripke.axiomVer_definability.proof_1 }

instance LO.Modal.Kripke.Ver_definability {α : Type u} : LO.Kripke.FrameClass.DefinedBy 𝔽(𝐕𝐞𝐫) LO.Kripke.IsolatedFrameClass

Equations

• LO.Modal.Kripke.Ver_definability = inferInstance

instance LO.Modal.Kripke.instSoundHilbertFormulaDepVerAltIsolatedFrameClass {α : Type u} : LO.Sound 𝐕𝐞𝐫 LO.Kripke.IsolatedFrameClass#α

Equations

• ⋯ = ⋯

instance LO.Modal.Kripke.instConsistentFormulaHilbertVer {α : Type u} : LO.System.Consistent 𝐕𝐞𝐫

Equations

• ⋯ = ⋯

theorem LO.Modal.Kripke.isolated_CanonicalFrame {α : Type u} [DecidableEq α] {Ax : LO.Modal.Theory α} (h : 𝗩𝗲𝗿 ⊆ Ax) [LO.System.Consistent 𝝂Ax] : Isolated (LO.Modal.Kripke.CanonicalFrame 𝝂Ax).Rel

instance LO.Modal.Kripke.instCompleteHilbertFormulaDepVerAltIsolatedFrameClass {α : Type u} [DecidableEq α] : LO.Complete 𝐕𝐞𝐫 LO.Kripke.IsolatedFrameClass#α

Equations

• ⋯ = ⋯