Documentation

Foundation.Modal.Modality.S5

source
@[reducible, inline]
abbrev LO.Modal.S5.modalities :
Modalities
Equations
Instances For
    source
    theorem LO.Modal.S5.modal_reduction_0 :
    ModalReduction Modal.S5 0 S5.modalities
    source
    theorem LO.Modal.S5.modal_reduction_1 :
    ModalReduction Modal.S5 1 S5.modalities
    source
    instance LO.Modal.S5.instS5LogicNatFormula :
    Entailment.S5 Modal.S5
    Equations
    • One or more equations did not get rendered due to their size.
    source
    instance LO.Modal.S5.instS4LogicNatFormula :
    Entailment.S4 Modal.S5
    Equations
    • One or more equations did not get rendered due to their size.
    source
    instance LO.Modal.S5.instEquivalenceBoxPbox :
    (□□) ≅[Modal.S5] □
    source
    instance LO.Modal.S5.instEquivalenceBoxPdia :
    (□◇) ≅[Modal.S5] ◇
    source
    instance LO.Modal.S5.instEquivalenceDiaPdia :
    (◇◇) ≅[Modal.S5] ◇
    source
    instance LO.Modal.S5.instEquivalenceDiaPbox :
    (◇□) ≅[Modal.S5] □
    source
    theorem LO.Modal.S5.modal_reduction_2 :
    ModalReduction Modal.S5 2 S5.modalities
    source
    instance LO.Modal.S5.instEquivalenceNegBoxPnegPdia :
    (∼□∼) ≅[Modal.S5] ◇
    source
    instance LO.Modal.S5.instEquivalenceNegBoxPbox :
    (∼□□) ≅[Modal.S5] ∼□
    source
    instance LO.Modal.S5.instEquivalenceNegDiaPdia :
    (∼◇◇) ≅[Modal.S5] ∼◇
    source
    instance LO.Modal.S5.instEquivalenceNegBoxPdia :
    (∼□◇) ≅[Modal.S5] ∼◇
    source
    instance LO.Modal.S5.instEquivalenceNegDiaPbox :
    (∼◇□) ≅[Modal.S5] ∼□
    source
    instance LO.Modal.S5.instEquivalenceDiaNegPnegPdia :
    (◇∼∼) ≅[Modal.S5] ◇
    source
    instance LO.Modal.S5.instEquivalenceDiaNegPbox :
    (◇∼□) ≅[Modal.S5] ∼□
    source
    instance LO.Modal.S5.instEquivalenceDiaNegPdia :
    (◇∼◇) ≅[Modal.S5] ∼◇
    source
    instance LO.Modal.S5.instEquivalenceDiaBoxPbox :
    (◇□□) ≅[Modal.S5] □
    source
    instance LO.Modal.S5.instEquivalenceDiaBoxPdia :
    (◇□◇) ≅[Modal.S5] ◇
    source
    instance LO.Modal.S5.instEquivalenceDiaBoxPnegNegPdia :
    (◇□∼) ≅[Modal.S5] ∼◇
    source
    instance LO.Modal.S5.instEquivalenceDiaPnegNegPbox :
    (◇◇∼) ≅[Modal.S5] ∼□
    source
    instance LO.Modal.S5.instEquivalenceDiaPbox_1 :
    (◇◇□) ≅[Modal.S5] ◇□
    source
    instance LO.Modal.S5.instEquivalenceDiaPdia_1 :
    (◇◇◇) ≅[Modal.S5] ◇
    source
    theorem LO.Modal.S5.modal_reduction_3 :
    ModalReduction Modal.S5 3 S5.modalities
    source
    theorem LO.Modal.S5.modal_reduction (n : ℕ) :
    ModalReduction Modal.S5 n S5.modalities