@[reducible, inline]

abbrev LO.Modal.Kripke.FrameClass.trans_cwf : FrameClass

Equations

• LO.Modal.Kripke.FrameClass.trans_cwf = {F : LO.Modal.Kripke.Frame | IsTrans F.World F.Rel ∧ IsConverseWellFounded F.World F.Rel}

@[reducible, inline]

abbrev LO.Modal.Kripke.FrameClass.finite_trans_irrefl : FrameClass

Equations

• LO.Modal.Kripke.FrameClass.finite_trans_irrefl = {F : LO.Modal.Kripke.Frame | Finite F.World ∧ IsTrans F.World F.Rel ∧ IsIrrefl F.World F.Rel}

Instances For

• LO.Modal.Hilbert.GL.Kripke.finiteComplete
• LO.Modal.Hilbert.GL.Kripke.finite_sound

instance LO.Modal.Hilbert.GL.Kripke.finite_sound : Sound Hilbert.GL Kripke.FrameClass.finite_trans_irrefl

instance LO.Modal.Hilbert.GL.Kripke.consistent : Entailment.Consistent Hilbert.GL