Documentation

Foundation.Modal.ModalCompanion.Basic

Gödel Translation

Equations
Instances For
    class LO.Modal.ModalCompanion {α : Type u_1} (iΛ : LO.IntProp.Hilbert α) (mΛ : LO.Modal.Hilbert α) :
    Instances
      theorem LO.Modal.ModalCompanion.companion {α : Type u_1} {iΛ : LO.IntProp.Hilbert α} {mΛ : LO.Modal.Hilbert α} [self : LO.Modal.ModalCompanion ] {p : LO.IntProp.Formula α} :
      ⊢! p ⊢! p
      Equations
      • LO.Modal.instK4HilbertFormulaOfS4 = LO.System.K4.mk