Documentation

Foundation.Modal.Boxdot.Basic

class LO.Modal.BoxdotProperty {α : Type u_1} (H₁ H₂ : Hilbert α) :
Instances
    theorem LO.Modal.boxdotTranslated {α : Type u_1} [DecidableEq α] {φ : Formula α} {H₁ H₂ : Hilbert α} [H₁.IsNormal] [H₂.IsNormal] (h : φH₁.axioms, H₂ ⊢! φ) :
    H₁ ⊢! φH₂ ⊢! φ