Documentation

Foundation.Modal.Kripke.Ver

source
@[reducible, inline]
abbrev LO.Kripke.IsolatedFrameClass :
LO.Kripke.FrameClass
Equations
Instances For
    source
    theorem LO.Modal.Kripke.axiomVer_defines {α : Type u} {F : LO.Kripke.Frame} :
    F#α ⊧* 𝗩𝗲𝗿 ↔ F ∈ LO.Kripke.IsolatedFrameClass
    source
    instance LO.Modal.Kripke.axiomVer_definability {α : Type u} :
    𝔽(𝗩𝗲𝗿).DefinedBy LO.Kripke.IsolatedFrameClass
    Equations
    source
    instance LO.Modal.Kripke.Ver_definability {α : Type u} :
    LO.Kripke.FrameClass.DefinedBy 𝔽(𝐕𝐞𝐫) LO.Kripke.IsolatedFrameClass
    Equations
    • LO.Modal.Kripke.Ver_definability = inferInstance
    source
    instance LO.Modal.Kripke.instSoundHilbertFormulaDepVerAltIsolatedFrameClass {α : Type u} :
    LO.Sound 𝐕𝐞𝐫 LO.Kripke.IsolatedFrameClass#α
    Equations
    • ⋯ = ⋯
    source
    instance LO.Modal.Kripke.instConsistentFormulaHilbertVer {α : Type u} :
    LO.System.Consistent 𝐕𝐞𝐫
    Equations
    • ⋯ = ⋯
    source
    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
    source
    instance LO.Modal.Kripke.instCompleteHilbertFormulaDepVerAltIsolatedFrameClass {α : Type u} [DecidableEq α] :
    LO.Complete 𝐕𝐞𝐫 LO.Kripke.IsolatedFrameClass#α
    Equations
    • ⋯ = ⋯