@[reducible, inline]

abbrev LO.Modal.Kripke.TransitiveConverseWellFoundedFrameClass : LO.Modal.Kripke.FrameClass

Equations

• LO.Modal.Kripke.TransitiveConverseWellFoundedFrameClass = {F : LO.Modal.Kripke.Frame | Transitive F.Rel ∧ ConverseWellFounded F.Rel}

@[reducible, inline]

abbrev LO.Modal.Kripke.TransitiveIrreflexiveFiniteFrameClass : LO.Modal.Kripke.FiniteFrameClass

Equations

• LO.Modal.Kripke.TransitiveIrreflexiveFiniteFrameClass = {F : LO.Modal.Kripke.FiniteFrame | Transitive F.Rel ∧ Irreflexive F.Rel}

theorem LO.Modal.Kripke.TransitiveConverseWellFoundedFrameClass.is_defined_by_L : LO.Modal.Kripke.TransitiveConverseWellFoundedFrameClass.DefinedBy 𝗟

theorem LO.Modal.Kripke.FiniteIrreflexiveFrameClass.is_finite_defined_by_L : LO.Modal.Kripke.TransitiveIrreflexiveFiniteFrameClass.DefinedBy 𝗟

instance LO.Modal.Hilbert.GL.Kripke.sound : LO.Sound (LO.Modal.Hilbert.GL ℕ) LO.Modal.Kripke.TransitiveConverseWellFoundedFrameClass

Equations

• LO.Modal.Hilbert.GL.Kripke.sound = ⋯

instance LO.Modal.Hilbert.GL.Kripke.finite_sound : LO.Sound (LO.Modal.Hilbert.GL ℕ) LO.Modal.Kripke.TransitiveIrreflexiveFiniteFrameClass

Equations

• LO.Modal.Hilbert.GL.Kripke.finite_sound = ⋯

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

Equations

• LO.Modal.Hilbert.GL.consistent = ⋯