Documentation

Foundation.Modal.Axioms

@[reducible, inline]
abbrev LO.Axioms.DiaDuality {F : Type u_1} [BasicModalLogicalConnective F] (φ : F) [Dia F] :
F

is duality of .

Equations
@[reducible, inline]
Equations
@[reducible, inline]
abbrev LO.Axioms.K {F : Type u_1} [BasicModalLogicalConnective F] (φ ψ : F) :
F
Equations
@[reducible, inline]
Equations
Instances For
@[reducible, inline]
abbrev LO.Axioms.T {F : Type u_1} [BasicModalLogicalConnective F] (φ : F) :
F
Equations
@[reducible, inline]
Equations
@[reducible, inline]
abbrev LO.Axioms.B {F : Type u_1} [BasicModalLogicalConnective F] (φ : F) [Dia F] :
F
Equations
@[reducible, inline]
Equations
@[reducible, inline]
abbrev LO.Axioms.B₂ {F : Type u_1} [BasicModalLogicalConnective F] (φ : F) :
F

-only version of axiom 𝗕.

Equations
@[reducible, inline]
Equations
@[reducible, inline]
abbrev LO.Axioms.D {F : Type u_1} [BasicModalLogicalConnective F] (φ : F) [Dia F] :
F
Equations
@[reducible, inline]
Equations
@[reducible, inline]
Equations
@[reducible, inline]
Equations
@[reducible, inline]
abbrev LO.Axioms.Four {F : Type u_1} [BasicModalLogicalConnective F] (φ : F) :
F
Equations
@[reducible, inline]
Equations
@[reducible, inline]
abbrev LO.Axioms.Five {F : Type u_1} [BasicModalLogicalConnective F] (φ : F) [Dia F] :
F
Equations
@[reducible, inline]
Equations
@[reducible, inline]
abbrev LO.Axioms.Five₂ {F : Type u_1} [BasicModalLogicalConnective F] (φ : F) :
F

-only version of axiom 𝟱.

Equations
@[reducible, inline]
Equations
@[reducible, inline]
abbrev LO.Axioms.Dot2 {F : Type u_1} [BasicModalLogicalConnective F] (φ : F) [Dia F] :
F
Equations
@[reducible, inline]
Equations
@[reducible, inline]
abbrev LO.Axioms.C4 {F : Type u_1} [BasicModalLogicalConnective F] (φ : F) :
F
Equations
@[reducible, inline]
Equations
@[reducible, inline]
abbrev LO.Axioms.CD {F : Type u_1} [BasicModalLogicalConnective F] (φ : F) [Dia F] :
F
Equations
@[reducible, inline]
Equations
@[reducible, inline]
abbrev LO.Axioms.Tc {F : Type u_1} [BasicModalLogicalConnective F] (φ : F) :
F
Equations
@[reducible, inline]
Equations
@[reducible, inline]
abbrev LO.Axioms.Ver {F : Type u_1} [BasicModalLogicalConnective F] (φ : F) :
F
Equations
@[reducible, inline]
Equations
@[reducible, inline]
abbrev LO.Axioms.Dot3 {F : Type u_1} [BasicModalLogicalConnective F] (φ ψ : F) :
F
Equations
@[reducible, inline]
Equations
@[reducible, inline]
abbrev LO.Axioms.Grz {F : Type u_1} [BasicModalLogicalConnective F] (φ : F) :
F
Equations
@[reducible, inline]
Equations
Instances For
@[reducible, inline]
abbrev LO.Axioms.M {F : Type u_1} [BasicModalLogicalConnective F] (φ : F) [Dia F] :
F
Equations
@[reducible, inline]
Equations
@[reducible, inline]
abbrev LO.Axioms.L {F : Type u_1} [BasicModalLogicalConnective F] (φ : F) :
F
Equations
@[reducible, inline]
Equations
Instances For
@[reducible, inline]
abbrev LO.Axioms.H {F : Type u_1} [BasicModalLogicalConnective F] (φ : F) :
F
Equations
@[reducible, inline]
Equations
Instances For
@[reducible, inline]
Equations
@[reducible, inline]
Equations
Equations
  • One or more equations did not get rendered due to their size.
@[simp]
theorem LO.Axioms.T.is_geach {F : Type u_1} [BasicModalLogicalConnective F] :
𝗧 = 𝗴𝗲({ i := 0, j := 0, m := 1, n := 0 })
@[simp]
theorem LO.Axioms.B.is_geach {F : Type u_1} [BasicModalLogicalConnective F] :
𝗕 = 𝗴𝗲({ i := 0, j := 1, m := 0, n := 1 })
@[simp]
theorem LO.Axioms.D.is_geach {F : Type u_1} [BasicModalLogicalConnective F] :
𝗗 = 𝗴𝗲({ i := 0, j := 0, m := 1, n := 1 })
@[simp]
theorem LO.Axioms.Four.is_geach {F : Type u_1} [BasicModalLogicalConnective F] :
𝟰 = 𝗴𝗲({ i := 0, j := 2, m := 1, n := 0 })
@[simp]
theorem LO.Axioms.Five.is_geach {F : Type u_1} [BasicModalLogicalConnective F] :
𝟱 = 𝗴𝗲({ i := 1, j := 1, m := 0, n := 1 })
@[simp]
theorem LO.Axioms.Dot2.is_geach {F : Type u_1} [BasicModalLogicalConnective F] :
.𝟮 = 𝗴𝗲({ i := 1, j := 1, m := 1, n := 1 })
@[simp]
theorem LO.Axioms.C4.is_geach {F : Type u_1} [BasicModalLogicalConnective F] :
𝗖𝟰 = 𝗴𝗲({ i := 0, j := 1, m := 2, n := 0 })
@[simp]
theorem LO.Axioms.CD.is_geach {F : Type u_1} [BasicModalLogicalConnective F] :
𝗖𝗗 = 𝗴𝗲({ i := 1, j := 1, m := 0, n := 0 })
@[simp]
theorem LO.Axioms.Tc.is_geach {F : Type u_1} [BasicModalLogicalConnective F] :
𝗧𝗰 = 𝗴𝗲({ i := 0, j := 1, m := 0, n := 0 })
Equations
  • One or more equations did not get rendered due to their size.