@[reducible, inline]

abbrev LO.Propositional.Logic.KC : Logic

Equations

• LO.Propositional.Logic.KC = LO.Propositional.Hilbert.KC.logic

theorem LO.Propositional.Logic.KC.Kripke.eq_confluent : Logic.KC = Kripke.FrameClass.confluent.logic

theorem LO.Propositional.Logic.KC.Kripke.eq_finite_confluent : Logic.KC = Kripke.FrameClass.finite_confluent.logic

@[reducible, inline]

abbrev LO.Propositional.Logic.LC : Logic

Equations

• LO.Propositional.Logic.LC = LO.Propositional.Hilbert.LC.logic

theorem LO.Propositional.Logic.LC.Kripke.eq_connected : Logic.LC = Kripke.FrameClass.connected.logic

theorem LO.Propositional.Logic.LC.Kripke.eq_finite_connected : Logic.LC = Kripke.FrameClass.finite_connected.logic

@[reducible, inline]

abbrev LO.Propositional.Logic.Cl : Logic

Equations

• LO.Propositional.Logic.Cl = LO.Propositional.Hilbert.Cl.logic

theorem LO.Propositional.Logic.Cl.Kripke.eq_euclidean : Logic.Cl = Kripke.FrameClass.euclidean.logic

theorem LO.Propositional.Logic.Cl.Kripke.eq_finite_euclidean : Logic.Cl = Kripke.FrameClass.finite_euclidean.logic

theorem LO.Propositional.Logic.Cl.Kripke.eq_finite_symmetric : Logic.Cl = Kripke.FrameClass.finite_symmetric.logic