Documentation

Foundation.Modal.Hilbert.WellKnown

source
class LO.Modal.Hilbert.HasT {α : Type u_1} (H : Hilbert α) :
Type u_1
Instances
source
instance LO.Modal.Hilbert.instHasAxiomTFormulaOfHasT {α : Type u_1} {H : Hilbert α} [DecidableEq α] [hT : H.HasT] :
Entailment.HasAxiomT H
Equations
source
class LO.Modal.Hilbert.HasB {α : Type u_1} (H : Hilbert α) :
Type u_1
Instances
source
instance LO.Modal.Hilbert.instHasAxiomBFormulaOfHasB {α : Type u_1} {H : Hilbert α} [DecidableEq α] [hB : H.HasB] :
Entailment.HasAxiomB H
Equations
source
class LO.Modal.Hilbert.HasD {α : Type u_1} (H : Hilbert α) :
Type u_1
Instances
source
instance LO.Modal.Hilbert.instHasAxiomDFormulaOfHasD {α : Type u_1} {H : Hilbert α} [DecidableEq α] [hD : H.HasD] :
Entailment.HasAxiomD H
Equations
source
class LO.Modal.Hilbert.HasFour {α : Type u_1} (H : Hilbert α) :
Type u_1
Instances
source
instance LO.Modal.Hilbert.instHasAxiomFourFormulaOfHasFour {α : Type u_1} {H : Hilbert α} [DecidableEq α] [hFour : H.HasFour] :
Entailment.HasAxiomFour H
Equations
source
class LO.Modal.Hilbert.HasFive {α : Type u_1} (H : Hilbert α) :
Type u_1
Instances
source
instance LO.Modal.Hilbert.instHasAxiomFiveFormulaOfHasFive {α : Type u_1} {H : Hilbert α} [DecidableEq α] [hFive : H.HasFive] :
Entailment.HasAxiomFive H
Equations
source
class LO.Modal.Hilbert.HasPoint2 {α : Type u_1} (H : Hilbert α) :
Type u_1
Instances
source
instance LO.Modal.Hilbert.instHasAxiomPoint2FormulaOfHasPoint2 {α : Type u_1} {H : Hilbert α} [DecidableEq α] [hPoint2 : H.HasPoint2] :
Entailment.HasAxiomPoint2 H
Equations
source
class LO.Modal.Hilbert.HasWeakPoint2 {α : Type u_1} (H : Hilbert α) :
Type u_1
Instances
source
instance LO.Modal.Hilbert.instHasAxiomWeakPoint2FormulaOfHasWeakPoint2 {α : Type u_1} {H : Hilbert α} [DecidableEq α] [hDotWeak2 : H.HasWeakPoint2] :
Entailment.HasAxiomWeakPoint2 H
Equations
source
class LO.Modal.Hilbert.HasPoint3 {α : Type u_1} (H : Hilbert α) :
Type u_1
Instances
source
instance LO.Modal.Hilbert.instHasAxiomPoint3FormulaOfHasPoint3 {α : Type u_1} {H : Hilbert α} [DecidableEq α] [hPoint3 : H.HasPoint3] :
Entailment.HasAxiomPoint3 H
Equations
source
class LO.Modal.Hilbert.HasWeakPoint3 {α : Type u_1} (H : Hilbert α) :
Type u_1
Instances
source
instance LO.Modal.Hilbert.instHasAxiomWeakPoint3FormulaOfHasWeakPoint3 {α : Type u_1} {H : Hilbert α} [DecidableEq α] [hDotWeak3 : H.HasWeakPoint3] :
Entailment.HasAxiomWeakPoint3 H
Equations
source
class LO.Modal.Hilbert.HasPoint4 {α : Type u_1} (H : Hilbert α) :
Type u_1
Instances
source
instance LO.Modal.Hilbert.instHasAxiomPoint4FormulaOfHasPoint4 {α : Type u_1} {H : Hilbert α} [DecidableEq α] [H.HasPoint4] :
Entailment.HasAxiomPoint4 H
Equations
source
class LO.Modal.Hilbert.HasL {α : Type u_1} (H : Hilbert α) :
Type u_1
Instances
source
instance LO.Modal.Hilbert.instHasAxiomLFormulaOfHasL {α : Type u_1} {H : Hilbert α} [DecidableEq α] [hL : H.HasL] :
Entailment.HasAxiomL H
Equations
source
class LO.Modal.Hilbert.HasGrz {α : Type u_1} (H : Hilbert α) :
Type u_1
Instances
source
instance LO.Modal.Hilbert.instHasAxiomGrzFormulaOfHasGrz {α : Type u_1} {H : Hilbert α} [DecidableEq α] [hGrz : H.HasGrz] :
Entailment.HasAxiomGrz H
Equations
source
class LO.Modal.Hilbert.HasTc {α : Type u_1} (H : Hilbert α) :
Type u_1
Instances
source
instance LO.Modal.Hilbert.instHasAxiomTcFormulaOfHasTc {α : Type u_1} {H : Hilbert α} [DecidableEq α] [hTc : H.HasTc] :
Entailment.HasAxiomTc H
Equations
source
class LO.Modal.Hilbert.HasVer {α : Type u_1} (H : Hilbert α) :
Type u_1
Instances
source
instance LO.Modal.Hilbert.instHasAxiomVerFormulaOfDecidableEqOfHasVer {α : Type u_1} {H : Hilbert α} [DecidableEq α] [hVer : H.HasVer] :
Entailment.HasAxiomVer H
Equations
source
class LO.Modal.Hilbert.HasH {α : Type u_1} (H : Hilbert α) :
Type u_1
Instances
source
instance LO.Modal.Hilbert.instHasAxiomHFormulaOfHasH {α : Type u_1} {H : Hilbert α} [DecidableEq α] [hH : H.HasH] :
Entailment.HasAxiomH H
Equations
source
class LO.Modal.Hilbert.HasZ {α : Type u_1} (H : Hilbert α) :
Type u_1
Instances
source
instance LO.Modal.Hilbert.instHasAxiomZFormulaOfHasZ {α : Type u_1} {H : Hilbert α} [DecidableEq α] [hZ : H.HasZ] :
Entailment.HasAxiomZ H
Equations
source
class LO.Modal.Hilbert.HasM {α : Type u_1} (H : Hilbert α) :
Type u_1
Instances
source
instance LO.Modal.Hilbert.instHasAxiomMFormulaOfHasM {α : Type u_1} {H : Hilbert α} [DecidableEq α] [hM : H.HasM] :
Entailment.HasAxiomM H
Equations
source
class LO.Modal.Hilbert.HasMk {α : Type u_1} (H : Hilbert α) :
Type u_1
Instances
source
instance LO.Modal.Hilbert.instHasAxiomMkFormulaOfHasMk {α : Type u_1} {H : Hilbert α} [DecidableEq α] [H.HasMk] :
Entailment.HasAxiomMk H
Equations
source
class LO.Modal.Hilbert.HasGeach {α : Type u_1} (g : Axioms.Geach.Taple) (H : Hilbert α) :
Type u_1
Instances
    source
    instance LO.Modal.Hilbert.instHasAxiomGeachFormulaOfHasGeach {α : Type u_1} {H : Hilbert α} [DecidableEq α] {g : Axioms.Geach.Taple} [HasGeach g H] :
    Entailment.HasAxiomGeach g H
    Equations
    source
    @[reducible, inline]
    abbrev LO.Modal.Hilbert.KT :
    Hilbert ℕ
    Equations
    Instances For
    source
    @[reducible, inline]
    abbrev LO.Modal.Logic.KT :
    Logic
    Equations
    source
    instance LO.Modal.Hilbert.KT.instHasKNat :
    Hilbert.KT.HasK
    Equations
    source
    instance LO.Modal.Hilbert.KT.instHasTNat :
    Hilbert.KT.HasT
    Equations
    source
    instance LO.Modal.Hilbert.KT.instKTNatFormula :
    Entailment.KT Hilbert.KT
    Equations
    • One or more equations did not get rendered due to their size.
    source
    @[reducible, inline]
    abbrev LO.Modal.Hilbert.KD :
    Hilbert ℕ
    Equations
    Instances For
    source
    @[reducible, inline]
    abbrev LO.Modal.Logic.KD :
    Logic
    Equations
    source
    instance LO.Modal.Hilbert.KD.instHasKNat :
    Hilbert.KD.HasK
    Equations
    source
    instance LO.Modal.Hilbert.KD.instHasDNat :
    Hilbert.KD.HasD
    Equations
    source
    instance LO.Modal.Hilbert.KD.instKDNatFormula :
    Entailment.KD Hilbert.KD
    Equations
    • One or more equations did not get rendered due to their size.
    source
    @[reducible, inline]
    abbrev LO.Modal.Hilbert.KB :
    Hilbert ℕ
    Equations
    Instances For
    source
    @[reducible, inline]
    abbrev LO.Modal.Logic.KB :
    Logic
    Equations
    source
    instance LO.Modal.Hilbert.KB.instHasKNat :
    Hilbert.KB.HasK
    Equations
    source
    instance LO.Modal.Hilbert.KB.instHasBNat :
    Hilbert.KB.HasB
    Equations
    source
    instance LO.Modal.Hilbert.KB.instKBNatFormula :
    Entailment.KB Hilbert.KB
    Equations
    • One or more equations did not get rendered due to their size.
    source
    @[reducible, inline]
    abbrev LO.Modal.Hilbert.KDB :
    Hilbert ℕ
    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
    source
    @[reducible, inline]
    abbrev LO.Modal.Logic.KDB :
    Logic
    Equations
    source
    instance LO.Modal.Hilbert.KDB.instHasKNat :
    Hilbert.KDB.HasK
    Equations
    source
    instance LO.Modal.Hilbert.KDB.instHasDNat :
    Hilbert.KDB.HasD
    Equations
    source
    instance LO.Modal.Hilbert.KDB.instHasBNat :
    Hilbert.KDB.HasB
    Equations
    source
    instance LO.Modal.Hilbert.KDB.instKDBNatFormula :
    Entailment.KDB Hilbert.KDB
    Equations
    • One or more equations did not get rendered due to their size.
    source
    @[reducible, inline]
    abbrev LO.Modal.Hilbert.KTB :
    Hilbert ℕ
    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
    source
    @[reducible, inline]
    abbrev LO.Modal.Logic.KTB :
    Logic
    Equations
    source
    instance LO.Modal.Hilbert.KTB.instHasKNat :
    Hilbert.KTB.HasK
    Equations
    source
    instance LO.Modal.Hilbert.KTB.instHasTNat :
    Hilbert.KTB.HasT
    Equations
    source
    instance LO.Modal.Hilbert.KTB.instHasBNat :
    Hilbert.KTB.HasB
    Equations
    source
    instance LO.Modal.Hilbert.KTB.instKTBNatFormula :
    Entailment.KTB Hilbert.KTB
    Equations
    • One or more equations did not get rendered due to their size.
    source
    @[reducible, inline]
    abbrev LO.Modal.Hilbert.KM :
    Hilbert ℕ
    Equations
    Instances For
    source
    @[reducible, inline]
    abbrev LO.Modal.Logic.KM :
    Logic
    Equations
    source
    instance LO.Modal.Hilbert.KM.instHasKNat :
    Hilbert.KM.HasK
    Equations
    source
    instance LO.Modal.Hilbert.KM.instHasMNat :
    Hilbert.KM.HasM
    Equations
    source
    instance LO.Modal.Hilbert.KM.instKMNatFormula :
    Entailment.KM Hilbert.KM
    Equations
    • One or more equations did not get rendered due to their size.
    source
    instance LO.Modal.Hilbert.K_weakerThan_KM :
    Hilbert.K ⪯ Hilbert.KM
    source
    @[reducible, inline]
    abbrev LO.Modal.Hilbert.K4 :
    Hilbert ℕ
    Equations
    Instances For
    source
    @[reducible, inline]
    abbrev LO.Modal.Logic.K4 :
    Logic
    Equations
    Instances For
    source
    instance LO.Modal.Hilbert.K4.instHasKNat :
    Hilbert.K4.HasK
    Equations
    source
    instance LO.Modal.Hilbert.K4.instHasFourNat :
    Hilbert.K4.HasFour
    Equations
    source
    instance LO.Modal.Hilbert.K4.instK4NatFormula :
    Entailment.K4 Hilbert.K4
    Equations
    • One or more equations did not get rendered due to their size.
    source
    @[reducible, inline]
    abbrev LO.Modal.Hilbert.K4Point1 :
    Hilbert ℕ
    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
    source
    @[reducible, inline]
    abbrev LO.Modal.Logic.K4Point1 :
    Logic
    Equations
    source
    instance LO.Modal.Hilbert.K4Point1.instHasKNat :
    Hilbert.K4Point1.HasK
    Equations
    source
    instance LO.Modal.Hilbert.K4Point1.instHasFourNat :
    Hilbert.K4Point1.HasFour
    Equations
    source
    instance LO.Modal.Hilbert.K4Point1.instHasMNat :
    Hilbert.K4Point1.HasM
    Equations
    source
    instance LO.Modal.Hilbert.K4Point1.instK4Point1NatFormula :
    Entailment.K4Point1 Hilbert.K4Point1
    Equations
    • One or more equations did not get rendered due to their size.
    source
    noncomputable instance LO.Modal.Hilbert.K4Point1.instK4Point1NatFormulaOfWeakerThan {H : Hilbert ℕ} [Hilbert.K4Point1 ⪯ H] :
    Entailment.K4Point1 H
    Equations
    • One or more equations did not get rendered due to their size.
    source
    instance LO.Modal.Hilbert.K_weakerThan_K4Point1 :
    Hilbert.K ⪯ Hilbert.K4Point1
    source
    @[reducible, inline]
    abbrev LO.Modal.Hilbert.K4Point2 :
    Hilbert ℕ
    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
    source
    @[reducible, inline]
    abbrev LO.Modal.Logic.K4Point2 :
    Logic
    Equations
    source
    instance LO.Modal.Hilbert.K4Point2.instHasKNat :
    Hilbert.K4Point2.HasK
    Equations
    source
    instance LO.Modal.Hilbert.K4Point2.instHasFourNat :
    Hilbert.K4Point2.HasFour
    Equations
    source
    instance LO.Modal.Hilbert.K4Point2.instHasWeakPoint2Nat :
    Hilbert.K4Point2.HasWeakPoint2
    Equations
    source
    instance LO.Modal.Hilbert.K4Point2.instK4Point2NatFormula :
    Entailment.K4Point2 Hilbert.K4Point2
    Equations
    • One or more equations did not get rendered due to their size.
    source
    @[reducible, inline]
    abbrev LO.Modal.Hilbert.K4Point3 :
    Hilbert ℕ
    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
    source
    @[reducible, inline]
    abbrev LO.Modal.Logic.K4Point3 :
    Logic
    Equations
    source
    instance LO.Modal.Hilbert.K4Point3.instHasKNat :
    Hilbert.K4Point3.HasK
    Equations
    source
    instance LO.Modal.Hilbert.K4Point3.instHasFourNat :
    Hilbert.K4Point3.HasFour
    Equations
    source
    instance LO.Modal.Hilbert.K4Point3.instHasWeakPoint3Nat :
    Hilbert.K4Point3.HasWeakPoint3
    Equations
    source
    instance LO.Modal.Hilbert.K4Point3.instK4Point3NatFormula :
    Entailment.K4Point3 Hilbert.K4Point3
    Equations
    • One or more equations did not get rendered due to their size.
    source
    @[reducible, inline]
    abbrev LO.Modal.Hilbert.KT4B :
    Hilbert ℕ
    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
    source
    @[reducible, inline]
    abbrev LO.Modal.Logic.KT4B :
    Logic
    Equations
    source
    instance LO.Modal.Hilbert.KT4B.instHasKNat :
    Hilbert.KT4B.HasK
    Equations
    source
    instance LO.Modal.Hilbert.KT4B.instHasTNat :
    Hilbert.KT4B.HasT
    Equations
    source
    instance LO.Modal.Hilbert.KT4B.instHasFourNat :
    Hilbert.KT4B.HasFour
    Equations
    source
    instance LO.Modal.Hilbert.KT4B.instHasBNat :
    Hilbert.KT4B.HasB
    Equations
    source
    instance LO.Modal.Hilbert.KT4B.instKT4BNatFormula :
    Entailment.KT4B Hilbert.KT4B
    Equations
    • One or more equations did not get rendered due to their size.
    source
    @[reducible, inline]
    abbrev LO.Modal.Hilbert.K45 :
    Hilbert ℕ
    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
    source
    @[reducible, inline]
    abbrev LO.Modal.Logic.K45 :
    Logic
    Equations
    source
    instance LO.Modal.Hilbert.K45.instHasKNat :
    Hilbert.K45.HasK
    Equations
    source
    instance LO.Modal.Hilbert.K45.instHasFourNat :
    Hilbert.K45.HasFour
    Equations
    source
    instance LO.Modal.Hilbert.K45.instHasFiveNat :
    Hilbert.K45.HasFive
    Equations
    source
    instance LO.Modal.Hilbert.K45.instK45NatFormula :
    Entailment.K45 Hilbert.K45
    Equations
    • One or more equations did not get rendered due to their size.
    source
    @[reducible, inline]
    abbrev LO.Modal.Hilbert.KD4 :
    Hilbert ℕ
    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
    source
    @[reducible, inline]
    abbrev LO.Modal.Logic.KD4 :
    Logic
    Equations
    source
    instance LO.Modal.Hilbert.KD4.instHasKNat :
    Hilbert.KD4.HasK
    Equations
    source
    instance LO.Modal.Hilbert.KD4.instHasDNat :
    Hilbert.KD4.HasD
    Equations
    source
    instance LO.Modal.Hilbert.KD4.instHasFourNat :
    Hilbert.KD4.HasFour
    Equations
    source
    instance LO.Modal.Hilbert.KD4.instKD4NatFormula :
    Entailment.KD4 Hilbert.KD4
    Equations
    • One or more equations did not get rendered due to their size.
    source
    @[reducible, inline]
    abbrev LO.Modal.Hilbert.KD5 :
    Hilbert ℕ
    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
    source
    @[reducible, inline]
    abbrev LO.Modal.Logic.KD5 :
    Logic
    Equations
    source
    instance LO.Modal.Hilbert.KD5.instHasKNat :
    Hilbert.KD5.HasK
    Equations
    source
    instance LO.Modal.Hilbert.KD5.instHasDNat :
    Hilbert.KD5.HasD
    Equations
    source
    instance LO.Modal.Hilbert.KD5.instHasFiveNat :
    Hilbert.KD5.HasFive
    Equations
    source
    instance LO.Modal.Hilbert.KD5.instKD5NatFormula :
    Entailment.KD5 Hilbert.KD5
    Equations
    • One or more equations did not get rendered due to their size.
    source
    @[reducible, inline]
    abbrev LO.Modal.Hilbert.KD45 :
    Hilbert ℕ
    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
    source
    @[reducible, inline]
    abbrev LO.Modal.Logic.KD45 :
    Logic
    Equations
    source
    instance LO.Modal.Hilbert.KD45.instHasKNat :
    Hilbert.KD45.HasK
    Equations
    source
    instance LO.Modal.Hilbert.KD45.instHasDNat :
    Hilbert.KD45.HasD
    Equations
    source
    instance LO.Modal.Hilbert.KD45.instHasFourNat :
    Hilbert.KD45.HasFour
    Equations
    source
    instance LO.Modal.Hilbert.KD45.instHasFiveNat :
    Hilbert.KD45.HasFive
    Equations
    source
    instance LO.Modal.Hilbert.KD45.instKD45NatFormula :
    Entailment.KD45 Hilbert.KD45
    Equations
    • One or more equations did not get rendered due to their size.
    source
    @[reducible, inline]
    abbrev LO.Modal.Hilbert.KB4 :
    Hilbert ℕ
    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
    source
    @[reducible, inline]
    abbrev LO.Modal.Logic.KB4 :
    Logic
    Equations
    source
    instance LO.Modal.Hilbert.KB4.instHasKNat :
    Hilbert.KB4.HasK
    Equations
    source
    instance LO.Modal.Hilbert.KB4.instHasBNat :
    Hilbert.KB4.HasB
    Equations
    source
    instance LO.Modal.Hilbert.KB4.instHasFourNat :
    Hilbert.KB4.HasFour
    Equations
    source
    instance LO.Modal.Hilbert.KB4.instKB4NatFormula :
    Entailment.KB4 Hilbert.KB4
    Equations
    • One or more equations did not get rendered due to their size.
    source
    @[reducible, inline]
    abbrev LO.Modal.Hilbert.KB5 :
    Hilbert ℕ
    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
    source
    @[reducible, inline]
    abbrev LO.Modal.Logic.KB5 :
    Logic
    Equations
    source
    instance LO.Modal.Hilbert.KB5.instHasKNat :
    Hilbert.KB5.HasK
    Equations
    source
    instance LO.Modal.Hilbert.KB5.instHasBNat :
    Hilbert.KB5.HasB
    Equations
    source
    instance LO.Modal.Hilbert.KB5.instHasFiveNat :
    Hilbert.KB5.HasFive
    Equations
    source
    instance LO.Modal.Hilbert.KB5.instKB5NatFormula :
    Entailment.KB5 Hilbert.KB5
    Equations
    • One or more equations did not get rendered due to their size.
    source
    @[reducible, inline]
    abbrev LO.Modal.Hilbert.S4 :
    Hilbert ℕ
    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
    source
    @[reducible, inline]
    abbrev LO.Modal.Logic.S4 :
    Logic
    Equations
    Instances For
    source
    instance LO.Modal.Hilbert.S4.instHasKNat :
    Hilbert.S4.HasK
    Equations
    source
    instance LO.Modal.Hilbert.S4.instHasTNat :
    Hilbert.S4.HasT
    Equations
    source
    instance LO.Modal.Hilbert.S4.instHasFourNat :
    Hilbert.S4.HasFour
    Equations
    source
    instance LO.Modal.Hilbert.S4.instS4NatFormula :
    Entailment.S4 Hilbert.S4
    Equations
    • One or more equations did not get rendered due to their size.
    source
    instance LO.Modal.Hilbert.K4_weakerThan_S4 :
    Hilbert.K4 ⪯ Hilbert.S4
    source
    @[reducible, inline]
    abbrev LO.Modal.Hilbert.S4Point1 :
    Hilbert ℕ
    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
    source
    @[reducible, inline]
    abbrev LO.Modal.Logic.S4Point1 :
    Logic
    Equations
    source
    instance LO.Modal.Hilbert.S4Point1.instHasKNat :
    Hilbert.S4Point1.HasK
    Equations
    source
    instance LO.Modal.Hilbert.S4Point1.instHasTNat :
    Hilbert.S4Point1.HasT
    Equations
    source
    instance LO.Modal.Hilbert.S4Point1.instHasFourNat :
    Hilbert.S4Point1.HasFour
    Equations
    source
    instance LO.Modal.Hilbert.S4Point1.instHasMNat :
    Hilbert.S4Point1.HasM
    Equations
    source
    instance LO.Modal.Hilbert.S4Point1.instS4Point1NatFormula :
    Entailment.S4Point1 Hilbert.S4Point1
    Equations
    • One or more equations did not get rendered due to their size.
    source
    instance LO.Modal.Hilbert.S4Point1.instWeakerThanFormulaNatK4Point1 :
    Hilbert.K4Point1 ⪯ Hilbert.S4Point1
    source
    @[reducible, inline]
    abbrev LO.Modal.Hilbert.S4Point2 :
    Hilbert ℕ
    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
    source
    @[reducible, inline]
    abbrev LO.Modal.Logic.S4Point2 :
    Logic
    Equations
    Instances For
    source
    instance LO.Modal.Hilbert.S4Point2.instHasKNat :
    Hilbert.S4Point2.HasK
    Equations
    source
    instance LO.Modal.Hilbert.S4Point2.instHasTNat :
    Hilbert.S4Point2.HasT
    Equations
    source
    instance LO.Modal.Hilbert.S4Point2.instHasFourNat :
    Hilbert.S4Point2.HasFour
    Equations
    source
    instance LO.Modal.Hilbert.S4Point2.instHasPoint2Nat :
    Hilbert.S4Point2.HasPoint2
    Equations
    source
    instance LO.Modal.Hilbert.S4Point2.instS4Point2NatFormula :
    Entailment.S4Point2 Hilbert.S4Point2
    Equations
    • One or more equations did not get rendered due to their size.
    source
    @[reducible, inline]
    abbrev LO.Modal.Hilbert.S4Point2Point1 :
    Hilbert ℕ
    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
    source
    @[reducible, inline]
    abbrev LO.Modal.Logic.S4Point2Point1 :
    Logic
    • Sobociński's K2 (Hudges & Cresswell 2007)
    Equations
    source
    instance LO.Modal.Hilbert.S4Point2Point1.instHasKNat :
    Hilbert.S4Point2Point1.HasK
    Equations
    source
    instance LO.Modal.Hilbert.S4Point2Point1.instHasTNat :
    Hilbert.S4Point2Point1.HasT
    Equations
    source
    instance LO.Modal.Hilbert.S4Point2Point1.instHasFourNat :
    Hilbert.S4Point2Point1.HasFour
    Equations
    source
    instance LO.Modal.Hilbert.S4Point2Point1.instHasMNat :
    Hilbert.S4Point2Point1.HasM
    Equations
    source
    instance LO.Modal.Hilbert.S4Point2Point1.instHasPoint2Nat :
    Hilbert.S4Point2Point1.HasPoint2
    Equations
    source
    instance LO.Modal.Hilbert.S4Point2Point1.instS4Point2Point1NatFormula :
    Entailment.S4Point2Point1 Hilbert.S4Point2Point1
    Equations
    • One or more equations did not get rendered due to their size.
    source
    instance LO.Modal.Hilbert.S4Point2Point1.instWeakerThanFormulaNatK4Point1 :
    Hilbert.K4Point1 ⪯ Hilbert.S4Point2Point1
    source
    @[reducible, inline]
    abbrev LO.Modal.Hilbert.S4Point3 :
    Hilbert ℕ
    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
    source
    @[reducible, inline]
    abbrev LO.Modal.Logic.S4Point3 :
    Logic
    Equations
    Instances For
    source
    instance LO.Modal.Hilbert.S4Point3.instHasKNat :
    Hilbert.S4Point3.HasK
    Equations
    source
    instance LO.Modal.Hilbert.S4Point3.instHasTNat :
    Hilbert.S4Point3.HasT
    Equations
    source
    instance LO.Modal.Hilbert.S4Point3.instHasFourNat :
    Hilbert.S4Point3.HasFour
    Equations
    source
    instance LO.Modal.Hilbert.S4Point3.instHasPoint3Nat :
    Hilbert.S4Point3.HasPoint3
    Equations
    source
    instance LO.Modal.Hilbert.S4Point3.instS4Point3NatFormula :
    Entailment.S4Point3 Hilbert.S4Point3
    Equations
    • One or more equations did not get rendered due to their size.
    source
    @[reducible, inline]
    abbrev LO.Modal.Hilbert.S4Point4 :
    Hilbert ℕ
    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
    source
    @[reducible, inline]
    abbrev LO.Modal.Logic.S4Point4 :
    Logic
    Equations
    source
    instance LO.Modal.Hilbert.S4Point4.instHasKNat :
    Hilbert.S4Point4.HasK
    Equations
    source
    instance LO.Modal.Hilbert.S4Point4.instHasTNat :
    Hilbert.S4Point4.HasT
    Equations
    source
    instance LO.Modal.Hilbert.S4Point4.instHasFourNat :
    Hilbert.S4Point4.HasFour
    Equations
    source
    instance LO.Modal.Hilbert.S4Point4.instHasPoint4Nat :
    Hilbert.S4Point4.HasPoint4
    Equations
    source
    instance LO.Modal.Hilbert.S4Point4.instS4Point4NatFormula :
    Entailment.S4Point4 Hilbert.S4Point4
    Equations
    • One or more equations did not get rendered due to their size.
    source
    @[reducible, inline]
    abbrev LO.Modal.Hilbert.K5 :
    Hilbert ℕ
    Equations
    Instances For
    source
    @[reducible, inline]
    abbrev LO.Modal.Logic.K5 :
    Logic
    Equations
    source
    instance LO.Modal.Hilbert.K5.instHasKNat :
    Hilbert.K5.HasK
    Equations
    source
    instance LO.Modal.Hilbert.K5.instHasFiveNat :
    Hilbert.K5.HasFive
    Equations
    source
    instance LO.Modal.Hilbert.K5.instK5NatFormula :
    Entailment.K5 Hilbert.K5
    Equations
    • One or more equations did not get rendered due to their size.
    source
    @[reducible, inline]
    abbrev LO.Modal.Hilbert.S5 :
    Hilbert ℕ
    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
    source
    @[reducible, inline]
    abbrev LO.Modal.Logic.S5 :
    Logic
    Equations
    Instances For
    source
    instance LO.Modal.Hilbert.S5.instHasKNat :
    Hilbert.S5.HasK
    Equations
    source
    instance LO.Modal.Hilbert.S5.instHasTNat :
    Hilbert.S5.HasT
    Equations
    source
    instance LO.Modal.Hilbert.S5.instHasFiveNat :
    Hilbert.S5.HasFive
    Equations
    source
    instance LO.Modal.Hilbert.S5.instS5NatFormula :
    Entailment.S5 Hilbert.S5
    Equations
    • One or more equations did not get rendered due to their size.
    source
    @[reducible, inline]
    abbrev LO.Modal.Hilbert.GL :
    Hilbert ℕ
    Equations
    Instances For
    source
    @[reducible, inline]
    abbrev LO.Modal.Logic.GL :
    Logic
    Equations
    Instances For
    source
    instance LO.Modal.Hilbert.GL.instHasKNat :
    Hilbert.GL.HasK
    Equations
    source
    instance LO.Modal.Hilbert.GL.instHasLNat :
    Hilbert.GL.HasL
    Equations
    source
    instance LO.Modal.Hilbert.GL.instGLNatFormula :
    Entailment.GL Hilbert.GL
    Equations
    • One or more equations did not get rendered due to their size.
    source
    @[reducible, inline]
    abbrev LO.Modal.Hilbert.GLPoint3 :
    Hilbert ℕ
    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
    source
    @[reducible, inline]
    abbrev LO.Modal.Logic.GLPoint3 :
    Logic
    Equations
    Instances For
    source
    instance LO.Modal.Hilbert.GLPoint3.instHasKNat :
    Hilbert.GLPoint3.HasK
    Equations
    source
    instance LO.Modal.Hilbert.GLPoint3.instHasLNat :
    Hilbert.GLPoint3.HasL
    Equations
    source
    instance LO.Modal.Hilbert.GLPoint3.instHasWeakPoint3Nat :
    Hilbert.GLPoint3.HasWeakPoint3
    Equations
    source
    instance LO.Modal.Hilbert.GLPoint3.instGLPoint3NatFormula :
    Entailment.GLPoint3 Hilbert.GLPoint3
    Equations
    • One or more equations did not get rendered due to their size.
    source
    @[reducible, inline]
    abbrev LO.Modal.Hilbert.KH :
    Hilbert ℕ
    Equations
    Instances For
    source
    @[reducible, inline]
    abbrev LO.Modal.Logic.KH :
    Logic
    Equations
    source
    instance LO.Modal.Hilbert.KH.instHasKNat :
    Hilbert.KH.HasK
    Equations
    source
    instance LO.Modal.Hilbert.KH.instHasHNat :
    Hilbert.KH.HasH
    Equations
    source
    @[reducible, inline]
    abbrev LO.Modal.Hilbert.Grz :
    Hilbert ℕ
    Equations
    Instances For
    source
    @[reducible, inline]
    abbrev LO.Modal.Logic.Grz :
    Logic
    Equations
    Instances For
    source
    instance LO.Modal.Hilbert.Grz.instHasKNat :
    Hilbert.Grz.HasK
    Equations
    source
    instance LO.Modal.Hilbert.Grz.instHasGrzNat :
    Hilbert.Grz.HasGrz
    Equations
    source
    instance LO.Modal.Hilbert.Grz.instGrzNatFormula :
    Entailment.Grz Hilbert.Grz
    Equations
    • One or more equations did not get rendered due to their size.
    source
    theorem LO.Modal.Hilbert.KT_weakerThan_Grz :
    Hilbert.KT ⪯ Hilbert.Grz
    source
    @[reducible, inline]
    abbrev LO.Modal.Hilbert.GrzPoint2 :
    Hilbert ℕ
    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
    source
    @[reducible, inline]
    abbrev LO.Modal.Logic.GrzPoint2 :
    Logic
    Equations
    Instances For
    source
    instance LO.Modal.Hilbert.GrzPoint2.instHasKNat :
    Hilbert.GrzPoint2.HasK
    Equations
    source
    instance LO.Modal.Hilbert.GrzPoint2.instHasGrzNat :
    Hilbert.GrzPoint2.HasGrz
    Equations
    source
    instance LO.Modal.Hilbert.GrzPoint2.instHasPoint2Nat :
    Hilbert.GrzPoint2.HasPoint2
    Equations
    source
    instance LO.Modal.Hilbert.GrzPoint2.instGrzNatFormula :
    Entailment.Grz Hilbert.GrzPoint2
    Equations
    • One or more equations did not get rendered due to their size.
    source
    @[reducible, inline]
    abbrev LO.Modal.Hilbert.GrzPoint3 :
    Hilbert ℕ
    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
    source
    @[reducible, inline]
    abbrev LO.Modal.Logic.GrzPoint3 :
    Logic
    Equations
    Instances For
    source
    instance LO.Modal.Hilbert.GrzPoint3.instHasKNat :
    Hilbert.GrzPoint3.HasK
    Equations
    source
    instance LO.Modal.Hilbert.GrzPoint3.instHasGrzNat :
    Hilbert.GrzPoint3.HasGrz
    Equations
    source
    instance LO.Modal.Hilbert.GrzPoint3.instHasPoint3Nat :
    Hilbert.GrzPoint3.HasPoint3
    Equations
    source
    instance LO.Modal.Hilbert.GrzPoint3.instGrzNatFormula :
    Entailment.Grz Hilbert.GrzPoint3
    Equations
    • One or more equations did not get rendered due to their size.
    source
    @[reducible, inline]
    abbrev LO.Modal.Hilbert.Ver :
    Hilbert ℕ
    Equations
    Instances For
    source
    @[reducible, inline]
    abbrev LO.Modal.Logic.Ver :
    Logic
    Equations
    Instances For
    source
    instance LO.Modal.Hilbert.Ver.instHasKNat :
    Hilbert.Ver.HasK
    Equations
    source
    instance LO.Modal.Hilbert.Ver.instHasVerNat :
    Hilbert.Ver.HasVer
    Equations
    source
    instance LO.Modal.Hilbert.Ver.instVerNatFormula :
    Entailment.Ver Hilbert.Ver
    Equations
    • One or more equations did not get rendered due to their size.
    source
    @[reducible, inline]
    abbrev LO.Modal.Hilbert.Triv :
    Hilbert ℕ
    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
    source
    @[reducible, inline]
    abbrev LO.Modal.Logic.Triv :
    Logic
    Equations
    Instances For
    source
    instance LO.Modal.Hilbert.Triv.instHasKNat :
    Hilbert.Triv.HasK
    Equations
    source
    instance LO.Modal.Hilbert.Triv.instHasTNat :
    Hilbert.Triv.HasT
    Equations
    source
    instance LO.Modal.Hilbert.Triv.instHasTcNat :
    Hilbert.Triv.HasTc
    Equations
    source
    instance LO.Modal.Hilbert.Triv.instTrivNatFormula :
    Entailment.Triv Hilbert.Triv
    Equations
    • One or more equations did not get rendered due to their size.
    source
    theorem LO.Modal.Hilbert.K4_weakerThan_Triv :
    Hilbert.K4 ⪯ Hilbert.Triv
    source
    @[reducible, inline]
    abbrev LO.Modal.Hilbert.KTc :
    Hilbert ℕ
    Equations
    Instances For
    source
    @[reducible, inline]
    abbrev LO.Modal.Logic.KTc :
    Logic
    Equations
    source
    instance LO.Modal.Hilbert.KTc.instHasKNat :
    Hilbert.KTc.HasK
    Equations
    source
    instance LO.Modal.Hilbert.KTc.instHasTcNat :
    Hilbert.KTc.HasTc
    Equations
    source
    instance LO.Modal.Hilbert.KTc.instKTcNatFormula :
    Entailment.KTc Hilbert.KTc
    Equations
    • One or more equations did not get rendered due to their size.
    source
    @[reducible, inline]
    abbrev LO.Modal.Hilbert.KD4Point3Z :
    Hilbert ℕ
    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
    source
    @[reducible, inline]
    abbrev LO.Modal.Logic.KD4Point3Z :
    Logic
    Equations
    source
    instance LO.Modal.Hilbert.KD4Point3Z.instHasKNat :
    Hilbert.KD4Point3Z.HasK
    Equations
    source
    instance LO.Modal.Hilbert.KD4Point3Z.instHasDNat :
    Hilbert.KD4Point3Z.HasD
    Equations
    source
    instance LO.Modal.Hilbert.KD4Point3Z.instHasFourNat :
    Hilbert.KD4Point3Z.HasFour
    Equations
    source
    instance LO.Modal.Hilbert.KD4Point3Z.instHasWeakPoint3Nat :
    Hilbert.KD4Point3Z.HasWeakPoint3
    Equations
    • One or more equations did not get rendered due to their size.
    source
    instance LO.Modal.Hilbert.KD4Point3Z.instHasZNat :
    Hilbert.KD4Point3Z.HasZ
    Equations
    source
    instance LO.Modal.Hilbert.KD4Point3Z.instKD4Point3ZNatFormula :
    Entailment.KD4Point3Z Hilbert.KD4Point3Z
    Equations
    • One or more equations did not get rendered due to their size.
    source
    @[reducible, inline]
    abbrev LO.Modal.Hilbert.KTMk :
    Hilbert ℕ
    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
    source
    @[reducible, inline]
    abbrev LO.Modal.Logic.KTMk :
    Logic
    Equations
    source
    instance LO.Modal.Hilbert.KTMk.instHasKNat :
    Hilbert.KTMk.HasK
    Equations
    source
    instance LO.Modal.Hilbert.KTMk.instHasTNat :
    Hilbert.KTMk.HasT
    Equations
    source
    instance LO.Modal.Hilbert.KTMk.instHasMkNat :
    Hilbert.KTMk.HasMk
    Equations
    source
    instance LO.Modal.Hilbert.KTMk.instKTMkNatFormula :
    Entailment.KTMk Hilbert.KTMk
    Equations
    • One or more equations did not get rendered due to their size.
    source
    @[reducible, inline]
    abbrev LO.Modal.Hilbert.N :
    Hilbert ℕ
    Equations
    Instances For
    source
    @[reducible, inline]
    abbrev LO.Modal.Logic.N :
    Logic
    Equations