Documentation

Foundation.Modal.Hilbert.Equiv.KD_KP

source
theorem LO.Modal.Hilbert.KD_weakerThan_KP {α : Type u_1} [DecidableEq α] :
Hilbert.KD α ≤ₛ Hilbert.KP α
source
theorem LO.Modal.Hilbert.KP_weakerThan_KD {α : Type u_1} [DecidableEq α] :
Hilbert.KP α ≤ₛ Hilbert.KD α
source
theorem LO.Modal.Hilbert.KD_equiv_KP {α : Type u_1} [DecidableEq α] :
Hilbert.KD α =ₛ Hilbert.KP α