class
LO.System.HasDiaDuality
{S : Type u_1}
{F : Type u_2}
[LO.LogicalConnective F]
[LO.BasicModalLogicalConnective F]
[LO.System F S]
(𝓢 : S)
:
Type (max u_2 u_3)
- dia_dual : (p : F) → 𝓢 ⊢ LO.Axioms.DiaDuality p
Instances
class
LO.System.Necessitation
{S : Type u_1}
{F : Type u_2}
[LO.BasicModalLogicalConnective F]
[LO.System F S]
(𝓢 : S)
:
Type (max u_2 u_3)
Instances
class
LO.System.Unnecessitation
{S : Type u_1}
{F : Type u_2}
[LO.BasicModalLogicalConnective F]
[LO.System F S]
(𝓢 : S)
:
Type (max u_2 u_3)
Instances
class
LO.System.LoebRule
{S : Type u_1}
{F : Type u_2}
[LO.LogicalConnective F]
[LO.BasicModalLogicalConnective F]
[LO.System F S]
(𝓢 : S)
:
Type (max u_2 u_3)
Instances
class
LO.System.HenkinRule
{S : Type u_1}
{F : Type u_2}
[LO.LogicalConnective F]
[LO.BasicModalLogicalConnective F]
[LO.System F S]
(𝓢 : S)
:
Type (max u_2 u_3)
Instances
class
LO.System.HasAxiomK
{S : Type u_1}
{F : Type u_2}
[LO.LogicalConnective F]
[LO.BasicModalLogicalConnective F]
[LO.System F S]
(𝓢 : S)
:
Type (max u_2 u_3)
- K : (p q : F) → 𝓢 ⊢ LO.Axioms.K p q
Instances
class
LO.System.HasAxiomT
{S : Type u_1}
{F : Type u_2}
[LO.LogicalConnective F]
[LO.BasicModalLogicalConnective F]
[LO.System F S]
(𝓢 : S)
:
Type (max u_2 u_3)
- T : (p : F) → 𝓢 ⊢ LO.Axioms.T p
Instances
class
LO.System.HasAxiomD
{S : Type u_1}
{F : Type u_2}
[LO.LogicalConnective F]
[LO.BasicModalLogicalConnective F]
[LO.System F S]
(𝓢 : S)
:
Type (max u_2 u_3)
- D : (p : F) → 𝓢 ⊢ LO.Axioms.D p
Instances
class
LO.System.HasAxiomP
{S : Type u_1}
{F : Type u_2}
[LO.LogicalConnective F]
[LO.BasicModalLogicalConnective F]
[LO.System F S]
(𝓢 : S)
:
Type u_3
- P : 𝓢 ⊢ LO.Axioms.P
Instances
class
LO.System.HasAxiomB
{S : Type u_1}
{F : Type u_2}
[LO.LogicalConnective F]
[LO.BasicModalLogicalConnective F]
[LO.System F S]
(𝓢 : S)
:
Type (max u_2 u_3)
- B : (p : F) → 𝓢 ⊢ LO.Axioms.B p
Instances
class
LO.System.HasAxiomFour
{S : Type u_1}
{F : Type u_2}
[LO.LogicalConnective F]
[LO.BasicModalLogicalConnective F]
[LO.System F S]
(𝓢 : S)
:
Type (max u_2 u_3)
- Four : (p : F) → 𝓢 ⊢ LO.Axioms.Four p
Instances
class
LO.System.HasAxiomFive
{S : Type u_1}
{F : Type u_2}
[LO.LogicalConnective F]
[LO.BasicModalLogicalConnective F]
[LO.System F S]
(𝓢 : S)
:
Type (max u_2 u_3)
- Five : (p : F) → 𝓢 ⊢ LO.Axioms.Five p
Instances
class
LO.System.HasAxiomL
{S : Type u_1}
{F : Type u_2}
[LO.LogicalConnective F]
[LO.BasicModalLogicalConnective F]
[LO.System F S]
(𝓢 : S)
:
Type (max u_2 u_3)
- L : (p : F) → 𝓢 ⊢ LO.Axioms.L p
Instances
class
LO.System.HasAxiomDot2
{S : Type u_1}
{F : Type u_2}
[LO.LogicalConnective F]
[LO.BasicModalLogicalConnective F]
[LO.System F S]
(𝓢 : S)
:
Type (max u_2 u_3)
- Dot2 : (p : F) → 𝓢 ⊢ LO.Axioms.Dot2 p
Instances
class
LO.System.HasAxiomDot3
{S : Type u_1}
{F : Type u_2}
[LO.LogicalConnective F]
[LO.BasicModalLogicalConnective F]
[LO.System F S]
(𝓢 : S)
:
Type (max u_2 u_3)
- Dot3 : (p q : F) → 𝓢 ⊢ LO.Axioms.Dot3 p q
Instances
class
LO.System.HasAxiomGrz
{S : Type u_1}
{F : Type u_2}
[LO.LogicalConnective F]
[LO.BasicModalLogicalConnective F]
[LO.System F S]
(𝓢 : S)
:
Type (max u_2 u_3)
- Grz : (p : F) → 𝓢 ⊢ LO.Axioms.Grz p
Instances
class
LO.System.HasAxiomTc
{S : Type u_1}
{F : Type u_2}
[LO.LogicalConnective F]
[LO.BasicModalLogicalConnective F]
[LO.System F S]
(𝓢 : S)
:
Type (max u_2 u_3)
- Tc : (p : F) → 𝓢 ⊢ LO.Axioms.Tc p
Instances
class
LO.System.HasAxiomVer
{S : Type u_1}
{F : Type u_2}
[LO.BasicModalLogicalConnective F]
[LO.System F S]
(𝓢 : S)
:
Type (max u_2 u_3)
- Ver : (p : F) → 𝓢 ⊢ LO.Axioms.Ver p
Instances
class
LO.System.HasAxiomH
{S : Type u_1}
{F : Type u_2}
[LO.LogicalConnective F]
[LO.BasicModalLogicalConnective F]
[LO.System F S]
(𝓢 : S)
:
Type (max u_2 u_3)
- H : (p : F) → 𝓢 ⊢ LO.Axioms.H p
Instances
class
LO.System.K
{S : Type u_1}
{F : Type u_2}
[LO.LogicalConnective F]
[LO.BasicModalLogicalConnective F]
[LO.System F S]
(𝓢 : S)
extends
LO.System.Classical
,
LO.System.Necessitation
,
LO.System.HasAxiomK
,
LO.System.HasDiaDuality
:
Type (max u_2 u_3)
Instances
class
LO.System.KT
{S : Type u_1}
{F : Type u_2}
[LO.LogicalConnective F]
[LO.BasicModalLogicalConnective F]
[LO.System F S]
(𝓢 : S)
extends
LO.System.K
,
LO.System.HasAxiomT
:
Type (max u_2 u_3)
Instances
class
LO.System.KD
{S : Type u_1}
{F : Type u_2}
[LO.LogicalConnective F]
[LO.BasicModalLogicalConnective F]
[LO.System F S]
(𝓢 : S)
extends
LO.System.K
,
LO.System.HasAxiomD
:
Type (max u_2 u_3)
Instances
class
LO.System.K4
{S : Type u_1}
{F : Type u_2}
[LO.LogicalConnective F]
[LO.BasicModalLogicalConnective F]
[LO.System F S]
(𝓢 : S)
extends
LO.System.K
,
LO.System.HasAxiomFour
:
Type (max u_2 u_3)
Instances
class
LO.System.S4
{S : Type u_1}
{F : Type u_2}
[LO.LogicalConnective F]
[LO.BasicModalLogicalConnective F]
[LO.System F S]
(𝓢 : S)
extends
LO.System.K
,
LO.System.HasAxiomT
,
LO.System.HasAxiomFour
:
Type (max u_2 u_3)
Instances
class
LO.System.S5
{S : Type u_1}
{F : Type u_2}
[LO.LogicalConnective F]
[LO.BasicModalLogicalConnective F]
[LO.System F S]
(𝓢 : S)
extends
LO.System.K
,
LO.System.HasAxiomT
,
LO.System.HasAxiomFive
:
Type (max u_2 u_3)
Instances
class
LO.System.S4Dot2
{S : Type u_1}
{F : Type u_2}
[LO.LogicalConnective F]
[LO.BasicModalLogicalConnective F]
[LO.System F S]
(𝓢 : S)
extends
LO.System.S4
,
LO.System.HasAxiomDot2
:
Type (max u_2 u_3)
Instances
class
LO.System.S4Dot3
{S : Type u_1}
{F : Type u_2}
[LO.LogicalConnective F]
[LO.BasicModalLogicalConnective F]
[LO.System F S]
(𝓢 : S)
extends
LO.System.S4
,
LO.System.HasAxiomDot3
:
Type (max u_2 u_3)
Instances
class
LO.System.S4Grz
{S : Type u_1}
{F : Type u_2}
[LO.LogicalConnective F]
[LO.BasicModalLogicalConnective F]
[LO.System F S]
(𝓢 : S)
extends
LO.System.S4
,
LO.System.HasAxiomGrz
:
Type (max u_2 u_3)
Instances
class
LO.System.GL
{S : Type u_1}
{F : Type u_2}
[LO.LogicalConnective F]
[LO.BasicModalLogicalConnective F]
[LO.System F S]
(𝓢 : S)
extends
LO.System.K
,
LO.System.HasAxiomL
:
Type (max u_2 u_3)
Instances
class
LO.System.Grz
{S : Type u_1}
{F : Type u_2}
[LO.LogicalConnective F]
[LO.BasicModalLogicalConnective F]
[LO.System F S]
(𝓢 : S)
extends
LO.System.K
,
LO.System.HasAxiomGrz
:
Type (max u_2 u_3)
Instances
class
LO.System.Triv
{S : Type u_1}
{F : Type u_2}
[LO.LogicalConnective F]
[LO.BasicModalLogicalConnective F]
[LO.System F S]
(𝓢 : S)
extends
LO.System.K
,
LO.System.HasAxiomT
,
LO.System.HasAxiomTc
:
Type (max u_2 u_3)
Instances
class
LO.System.Ver
{S : Type u_1}
{F : Type u_2}
[LO.LogicalConnective F]
[LO.BasicModalLogicalConnective F]
[LO.System F S]
(𝓢 : S)
extends
LO.System.K
,
LO.System.HasAxiomVer
:
Type (max u_2 u_3)
Instances
class
LO.System.K4H
{S : Type u_1}
{F : Type u_2}
[LO.LogicalConnective F]
[LO.BasicModalLogicalConnective F]
[LO.System F S]
(𝓢 : S)
extends
LO.System.K4
,
LO.System.HasAxiomH
:
Type (max u_2 u_3)
Instances
class
LO.System.K4Loeb
{S : Type u_1}
{F : Type u_2}
[LO.LogicalConnective F]
[LO.BasicModalLogicalConnective F]
[LO.System F S]
(𝓢 : S)
extends
LO.System.K4
,
LO.System.LoebRule
:
Type (max u_2 u_3)
Instances
class
LO.System.K4Henkin
{S : Type u_1}
{F : Type u_2}
[LO.LogicalConnective F]
[LO.BasicModalLogicalConnective F]
[LO.System F S]
(𝓢 : S)
extends
LO.System.K4
,
LO.System.HenkinRule
:
Type (max u_2 u_3)
Instances
def
LO.System.nec
{S : Type u_1}
{F : Type u_2}
[LO.BasicModalLogicalConnective F]
[LO.System F S]
{𝓢 : S}
[self : LO.System.Necessitation 𝓢]
{p : F}
:
Alias of LO.System.Necessitation.nec
.
Equations
Instances For
theorem
LO.System.nec!
{F : Type u_1}
[LO.BasicModalLogicalConnective F]
{S : Type u_2}
[LO.System F S]
{p : F}
{𝓢 : S}
[LO.System.Necessitation 𝓢]
:
def
LO.System.multinec
{F : Type u_1}
[LO.BasicModalLogicalConnective F]
{S : Type u_2}
[LO.System F S]
{p : F}
{𝓢 : S}
[LO.System.Necessitation 𝓢]
{n : ℕ}
:
Equations
- LO.System.multinec h = Nat.recAux (id h) (fun (n : ℕ) (ih : 𝓢 ⊢ □^[n]p) => ⋯.mpr (LO.System.nec ih)) n
Instances For
theorem
LO.System.multinec!
{F : Type u_1}
[LO.BasicModalLogicalConnective F]
{S : Type u_2}
[LO.System F S]
{p : F}
{𝓢 : S}
[LO.System.Necessitation 𝓢]
{n : ℕ}
:
def
LO.System.axiomK
{F : Type u_1}
[LO.BasicModalLogicalConnective F]
{S : Type u_2}
[LO.System F S]
{p : F}
{q : F}
{𝓢 : S}
[LO.System.HasAxiomK 𝓢]
:
Equations
- LO.System.axiomK = LO.System.HasAxiomK.K p q
Instances For
@[simp]
theorem
LO.System.axiomK!
{F : Type u_1}
[LO.BasicModalLogicalConnective F]
{S : Type u_2}
[LO.System F S]
{p : F}
{q : F}
{𝓢 : S}
[LO.System.HasAxiomK 𝓢]
:
instance
LO.System.instHasAxiomKFiniteContext
{F : Type u_1}
[LO.BasicModalLogicalConnective F]
{S : Type u_2}
[LO.System F S]
{𝓢 : S}
[LO.System.Classical 𝓢]
[LO.System.HasAxiomK 𝓢]
(Γ : LO.System.FiniteContext F 𝓢)
:
Equations
- LO.System.instHasAxiomKFiniteContext Γ = { K := fun (x x_1 : F) => LO.System.FiniteContext.of LO.System.axiomK }
instance
LO.System.instHasAxiomKContext
{F : Type u_1}
[LO.BasicModalLogicalConnective F]
{S : Type u_2}
[LO.System F S]
{𝓢 : S}
[LO.System.Classical 𝓢]
[LO.System.HasAxiomK 𝓢]
(Γ : LO.System.Context F 𝓢)
:
Equations
- LO.System.instHasAxiomKContext Γ = { K := fun (x x_1 : F) => LO.System.Context.of LO.System.axiomK }
def
LO.System.axiomK'
{F : Type u_1}
[LO.BasicModalLogicalConnective F]
{S : Type u_2}
[LO.System F S]
{p : F}
{q : F}
{𝓢 : S}
[LO.System.Classical 𝓢]
[LO.System.HasAxiomK 𝓢]
(h : 𝓢 ⊢ □(p ➝ q))
:
Equations
- LO.System.axiomK' h = LO.System.axiomK⨀h
Instances For
@[simp]
theorem
LO.System.axiomK'!
{F : Type u_1}
[LO.BasicModalLogicalConnective F]
{S : Type u_2}
[LO.System F S]
{p : F}
{q : F}
{𝓢 : S}
[LO.System.Classical 𝓢]
[LO.System.HasAxiomK 𝓢]
(h : 𝓢 ⊢! □(p ➝ q))
:
def
LO.System.axiomK''
{F : Type u_1}
[LO.BasicModalLogicalConnective F]
{S : Type u_2}
[LO.System F S]
{p : F}
{q : F}
{𝓢 : S}
[LO.System.Classical 𝓢]
[LO.System.HasAxiomK 𝓢]
(h₁ : 𝓢 ⊢ □(p ➝ q))
(h₂ : 𝓢 ⊢ □p)
:
Equations
- LO.System.axiomK'' h₁ h₂ = LO.System.axiomK' h₁⨀h₂
Instances For
@[simp]
theorem
LO.System.axiomK''!
{F : Type u_1}
[LO.BasicModalLogicalConnective F]
{S : Type u_2}
[LO.System F S]
{p : F}
{q : F}
{𝓢 : S}
[LO.System.Classical 𝓢]
[LO.System.HasAxiomK 𝓢]
(h₁ : 𝓢 ⊢! □(p ➝ q))
(h₂ : 𝓢 ⊢! □p)
:
def
LO.System.multibox_axiomK
{F : Type u_1}
[LO.BasicModalLogicalConnective F]
{S : Type u_2}
[LO.System F S]
{p : F}
{q : F}
{𝓢 : S}
[LO.System.Classical 𝓢]
[LO.System.Necessitation 𝓢]
[LO.System.HasAxiomK 𝓢]
{n : ℕ}
:
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
LO.System.multibox_axiomK!
{F : Type u_1}
[LO.BasicModalLogicalConnective F]
{S : Type u_2}
[LO.System F S]
{p : F}
{q : F}
{𝓢 : S}
[LO.System.Classical 𝓢]
[LO.System.Necessitation 𝓢]
[LO.System.HasAxiomK 𝓢]
{n : ℕ}
:
def
LO.System.multibox_axiomK'
{F : Type u_1}
[LO.BasicModalLogicalConnective F]
{S : Type u_2}
[LO.System F S]
{p : F}
{q : F}
{𝓢 : S}
[LO.System.Classical 𝓢]
[LO.System.Necessitation 𝓢]
[LO.System.HasAxiomK 𝓢]
{n : ℕ}
(h : 𝓢 ⊢ □^[n](p ➝ q))
:
Equations
- LO.System.multibox_axiomK' h = LO.System.multibox_axiomK⨀h
Instances For
@[simp]
theorem
LO.System.multibox_axiomK'!
{F : Type u_1}
[LO.BasicModalLogicalConnective F]
{S : Type u_2}
[LO.System F S]
{p : F}
{q : F}
{𝓢 : S}
[LO.System.Classical 𝓢]
[LO.System.Necessitation 𝓢]
[LO.System.HasAxiomK 𝓢]
{n : ℕ}
(h : 𝓢 ⊢! □^[n](p ➝ q))
:
def
LO.System.multiboxedImplyDistribute
{F : Type u_1}
[LO.BasicModalLogicalConnective F]
{S : Type u_2}
[LO.System F S]
{p : F}
{q : F}
{𝓢 : S}
[LO.System.Classical 𝓢]
[LO.System.Necessitation 𝓢]
[LO.System.HasAxiomK 𝓢]
{n : ℕ}
(h : 𝓢 ⊢ □^[n](p ➝ q))
:
Alias of LO.System.multibox_axiomK'
.
Instances For
theorem
LO.System.multiboxed_imply_distribute!
{F : Type u_1}
[LO.BasicModalLogicalConnective F]
{S : Type u_2}
[LO.System F S]
{p : F}
{q : F}
{𝓢 : S}
[LO.System.Classical 𝓢]
[LO.System.Necessitation 𝓢]
[LO.System.HasAxiomK 𝓢]
{n : ℕ}
(h : 𝓢 ⊢! □^[n](p ➝ q))
:
Alias of LO.System.multibox_axiomK'!
.
def
LO.System.boxIff'
{F : Type u_1}
[LO.BasicModalLogicalConnective F]
{S : Type u_2}
[LO.System F S]
{p : F}
{q : F}
{𝓢 : S}
[LO.System.Classical 𝓢]
[LO.System.Necessitation 𝓢]
[LO.System.HasAxiomK 𝓢]
(h : 𝓢 ⊢ p ⭤ q)
:
Equations
Instances For
@[simp]
theorem
LO.System.box_iff!
{F : Type u_1}
[LO.BasicModalLogicalConnective F]
{S : Type u_2}
[LO.System F S]
{p : F}
{q : F}
{𝓢 : S}
[LO.System.Classical 𝓢]
[LO.System.Necessitation 𝓢]
[LO.System.HasAxiomK 𝓢]
(h : 𝓢 ⊢! p ⭤ q)
:
def
LO.System.multiboxIff'
{F : Type u_1}
[LO.BasicModalLogicalConnective F]
{S : Type u_2}
[LO.System F S]
{p : F}
{q : F}
{𝓢 : S}
[LO.System.Classical 𝓢]
[LO.System.Necessitation 𝓢]
[LO.System.HasAxiomK 𝓢]
{n : ℕ}
(h : 𝓢 ⊢ p ⭤ q)
:
Equations
- LO.System.multiboxIff' h = Nat.recAux (id h) (fun (n : ℕ) (ih : 𝓢 ⊢ □^[n]p ⭤ □^[n]q) => ⋯.mpr (LO.System.boxIff' ih)) n
Instances For
@[simp]
theorem
LO.System.multibox_iff!
{F : Type u_1}
[LO.BasicModalLogicalConnective F]
{S : Type u_2}
[LO.System F S]
{p : F}
{q : F}
{𝓢 : S}
[LO.System.Classical 𝓢]
[LO.System.Necessitation 𝓢]
[LO.System.HasAxiomK 𝓢]
{n : ℕ}
(h : 𝓢 ⊢! p ⭤ q)
:
instance
LO.System.instHasDiaDualityOfModalDeMorganOfHasAxiomDNE
{F : Type u_1}
[LO.BasicModalLogicalConnective F]
{S : Type u_2}
[LO.System F S]
{𝓢 : S}
[LO.System.Classical 𝓢]
[LO.ModalDeMorgan F]
[LO.System.HasAxiomDNE 𝓢]
:
Equations
- LO.System.instHasDiaDualityOfModalDeMorganOfHasAxiomDNE = { dia_dual := fun (p : F) => ⋯.mpr (LO.System.iffId (◇p)) }
instance
LO.System.instHasDiaDualityOfDiaAbbrev
{F : Type u_1}
[LO.BasicModalLogicalConnective F]
{S : Type u_2}
[LO.System F S]
{𝓢 : S}
[LO.System.Classical 𝓢]
[LO.DiaAbbrev F]
:
Equations
- LO.System.instHasDiaDualityOfDiaAbbrev = { dia_dual := fun (p : F) => ⋯.mpr (LO.System.iffId (∼□(∼p))) }
def
LO.System.diaDuality
{F : Type u_1}
[LO.BasicModalLogicalConnective F]
{S : Type u_2}
[LO.System F S]
{p : F}
{𝓢 : S}
[LO.System.HasDiaDuality 𝓢]
:
Equations
- LO.System.diaDuality = LO.System.HasDiaDuality.dia_dual p
Instances For
@[simp]
theorem
LO.System.dia_duality!
{F : Type u_1}
[LO.BasicModalLogicalConnective F]
{S : Type u_2}
[LO.System F S]
{p : F}
{𝓢 : S}
[LO.System.HasDiaDuality 𝓢]
:
def
LO.System.diaDuality_mp
{F : Type u_1}
[LO.BasicModalLogicalConnective F]
{S : Type u_2}
[LO.System F S]
{p : F}
{𝓢 : S}
[LO.System.Classical 𝓢]
[LO.System.HasDiaDuality 𝓢]
:
Equations
- LO.System.diaDuality_mp = LO.System.and₁' LO.System.diaDuality
Instances For
@[simp]
theorem
LO.System.diaDuality_mp!
{F : Type u_1}
[LO.BasicModalLogicalConnective F]
{S : Type u_2}
[LO.System F S]
{p : F}
{𝓢 : S}
[LO.System.Classical 𝓢]
[LO.System.HasDiaDuality 𝓢]
:
def
LO.System.diaDuality_mpr
{F : Type u_1}
[LO.BasicModalLogicalConnective F]
{S : Type u_2}
[LO.System F S]
{p : F}
{𝓢 : S}
[LO.System.Classical 𝓢]
[LO.System.HasDiaDuality 𝓢]
:
Equations
- LO.System.diaDuality_mpr = LO.System.and₂' LO.System.diaDuality
Instances For
@[simp]
theorem
LO.System.diaDuality_mpr!
{F : Type u_1}
[LO.BasicModalLogicalConnective F]
{S : Type u_2}
[LO.System F S]
{p : F}
{𝓢 : S}
[LO.System.Classical 𝓢]
[LO.System.HasDiaDuality 𝓢]
:
def
LO.System.diaDuality'.mp
{F : Type u_1}
[LO.BasicModalLogicalConnective F]
{S : Type u_2}
[LO.System F S]
{p : F}
{𝓢 : S}
[LO.System.Classical 𝓢]
[LO.System.HasDiaDuality 𝓢]
(h : 𝓢 ⊢ ◇p)
:
Equations
- LO.System.diaDuality'.mp h = LO.System.and₁' LO.System.diaDuality⨀h
Instances For
def
LO.System.diaDuality'.mpr
{F : Type u_1}
[LO.BasicModalLogicalConnective F]
{S : Type u_2}
[LO.System F S]
{p : F}
{𝓢 : S}
[LO.System.Classical 𝓢]
[LO.System.HasDiaDuality 𝓢]
(h : 𝓢 ⊢ ∼□(∼p))
:
Equations
- LO.System.diaDuality'.mpr h = LO.System.and₂' LO.System.diaDuality⨀h
Instances For
theorem
LO.System.dia_duality'!
{F : Type u_1}
[LO.BasicModalLogicalConnective F]
{S : Type u_2}
[LO.System F S]
{p : F}
{𝓢 : S}
[LO.System.Classical 𝓢]
[LO.System.HasDiaDuality 𝓢]
:
def
LO.System.multiDiaDuality
{F : Type u_1}
[LO.BasicModalLogicalConnective F]
[DecidableEq F]
{S : Type u_2}
[LO.System F S]
{p : F}
{𝓢 : S}
[LO.System.Classical 𝓢]
[LO.System.NegationEquiv 𝓢]
[LO.System.Necessitation 𝓢]
[LO.System.HasAxiomK 𝓢]
[LO.System.HasDiaDuality 𝓢]
{n : ℕ}
:
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
LO.System.multidia_duality!
{F : Type u_1}
[LO.BasicModalLogicalConnective F]
[DecidableEq F]
{S : Type u_2}
[LO.System F S]
{p : F}
{𝓢 : S}
[LO.System.Classical 𝓢]
[LO.System.NegationEquiv 𝓢]
[LO.System.Necessitation 𝓢]
[LO.System.HasAxiomK 𝓢]
[LO.System.HasDiaDuality 𝓢]
{n : ℕ}
:
theorem
LO.System.multidia_duality'!
{F : Type u_1}
[LO.BasicModalLogicalConnective F]
[DecidableEq F]
{S : Type u_2}
[LO.System F S]
{p : F}
{𝓢 : S}
[LO.System.Classical 𝓢]
[LO.System.NegationEquiv 𝓢]
[LO.System.Necessitation 𝓢]
[LO.System.HasAxiomK 𝓢]
[LO.System.HasDiaDuality 𝓢]
{n : ℕ}
:
def
LO.System.diaIff'
{F : Type u_1}
[LO.BasicModalLogicalConnective F]
[DecidableEq F]
{S : Type u_2}
[LO.System F S]
{p : F}
{q : F}
{𝓢 : S}
[LO.System.Classical 𝓢]
[LO.System.NegationEquiv 𝓢]
[LO.System.Necessitation 𝓢]
[LO.System.HasAxiomK 𝓢]
[LO.System.HasDiaDuality 𝓢]
(h : 𝓢 ⊢ p ⭤ q)
:
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
LO.System.dia_iff!
{F : Type u_1}
[LO.BasicModalLogicalConnective F]
[DecidableEq F]
{S : Type u_2}
[LO.System F S]
{p : F}
{q : F}
{𝓢 : S}
[LO.System.Classical 𝓢]
[LO.System.NegationEquiv 𝓢]
[LO.System.Necessitation 𝓢]
[LO.System.HasAxiomK 𝓢]
[LO.System.HasDiaDuality 𝓢]
(h : 𝓢 ⊢! p ⭤ q)
:
def
LO.System.multidiaIff'
{F : Type u_1}
[LO.BasicModalLogicalConnective F]
[DecidableEq F]
{S : Type u_2}
[LO.System F S]
{p : F}
{q : F}
{𝓢 : S}
[LO.System.Classical 𝓢]
[LO.System.NegationEquiv 𝓢]
[LO.System.Necessitation 𝓢]
[LO.System.HasAxiomK 𝓢]
[LO.System.HasDiaDuality 𝓢]
{n : ℕ}
(h : 𝓢 ⊢ p ⭤ q)
:
Equations
- LO.System.multidiaIff' h = Nat.recAux (id h) (fun (n : ℕ) (ih : 𝓢 ⊢ ◇^[n]p ⭤ ◇^[n]q) => ⋯.mpr (LO.System.diaIff' ih)) n
Instances For
@[simp]
theorem
LO.System.multidia_iff!
{F : Type u_1}
[LO.BasicModalLogicalConnective F]
[DecidableEq F]
{S : Type u_2}
[LO.System F S]
{p : F}
{q : F}
{𝓢 : S}
[LO.System.Classical 𝓢]
[LO.System.NegationEquiv 𝓢]
[LO.System.Necessitation 𝓢]
[LO.System.HasAxiomK 𝓢]
[LO.System.HasDiaDuality 𝓢]
{n : ℕ}
(h : 𝓢 ⊢! p ⭤ q)
:
def
LO.System.multiboxDuality
{F : Type u_1}
[LO.BasicModalLogicalConnective F]
[DecidableEq F]
{S : Type u_2}
[LO.System F S]
{p : F}
{𝓢 : S}
[LO.System.Classical 𝓢]
[LO.System.NegationEquiv 𝓢]
[LO.System.Necessitation 𝓢]
[LO.System.HasAxiomK 𝓢]
[LO.System.HasDiaDuality 𝓢]
{n : ℕ}
:
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
LO.System.multibox_duality!
{F : Type u_1}
[LO.BasicModalLogicalConnective F]
[DecidableEq F]
{S : Type u_2}
[LO.System F S]
{p : F}
{𝓢 : S}
[LO.System.Classical 𝓢]
[LO.System.NegationEquiv 𝓢]
[LO.System.Necessitation 𝓢]
[LO.System.HasAxiomK 𝓢]
[LO.System.HasDiaDuality 𝓢]
{n : ℕ}
:
def
LO.System.boxDuality
{F : Type u_1}
[LO.BasicModalLogicalConnective F]
[DecidableEq F]
{S : Type u_2}
[LO.System F S]
{p : F}
{𝓢 : S}
[LO.System.Classical 𝓢]
[LO.System.NegationEquiv 𝓢]
[LO.System.Necessitation 𝓢]
[LO.System.HasAxiomK 𝓢]
[LO.System.HasDiaDuality 𝓢]
:
Equations
- LO.System.boxDuality = LO.System.multiboxDuality
Instances For
@[simp]
theorem
LO.System.box_duality!
{F : Type u_1}
[LO.BasicModalLogicalConnective F]
[DecidableEq F]
{S : Type u_2}
[LO.System F S]
{p : F}
{𝓢 : S}
[LO.System.Classical 𝓢]
[LO.System.NegationEquiv 𝓢]
[LO.System.Necessitation 𝓢]
[LO.System.HasAxiomK 𝓢]
[LO.System.HasDiaDuality 𝓢]
:
def
LO.System.boxDuality_mp
{F : Type u_1}
[LO.BasicModalLogicalConnective F]
[DecidableEq F]
{S : Type u_2}
[LO.System F S]
{p : F}
{𝓢 : S}
[LO.System.Classical 𝓢]
[LO.System.NegationEquiv 𝓢]
[LO.System.Necessitation 𝓢]
[LO.System.HasAxiomK 𝓢]
[LO.System.HasDiaDuality 𝓢]
:
Equations
- LO.System.boxDuality_mp = LO.System.and₁' LO.System.boxDuality
Instances For
@[simp]
theorem
LO.System.boxDuality_mp!
{F : Type u_1}
[LO.BasicModalLogicalConnective F]
[DecidableEq F]
{S : Type u_2}
[LO.System F S]
{p : F}
{𝓢 : S}
[LO.System.Classical 𝓢]
[LO.System.NegationEquiv 𝓢]
[LO.System.Necessitation 𝓢]
[LO.System.HasAxiomK 𝓢]
[LO.System.HasDiaDuality 𝓢]
:
def
LO.System.boxDuality_mp'
{F : Type u_1}
[LO.BasicModalLogicalConnective F]
[DecidableEq F]
{S : Type u_2}
[LO.System F S]
{p : F}
{𝓢 : S}
[LO.System.Classical 𝓢]
[LO.System.NegationEquiv 𝓢]
[LO.System.Necessitation 𝓢]
[LO.System.HasAxiomK 𝓢]
[LO.System.HasDiaDuality 𝓢]
(h : 𝓢 ⊢ □p)
:
Equations
- LO.System.boxDuality_mp' h = LO.System.boxDuality_mp⨀h
Instances For
theorem
LO.System.boxDuality_mp'!
{F : Type u_1}
[LO.BasicModalLogicalConnective F]
[DecidableEq F]
{S : Type u_2}
[LO.System F S]
{p : F}
{𝓢 : S}
[LO.System.Classical 𝓢]
[LO.System.NegationEquiv 𝓢]
[LO.System.Necessitation 𝓢]
[LO.System.HasAxiomK 𝓢]
[LO.System.HasDiaDuality 𝓢]
(h : 𝓢 ⊢! □p)
:
def
LO.System.boxDuality_mpr
{F : Type u_1}
[LO.BasicModalLogicalConnective F]
[DecidableEq F]
{S : Type u_2}
[LO.System F S]
{p : F}
{𝓢 : S}
[LO.System.Classical 𝓢]
[LO.System.NegationEquiv 𝓢]
[LO.System.Necessitation 𝓢]
[LO.System.HasAxiomK 𝓢]
[LO.System.HasDiaDuality 𝓢]
:
Equations
- LO.System.boxDuality_mpr = LO.System.and₂' LO.System.boxDuality
Instances For
@[simp]
theorem
LO.System.boxDuality_mpr!
{F : Type u_1}
[LO.BasicModalLogicalConnective F]
[DecidableEq F]
{S : Type u_2}
[LO.System F S]
{p : F}
{𝓢 : S}
[LO.System.Classical 𝓢]
[LO.System.NegationEquiv 𝓢]
[LO.System.Necessitation 𝓢]
[LO.System.HasAxiomK 𝓢]
[LO.System.HasDiaDuality 𝓢]
:
def
LO.System.boxDuality_mpr'
{F : Type u_1}
[LO.BasicModalLogicalConnective F]
[DecidableEq F]
{S : Type u_2}
[LO.System F S]
{p : F}
{𝓢 : S}
[LO.System.Classical 𝓢]
[LO.System.NegationEquiv 𝓢]
[LO.System.Necessitation 𝓢]
[LO.System.HasAxiomK 𝓢]
[LO.System.HasDiaDuality 𝓢]
(h : 𝓢 ⊢ ∼◇(∼p))
:
Equations
- LO.System.boxDuality_mpr' h = LO.System.boxDuality_mpr⨀h
Instances For
theorem
LO.System.boxDuality_mpr'!
{F : Type u_1}
[LO.BasicModalLogicalConnective F]
[DecidableEq F]
{S : Type u_2}
[LO.System F S]
{p : F}
{𝓢 : S}
[LO.System.Classical 𝓢]
[LO.System.NegationEquiv 𝓢]
[LO.System.Necessitation 𝓢]
[LO.System.HasAxiomK 𝓢]
[LO.System.HasDiaDuality 𝓢]
(h : 𝓢 ⊢! ∼◇(∼p))
:
theorem
LO.System.multibox_duality'!
{F : Type u_1}
[LO.BasicModalLogicalConnective F]
[DecidableEq F]
{S : Type u_2}
[LO.System F S]
{p : F}
{𝓢 : S}
[LO.System.Classical 𝓢]
[LO.System.NegationEquiv 𝓢]
[LO.System.Necessitation 𝓢]
[LO.System.HasAxiomK 𝓢]
[LO.System.HasDiaDuality 𝓢]
{n : ℕ}
:
theorem
LO.System.box_duality'!
{F : Type u_1}
[LO.BasicModalLogicalConnective F]
[DecidableEq F]
{S : Type u_2}
[LO.System F S]
{p : F}
{𝓢 : S}
[LO.System.Classical 𝓢]
[LO.System.NegationEquiv 𝓢]
[LO.System.Necessitation 𝓢]
[LO.System.HasAxiomK 𝓢]
[LO.System.HasDiaDuality 𝓢]
:
def
LO.System.box_dne
{F : Type u_1}
[LO.BasicModalLogicalConnective F]
{S : Type u_2}
[LO.System F S]
{p : F}
{𝓢 : S}
[LO.System.Classical 𝓢]
[LO.System.Necessitation 𝓢]
[LO.System.HasAxiomK 𝓢]
:
Equations
- LO.System.box_dne = LO.System.axiomK' (LO.System.nec LO.System.dne)
Instances For
@[simp]
theorem
LO.System.box_dne!
{F : Type u_1}
[LO.BasicModalLogicalConnective F]
{S : Type u_2}
[LO.System F S]
{p : F}
{𝓢 : S}
[LO.System.Classical 𝓢]
[LO.System.Necessitation 𝓢]
[LO.System.HasAxiomK 𝓢]
:
def
LO.System.box_dne'
{F : Type u_1}
[LO.BasicModalLogicalConnective F]
{S : Type u_2}
[LO.System F S]
{p : F}
{𝓢 : S}
[LO.System.Classical 𝓢]
[LO.System.Necessitation 𝓢]
[LO.System.HasAxiomK 𝓢]
(h : 𝓢 ⊢ □(∼∼p))
:
Equations
- LO.System.box_dne' h = LO.System.box_dne⨀h
Instances For
theorem
LO.System.box_dne'!
{F : Type u_1}
[LO.BasicModalLogicalConnective F]
{S : Type u_2}
[LO.System F S]
{p : F}
{𝓢 : S}
[LO.System.Classical 𝓢]
[LO.System.Necessitation 𝓢]
[LO.System.HasAxiomK 𝓢]
(h : 𝓢 ⊢! □(∼∼p))
:
def
LO.System.multiboxverum
{F : Type u_1}
[LO.BasicModalLogicalConnective F]
{S : Type u_2}
[LO.System F S]
{𝓢 : S}
[LO.System.Classical 𝓢]
[LO.System.Necessitation 𝓢]
{n : ℕ}
:
Equations
- LO.System.multiboxverum = LO.System.multinec LO.System.verum
Instances For
@[simp]
theorem
LO.System.multiboxverum!
{F : Type u_1}
[LO.BasicModalLogicalConnective F]
{S : Type u_2}
[LO.System F S]
{𝓢 : S}
[LO.System.Classical 𝓢]
[LO.System.Necessitation 𝓢]
{n : ℕ}
:
def
LO.System.boxverum
{F : Type u_1}
[LO.BasicModalLogicalConnective F]
{S : Type u_2}
[LO.System F S]
{𝓢 : S}
[LO.System.Classical 𝓢]
[LO.System.Necessitation 𝓢]
:
Equations
- LO.System.boxverum = LO.System.multiboxverum
Instances For
@[simp]
theorem
LO.System.boxverum!
{F : Type u_1}
[LO.BasicModalLogicalConnective F]
{S : Type u_2}
[LO.System F S]
{𝓢 : S}
[LO.System.Classical 𝓢]
[LO.System.Necessitation 𝓢]
:
def
LO.System.boxdotverum
{F : Type u_1}
[LO.BasicModalLogicalConnective F]
{S : Type u_2}
[LO.System F S]
{𝓢 : S}
[LO.System.Classical 𝓢]
[LO.System.Necessitation 𝓢]
:
Equations
- LO.System.boxdotverum = LO.System.andIntro LO.System.verum LO.System.boxverum
Instances For
@[simp]
theorem
LO.System.boxdotverum!
{F : Type u_1}
[LO.BasicModalLogicalConnective F]
{S : Type u_2}
[LO.System F S]
{𝓢 : S}
[LO.System.Classical 𝓢]
[LO.System.Necessitation 𝓢]
:
def
LO.System.implyMultiboxDistribute'
{F : Type u_1}
[LO.BasicModalLogicalConnective F]
{S : Type u_2}
[LO.System F S]
{p : F}
{q : F}
{𝓢 : S}
[LO.System.Classical 𝓢]
[LO.System.Necessitation 𝓢]
[LO.System.HasAxiomK 𝓢]
{n : ℕ}
(h : 𝓢 ⊢ p ➝ q)
:
Instances For
theorem
LO.System.imply_multibox_distribute'!
{F : Type u_1}
[LO.BasicModalLogicalConnective F]
{S : Type u_2}
[LO.System F S]
{p : F}
{q : F}
{𝓢 : S}
[LO.System.Classical 𝓢]
[LO.System.Necessitation 𝓢]
[LO.System.HasAxiomK 𝓢]
{n : ℕ}
(h : 𝓢 ⊢! p ➝ q)
:
def
LO.System.implyBoxDistribute'
{F : Type u_1}
[LO.BasicModalLogicalConnective F]
{S : Type u_2}
[LO.System F S]
{p : F}
{q : F}
{𝓢 : S}
[LO.System.Classical 𝓢]
[LO.System.Necessitation 𝓢]
[LO.System.HasAxiomK 𝓢]
(h : 𝓢 ⊢ p ➝ q)
:
Instances For
theorem
LO.System.imply_box_distribute'!
{F : Type u_1}
[LO.BasicModalLogicalConnective F]
{S : Type u_2}
[LO.System F S]
{p : F}
{q : F}
{𝓢 : S}
[LO.System.Classical 𝓢]
[LO.System.Necessitation 𝓢]
[LO.System.HasAxiomK 𝓢]
(h : 𝓢 ⊢! p ➝ q)
:
def
LO.System.distribute_multibox_and
{F : Type u_1}
[LO.BasicModalLogicalConnective F]
[DecidableEq F]
{S : Type u_2}
[LO.System F S]
{p : F}
{q : F}
{𝓢 : S}
[LO.System.Classical 𝓢]
[LO.System.Necessitation 𝓢]
[LO.System.HasAxiomK 𝓢]
{n : ℕ}
:
Equations
- LO.System.distribute_multibox_and = LO.System.implyRightAnd (LO.System.implyMultiboxDistribute' LO.System.and₁) (LO.System.implyMultiboxDistribute' LO.System.and₂)
Instances For
@[simp]
theorem
LO.System.distribute_multibox_and!
{F : Type u_1}
[LO.BasicModalLogicalConnective F]
[DecidableEq F]
{S : Type u_2}
[LO.System F S]
{p : F}
{q : F}
{𝓢 : S}
[LO.System.Classical 𝓢]
[LO.System.Necessitation 𝓢]
[LO.System.HasAxiomK 𝓢]
{n : ℕ}
:
def
LO.System.distribute_box_and
{F : Type u_1}
[LO.BasicModalLogicalConnective F]
[DecidableEq F]
{S : Type u_2}
[LO.System F S]
{p : F}
{q : F}
{𝓢 : S}
[LO.System.Classical 𝓢]
[LO.System.Necessitation 𝓢]
[LO.System.HasAxiomK 𝓢]
:
Equations
- LO.System.distribute_box_and = LO.System.distribute_multibox_and
Instances For
@[simp]
theorem
LO.System.distribute_box_and!
{F : Type u_1}
[LO.BasicModalLogicalConnective F]
[DecidableEq F]
{S : Type u_2}
[LO.System F S]
{p : F}
{q : F}
{𝓢 : S}
[LO.System.Classical 𝓢]
[LO.System.Necessitation 𝓢]
[LO.System.HasAxiomK 𝓢]
:
def
LO.System.distribute_multibox_and'
{F : Type u_1}
[LO.BasicModalLogicalConnective F]
[DecidableEq F]
{S : Type u_2}
[LO.System F S]
{p : F}
{q : F}
{𝓢 : S}
[LO.System.Classical 𝓢]
[LO.System.Necessitation 𝓢]
[LO.System.HasAxiomK 𝓢]
{n : ℕ}
(h : 𝓢 ⊢ □^[n](p ⋏ q))
:
Equations
- LO.System.distribute_multibox_and' h = LO.System.distribute_multibox_and⨀h
Instances For
theorem
LO.System.distribute_multibox_and'!
{F : Type u_1}
[LO.BasicModalLogicalConnective F]
[DecidableEq F]
{S : Type u_2}
[LO.System F S]
{p : F}
{q : F}
{𝓢 : S}
[LO.System.Classical 𝓢]
[LO.System.Necessitation 𝓢]
[LO.System.HasAxiomK 𝓢]
{n : ℕ}
(d : 𝓢 ⊢! □^[n](p ⋏ q))
:
def
LO.System.distribute_box_and'
{F : Type u_1}
[LO.BasicModalLogicalConnective F]
[DecidableEq F]
{S : Type u_2}
[LO.System F S]
{p : F}
{q : F}
{𝓢 : S}
[LO.System.Classical 𝓢]
[LO.System.Necessitation 𝓢]
[LO.System.HasAxiomK 𝓢]
(h : 𝓢 ⊢ □(p ⋏ q))
:
Instances For
theorem
LO.System.distribute_box_and'!
{F : Type u_1}
[LO.BasicModalLogicalConnective F]
[DecidableEq F]
{S : Type u_2}
[LO.System F S]
{p : F}
{q : F}
{𝓢 : S}
[LO.System.Classical 𝓢]
[LO.System.Necessitation 𝓢]
[LO.System.HasAxiomK 𝓢]
(d : 𝓢 ⊢! □(p ⋏ q))
:
theorem
LO.System.conj_cons!
{F : Type u_1}
[LO.BasicModalLogicalConnective F]
[DecidableEq F]
{S : Type u_2}
[LO.System F S]
{p : F}
{Γ : List F}
{𝓢 : S}
[LO.System.Classical 𝓢]
:
@[simp]
theorem
LO.System.distribute_multibox_conj!
{F : Type u_1}
[LO.BasicModalLogicalConnective F]
[DecidableEq F]
{S : Type u_2}
[LO.System F S]
{Γ : List F}
{𝓢 : S}
[LO.System.Classical 𝓢]
[LO.System.Necessitation 𝓢]
[LO.System.HasAxiomK 𝓢]
{n : ℕ}
:
@[simp]
theorem
LO.System.distribute_box_conj!
{F : Type u_1}
[LO.BasicModalLogicalConnective F]
[DecidableEq F]
{S : Type u_2}
[LO.System F S]
{Γ : List F}
{𝓢 : S}
[LO.System.Classical 𝓢]
[LO.System.Necessitation 𝓢]
[LO.System.HasAxiomK 𝓢]
:
def
LO.System.collect_multibox_and
{F : Type u_1}
[LO.BasicModalLogicalConnective F]
{S : Type u_2}
[LO.System F S]
{p : F}
{q : F}
{𝓢 : S}
[LO.System.Classical 𝓢]
[LO.System.Necessitation 𝓢]
[LO.System.HasAxiomK 𝓢]
{n : ℕ}
:
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
LO.System.collect_multibox_and!
{F : Type u_1}
[LO.BasicModalLogicalConnective F]
{S : Type u_2}
[LO.System F S]
{p : F}
{q : F}
{𝓢 : S}
[LO.System.Classical 𝓢]
[LO.System.Necessitation 𝓢]
[LO.System.HasAxiomK 𝓢]
{n : ℕ}
:
def
LO.System.collect_box_and
{F : Type u_1}
[LO.BasicModalLogicalConnective F]
{S : Type u_2}
[LO.System F S]
{p : F}
{q : F}
{𝓢 : S}
[LO.System.Classical 𝓢]
[LO.System.Necessitation 𝓢]
[LO.System.HasAxiomK 𝓢]
:
Equations
- LO.System.collect_box_and = LO.System.collect_multibox_and
Instances For
@[simp]
theorem
LO.System.collect_box_and!
{F : Type u_1}
[LO.BasicModalLogicalConnective F]
{S : Type u_2}
[LO.System F S]
{p : F}
{q : F}
{𝓢 : S}
[LO.System.Classical 𝓢]
[LO.System.Necessitation 𝓢]
[LO.System.HasAxiomK 𝓢]
:
def
LO.System.collect_multibox_and'
{F : Type u_1}
[LO.BasicModalLogicalConnective F]
{S : Type u_2}
[LO.System F S]
{p : F}
{q : F}
{𝓢 : S}
[LO.System.Classical 𝓢]
[LO.System.Necessitation 𝓢]
[LO.System.HasAxiomK 𝓢]
{n : ℕ}
(h : 𝓢 ⊢ □^[n]p ⋏ □^[n]q)
:
Equations
- LO.System.collect_multibox_and' h = LO.System.collect_multibox_and⨀h
Instances For
theorem
LO.System.collect_multibox_and'!
{F : Type u_1}
[LO.BasicModalLogicalConnective F]
{S : Type u_2}
[LO.System F S]
{p : F}
{q : F}
{𝓢 : S}
[LO.System.Classical 𝓢]
[LO.System.Necessitation 𝓢]
[LO.System.HasAxiomK 𝓢]
{n : ℕ}
(h : 𝓢 ⊢! □^[n]p ⋏ □^[n]q)
:
def
LO.System.collect_box_and'
{F : Type u_1}
[LO.BasicModalLogicalConnective F]
{S : Type u_2}
[LO.System F S]
{p : F}
{q : F}
{𝓢 : S}
[LO.System.Classical 𝓢]
[LO.System.Necessitation 𝓢]
[LO.System.HasAxiomK 𝓢]
(h : 𝓢 ⊢ □p ⋏ □q)
:
Equations
Instances For
theorem
LO.System.collect_box_and'!
{F : Type u_1}
[LO.BasicModalLogicalConnective F]
{S : Type u_2}
[LO.System F S]
{p : F}
{q : F}
{𝓢 : S}
[LO.System.Classical 𝓢]
[LO.System.Necessitation 𝓢]
[LO.System.HasAxiomK 𝓢]
(h : 𝓢 ⊢! □p ⋏ □q)
:
theorem
LO.System.multiboxConj'_iff!
{F : Type u_1}
[LO.BasicModalLogicalConnective F]
[DecidableEq F]
{S : Type u_2}
[LO.System F S]
{Γ : List F}
{𝓢 : S}
[LO.System.Classical 𝓢]
[LO.System.Necessitation 𝓢]
[LO.System.HasAxiomK 𝓢]
{n : ℕ}
:
theorem
LO.System.boxConj'_iff!
{F : Type u_1}
[LO.BasicModalLogicalConnective F]
[DecidableEq F]
{S : Type u_2}
[LO.System F S]
{Γ : List F}
{𝓢 : S}
[LO.System.Classical 𝓢]
[LO.System.Necessitation 𝓢]
[LO.System.HasAxiomK 𝓢]
:
theorem
LO.System.multiboxconj_of_conjmultibox!
{F : Type u_1}
[LO.BasicModalLogicalConnective F]
[DecidableEq F]
{S : Type u_2}
[LO.System F S]
{Γ : List F}
{𝓢 : S}
[LO.System.Classical 𝓢]
[LO.System.Necessitation 𝓢]
[LO.System.HasAxiomK 𝓢]
{n : ℕ}
(d : 𝓢 ⊢! ⋀□'^[n]Γ)
:
@[simp]
theorem
LO.System.multibox_cons_conjAux₁!
{F : Type u_1}
[LO.BasicModalLogicalConnective F]
[DecidableEq F]
{S : Type u_2}
[LO.System F S]
{p : F}
{Γ : List F}
{𝓢 : S}
[LO.System.Classical 𝓢]
{n : ℕ}
:
@[simp]
theorem
LO.System.multibox_cons_conjAux₂!
{F : Type u_1}
[LO.BasicModalLogicalConnective F]
[DecidableEq F]
{S : Type u_2}
[LO.System F S]
{p : F}
{Γ : List F}
{𝓢 : S}
[LO.System.Classical 𝓢]
{n : ℕ}
:
@[simp]
theorem
LO.System.collect_multibox_conj!
{F : Type u_1}
[LO.BasicModalLogicalConnective F]
[DecidableEq F]
{S : Type u_2}
[LO.System F S]
{Γ : List F}
{𝓢 : S}
[LO.System.Classical 𝓢]
[LO.System.Necessitation 𝓢]
[LO.System.HasAxiomK 𝓢]
{n : ℕ}
:
@[simp]
theorem
LO.System.collect_box_conj!
{F : Type u_1}
[LO.BasicModalLogicalConnective F]
[DecidableEq F]
{S : Type u_2}
[LO.System F S]
{Γ : List F}
{𝓢 : S}
[LO.System.Classical 𝓢]
[LO.System.Necessitation 𝓢]
[LO.System.HasAxiomK 𝓢]
:
def
LO.System.collect_multibox_or
{F : Type u_1}
[LO.BasicModalLogicalConnective F]
{S : Type u_2}
[LO.System F S]
{p : F}
{q : F}
{𝓢 : S}
[LO.System.Classical 𝓢]
[LO.System.Necessitation 𝓢]
[LO.System.HasAxiomK 𝓢]
{n : ℕ}
:
Equations
- LO.System.collect_multibox_or = LO.System.or₃'' (LO.System.multibox_axiomK' (LO.System.multinec LO.System.or₁)) (LO.System.multibox_axiomK' (LO.System.multinec LO.System.or₂))
Instances For
@[simp]
theorem
LO.System.collect_multibox_or!
{F : Type u_1}
[LO.BasicModalLogicalConnective F]
{S : Type u_2}
[LO.System F S]
{p : F}
{q : F}
{𝓢 : S}
[LO.System.Classical 𝓢]
[LO.System.Necessitation 𝓢]
[LO.System.HasAxiomK 𝓢]
{n : ℕ}
:
def
LO.System.collect_box_or
{F : Type u_1}
[LO.BasicModalLogicalConnective F]
{S : Type u_2}
[LO.System F S]
{p : F}
{q : F}
{𝓢 : S}
[LO.System.Classical 𝓢]
[LO.System.Necessitation 𝓢]
[LO.System.HasAxiomK 𝓢]
:
Equations
- LO.System.collect_box_or = LO.System.collect_multibox_or
Instances For
@[simp]
theorem
LO.System.collect_box_or!
{F : Type u_1}
[LO.BasicModalLogicalConnective F]
{S : Type u_2}
[LO.System F S]
{p : F}
{q : F}
{𝓢 : S}
[LO.System.Classical 𝓢]
[LO.System.Necessitation 𝓢]
[LO.System.HasAxiomK 𝓢]
:
def
LO.System.collect_multibox_or'
{F : Type u_1}
[LO.BasicModalLogicalConnective F]
{S : Type u_2}
[LO.System F S]
{p : F}
{q : F}
{𝓢 : S}
[LO.System.Classical 𝓢]
[LO.System.Necessitation 𝓢]
[LO.System.HasAxiomK 𝓢]
{n : ℕ}
(h : 𝓢 ⊢ □^[n]p ⋎ □^[n]q)
:
Equations
- LO.System.collect_multibox_or' h = LO.System.collect_multibox_or⨀h
Instances For
theorem
LO.System.collect_multibox_or'!
{F : Type u_1}
[LO.BasicModalLogicalConnective F]
{S : Type u_2}
[LO.System F S]
{p : F}
{q : F}
{𝓢 : S}
[LO.System.Classical 𝓢]
[LO.System.Necessitation 𝓢]
[LO.System.HasAxiomK 𝓢]
{n : ℕ}
(h : 𝓢 ⊢! □^[n]p ⋎ □^[n]q)
:
def
LO.System.collect_box_or'
{F : Type u_1}
[LO.BasicModalLogicalConnective F]
{S : Type u_2}
[LO.System F S]
{p : F}
{q : F}
{𝓢 : S}
[LO.System.Classical 𝓢]
[LO.System.Necessitation 𝓢]
[LO.System.HasAxiomK 𝓢]
(h : 𝓢 ⊢ □p ⋎ □q)
:
Equations
Instances For
theorem
LO.System.collect_box_or'!
{F : Type u_1}
[LO.BasicModalLogicalConnective F]
{S : Type u_2}
[LO.System F S]
{p : F}
{q : F}
{𝓢 : S}
[LO.System.Classical 𝓢]
[LO.System.Necessitation 𝓢]
[LO.System.HasAxiomK 𝓢]
(h : 𝓢 ⊢! □p ⋎ □q)
:
def
LO.System.diaOrInst₁
{F : Type u_1}
[LO.BasicModalLogicalConnective F]
[DecidableEq F]
{S : Type u_2}
[LO.System F S]
{p : F}
{q : F}
{𝓢 : S}
[LO.System.Classical 𝓢]
[LO.System.NegationEquiv 𝓢]
[LO.System.Necessitation 𝓢]
[LO.System.HasAxiomK 𝓢]
[LO.System.HasDiaDuality 𝓢]
:
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
LO.System.dia_or_inst₁!
{F : Type u_1}
[LO.BasicModalLogicalConnective F]
[DecidableEq F]
{S : Type u_2}
[LO.System F S]
{p : F}
{q : F}
{𝓢 : S}
[LO.System.Classical 𝓢]
[LO.System.NegationEquiv 𝓢]
[LO.System.Necessitation 𝓢]
[LO.System.HasAxiomK 𝓢]
[LO.System.HasDiaDuality 𝓢]
:
def
LO.System.diaOrInst₂
{F : Type u_1}
[LO.BasicModalLogicalConnective F]
[DecidableEq F]
{S : Type u_2}
[LO.System F S]
{p : F}
{q : F}
{𝓢 : S}
[LO.System.Classical 𝓢]
[LO.System.NegationEquiv 𝓢]
[LO.System.Necessitation 𝓢]
[LO.System.HasAxiomK 𝓢]
[LO.System.HasDiaDuality 𝓢]
:
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
LO.System.dia_or_inst₂!
{F : Type u_1}
[LO.BasicModalLogicalConnective F]
[DecidableEq F]
{S : Type u_2}
[LO.System F S]
{p : F}
{q : F}
{𝓢 : S}
[LO.System.Classical 𝓢]
[LO.System.NegationEquiv 𝓢]
[LO.System.Necessitation 𝓢]
[LO.System.HasAxiomK 𝓢]
[LO.System.HasDiaDuality 𝓢]
:
def
LO.System.collect_dia_or
{F : Type u_1}
[LO.BasicModalLogicalConnective F]
[DecidableEq F]
{S : Type u_2}
[LO.System F S]
{p : F}
{q : F}
{𝓢 : S}
[LO.System.Classical 𝓢]
[LO.System.NegationEquiv 𝓢]
[LO.System.Necessitation 𝓢]
[LO.System.HasAxiomK 𝓢]
[LO.System.HasDiaDuality 𝓢]
:
Equations
- LO.System.collect_dia_or = LO.System.or₃'' LO.System.diaOrInst₁ LO.System.diaOrInst₂
Instances For
@[simp]
theorem
LO.System.collect_dia_or!
{F : Type u_1}
[LO.BasicModalLogicalConnective F]
[DecidableEq F]
{S : Type u_2}
[LO.System F S]
{p : F}
{q : F}
{𝓢 : S}
[LO.System.Classical 𝓢]
[LO.System.NegationEquiv 𝓢]
[LO.System.Necessitation 𝓢]
[LO.System.HasAxiomK 𝓢]
[LO.System.HasDiaDuality 𝓢]
:
def
LO.System.collect_dia_or'
{F : Type u_1}
[LO.BasicModalLogicalConnective F]
[DecidableEq F]
{S : Type u_2}
[LO.System F S]
{p : F}
{q : F}
{𝓢 : S}
[LO.System.Classical 𝓢]
[LO.System.NegationEquiv 𝓢]
[LO.System.Necessitation 𝓢]
[LO.System.HasAxiomK 𝓢]
[LO.System.HasDiaDuality 𝓢]
(h : 𝓢 ⊢ ◇p ⋎ ◇q)
:
Equations
- LO.System.collect_dia_or' h = LO.System.collect_dia_or⨀h
Instances For
@[simp]
theorem
LO.System.collect_dia_or'!
{F : Type u_1}
[LO.BasicModalLogicalConnective F]
[DecidableEq F]
{S : Type u_2}
[LO.System F S]
{p : F}
{q : F}
{𝓢 : S}
[LO.System.Classical 𝓢]
[LO.System.NegationEquiv 𝓢]
[LO.System.Necessitation 𝓢]
[LO.System.HasAxiomK 𝓢]
[LO.System.HasDiaDuality 𝓢]
(h : 𝓢 ⊢! ◇p ⋎ ◇q)
:
@[simp]
theorem
LO.System.distribute_multidia_and!
{F : Type u_1}
[LO.BasicModalLogicalConnective F]
[DecidableEq F]
{S : Type u_2}
[LO.System F S]
{p : F}
{q : F}
{𝓢 : S}
[LO.System.Classical 𝓢]
[LO.System.NegationEquiv 𝓢]
[LO.System.Necessitation 𝓢]
[LO.System.HasAxiomK 𝓢]
[LO.System.HasDiaDuality 𝓢]
{n : ℕ}
:
@[simp]
theorem
LO.System.distribute_dia_and!
{F : Type u_1}
[LO.BasicModalLogicalConnective F]
[DecidableEq F]
{S : Type u_2}
[LO.System F S]
{p : F}
{q : F}
{𝓢 : S}
[LO.System.Classical 𝓢]
[LO.System.NegationEquiv 𝓢]
[LO.System.Necessitation 𝓢]
[LO.System.HasAxiomK 𝓢]
[LO.System.HasDiaDuality 𝓢]
:
@[simp]
theorem
LO.System.iff_conjmultidia_multidiaconj!
{F : Type u_1}
[LO.BasicModalLogicalConnective F]
[DecidableEq F]
{S : Type u_2}
[LO.System F S]
{Γ : List F}
{𝓢 : S}
[LO.System.Classical 𝓢]
[LO.System.NegationEquiv 𝓢]
[LO.System.Necessitation 𝓢]
[LO.System.HasAxiomK 𝓢]
[LO.System.HasDiaDuality 𝓢]
{n : ℕ}
:
theorem
LO.System.distribute_dia_and'!
{F : Type u_1}
[LO.BasicModalLogicalConnective F]
[DecidableEq F]
{S : Type u_2}
[LO.System F S]
{p : F}
{q : F}
{𝓢 : S}
[LO.System.Classical 𝓢]
[LO.System.NegationEquiv 𝓢]
[LO.System.Necessitation 𝓢]
[LO.System.HasAxiomK 𝓢]
[LO.System.HasDiaDuality 𝓢]
(h : 𝓢 ⊢! ◇(p ⋏ q))
:
def
LO.System.boxdotAxiomK
{F : Type u_1}
[LO.BasicModalLogicalConnective F]
[DecidableEq F]
{S : Type u_2}
[LO.System F S]
{p : F}
{q : F}
{𝓢 : S}
[LO.System.Classical 𝓢]
[LO.System.HasAxiomK 𝓢]
:
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
LO.System.boxdot_axiomK!
{F : Type u_1}
[LO.BasicModalLogicalConnective F]
[DecidableEq F]
{S : Type u_2}
[LO.System F S]
{p : F}
{q : F}
{𝓢 : S}
[LO.System.Classical 𝓢]
[LO.System.HasAxiomK 𝓢]
:
def
LO.System.boxdotAxiomT
{F : Type u_1}
[LO.BasicModalLogicalConnective F]
{S : Type u_2}
[LO.System F S]
{p : F}
{𝓢 : S}
[LO.System.Classical 𝓢]
:
Equations
- LO.System.boxdotAxiomT = LO.System.and₁
Instances For
@[simp]
theorem
LO.System.boxdot_axiomT!
{F : Type u_1}
[LO.BasicModalLogicalConnective F]
{S : Type u_2}
[LO.System F S]
{p : F}
{𝓢 : S}
[LO.System.Classical 𝓢]
:
def
LO.System.boxdotNec
{F : Type u_1}
[LO.BasicModalLogicalConnective F]
{S : Type u_2}
[LO.System F S]
{p : F}
{𝓢 : S}
[LO.System.Classical 𝓢]
[LO.System.Necessitation 𝓢]
(d : 𝓢 ⊢ p)
:
Equations
Instances For
theorem
LO.System.boxdot_nec!
{F : Type u_1}
[LO.BasicModalLogicalConnective F]
{S : Type u_2}
[LO.System F S]
{p : F}
{𝓢 : S}
[LO.System.Classical 𝓢]
[LO.System.Necessitation 𝓢]
(d : 𝓢 ⊢! p)
:
def
LO.System.boxdotBox
{F : Type u_1}
[LO.BasicModalLogicalConnective F]
{S : Type u_2}
[LO.System F S]
{p : F}
{𝓢 : S}
[LO.System.Classical 𝓢]
:
Equations
- LO.System.boxdotBox = LO.System.and₂
Instances For
theorem
LO.System.boxdot_box!
{F : Type u_1}
[LO.BasicModalLogicalConnective F]
{S : Type u_2}
[LO.System F S]
{p : F}
{𝓢 : S}
[LO.System.Classical 𝓢]
:
def
LO.System.BoxBoxdot_BoxDotbox
{F : Type u_1}
[LO.BasicModalLogicalConnective F]
[DecidableEq F]
{S : Type u_2}
[LO.System F S]
{p : F}
{𝓢 : S}
[LO.System.Classical 𝓢]
[LO.System.Necessitation 𝓢]
[LO.System.HasAxiomK 𝓢]
:
Equations
- LO.System.BoxBoxdot_BoxDotbox = LO.System.impTrans'' LO.System.distribute_box_and (LO.System.impId (□p ⋏ □□p))
Instances For
theorem
LO.System.boxboxdot_boxdotbox
{F : Type u_1}
[LO.BasicModalLogicalConnective F]
[DecidableEq F]
{S : Type u_2}
[LO.System F S]
{p : F}
{𝓢 : S}
[LO.System.Classical 𝓢]
[LO.System.Necessitation 𝓢]
[LO.System.HasAxiomK 𝓢]
:
def
LO.System.axiomT
{F : Type u_1}
[LO.BasicModalLogicalConnective F]
{S : Type u_2}
[LO.System F S]
{p : F}
{𝓢 : S}
[LO.System.HasAxiomT 𝓢]
:
Equations
- LO.System.axiomT = LO.System.HasAxiomT.T p
Instances For
@[simp]
theorem
LO.System.axiomT!
{F : Type u_1}
[LO.BasicModalLogicalConnective F]
{S : Type u_2}
[LO.System F S]
{p : F}
{𝓢 : S}
[LO.System.HasAxiomT 𝓢]
:
instance
LO.System.instHasAxiomTFiniteContext
{F : Type u_1}
[LO.BasicModalLogicalConnective F]
{S : Type u_2}
[LO.System F S]
{𝓢 : S}
[LO.System.Classical 𝓢]
[LO.System.HasAxiomT 𝓢]
(Γ : LO.System.FiniteContext F 𝓢)
:
Equations
- LO.System.instHasAxiomTFiniteContext Γ = { T := fun (x : F) => LO.System.FiniteContext.of LO.System.axiomT }
instance
LO.System.instHasAxiomTContext
{F : Type u_1}
[LO.BasicModalLogicalConnective F]
{S : Type u_2}
[LO.System F S]
{𝓢 : S}
[LO.System.Classical 𝓢]
[LO.System.HasAxiomT 𝓢]
(Γ : LO.System.Context F 𝓢)
:
Equations
- LO.System.instHasAxiomTContext Γ = { T := fun (x : F) => LO.System.Context.of LO.System.axiomT }
def
LO.System.axiomT'
{F : Type u_1}
[LO.BasicModalLogicalConnective F]
{S : Type u_2}
[LO.System F S]
{p : F}
{𝓢 : S}
[LO.System.Classical 𝓢]
[LO.System.HasAxiomT 𝓢]
(h : 𝓢 ⊢ □p)
:
𝓢 ⊢ p
Equations
- LO.System.axiomT' h = LO.System.axiomT⨀h
Instances For
@[simp]
theorem
LO.System.axiomT'!
{F : Type u_1}
[LO.BasicModalLogicalConnective F]
{S : Type u_2}
[LO.System F S]
{p : F}
{𝓢 : S}
[LO.System.Classical 𝓢]
[LO.System.HasAxiomT 𝓢]
(h : 𝓢 ⊢! □p)
:
𝓢 ⊢! p
def
LO.System.diaTc
{F : Type u_1}
[LO.BasicModalLogicalConnective F]
[DecidableEq F]
{S : Type u_2}
[LO.System F S]
{p : F}
{𝓢 : S}
[LO.System.Classical 𝓢]
[LO.System.NegationEquiv 𝓢]
[LO.System.HasDiaDuality 𝓢]
[LO.System.HasAxiomT 𝓢]
:
Equations
- LO.System.diaTc = LO.System.impTrans'' (LO.System.impTrans'' LO.System.dni (LO.System.contra₀' LO.System.axiomT)) (LO.System.and₂' LO.System.diaDuality)
Instances For
@[simp]
theorem
LO.System.diaTc!
{F : Type u_1}
[LO.BasicModalLogicalConnective F]
[DecidableEq F]
{S : Type u_2}
[LO.System F S]
{p : F}
{𝓢 : S}
[LO.System.Classical 𝓢]
[LO.System.NegationEquiv 𝓢]
[LO.System.HasDiaDuality 𝓢]
[LO.System.HasAxiomT 𝓢]
:
def
LO.System.diaTc'
{F : Type u_1}
[LO.BasicModalLogicalConnective F]
[DecidableEq F]
{S : Type u_2}
[LO.System F S]
{p : F}
{𝓢 : S}
[LO.System.Classical 𝓢]
[LO.System.NegationEquiv 𝓢]
[LO.System.HasDiaDuality 𝓢]
[LO.System.HasAxiomT 𝓢]
(h : 𝓢 ⊢ p)
:
Equations
- LO.System.diaTc' h = LO.System.diaTc⨀h
Instances For
theorem
LO.System.diaTc'!
{F : Type u_1}
[LO.BasicModalLogicalConnective F]
[DecidableEq F]
{S : Type u_2}
[LO.System F S]
{p : F}
{𝓢 : S}
[LO.System.Classical 𝓢]
[LO.System.NegationEquiv 𝓢]
[LO.System.HasDiaDuality 𝓢]
[LO.System.HasAxiomT 𝓢]
(h : 𝓢 ⊢! p)
:
def
LO.System.axiomB
{F : Type u_1}
[LO.BasicModalLogicalConnective F]
{S : Type u_2}
[LO.System F S]
{p : F}
{𝓢 : S}
[LO.System.HasAxiomB 𝓢]
:
Equations
- LO.System.axiomB = LO.System.HasAxiomB.B p
Instances For
@[simp]
theorem
LO.System.axiomB!
{F : Type u_1}
[LO.BasicModalLogicalConnective F]
{S : Type u_2}
[LO.System F S]
{p : F}
{𝓢 : S}
[LO.System.HasAxiomB 𝓢]
:
instance
LO.System.instHasAxiomBFiniteContext
{F : Type u_1}
[LO.BasicModalLogicalConnective F]
{S : Type u_2}
[LO.System F S]
{𝓢 : S}
[LO.System.Classical 𝓢]
[LO.System.HasAxiomB 𝓢]
(Γ : LO.System.FiniteContext F 𝓢)
:
Equations
- LO.System.instHasAxiomBFiniteContext Γ = { B := fun (x : F) => LO.System.FiniteContext.of LO.System.axiomB }
instance
LO.System.instHasAxiomBContext
{F : Type u_1}
[LO.BasicModalLogicalConnective F]
{S : Type u_2}
[LO.System F S]
{𝓢 : S}
[LO.System.Classical 𝓢]
[LO.System.HasAxiomB 𝓢]
(Γ : LO.System.Context F 𝓢)
:
Equations
- LO.System.instHasAxiomBContext Γ = { B := fun (x : F) => LO.System.Context.of LO.System.axiomB }
def
LO.System.axiomD
{F : Type u_1}
[LO.BasicModalLogicalConnective F]
{S : Type u_2}
[LO.System F S]
{p : F}
{𝓢 : S}
[LO.System.HasAxiomD 𝓢]
:
Equations
- LO.System.axiomD = LO.System.HasAxiomD.D p
Instances For
@[simp]
theorem
LO.System.axiomD!
{F : Type u_1}
[LO.BasicModalLogicalConnective F]
{S : Type u_2}
[LO.System F S]
{p : F}
{𝓢 : S}
[LO.System.HasAxiomD 𝓢]
:
instance
LO.System.instHasAxiomDFiniteContext
{F : Type u_1}
[LO.BasicModalLogicalConnective F]
{S : Type u_2}
[LO.System F S]
{𝓢 : S}
[LO.System.Classical 𝓢]
[LO.System.HasAxiomD 𝓢]
(Γ : LO.System.FiniteContext F 𝓢)
:
Equations
- LO.System.instHasAxiomDFiniteContext Γ = { D := fun (x : F) => LO.System.FiniteContext.of LO.System.axiomD }
instance
LO.System.instHasAxiomDContext
{F : Type u_1}
[LO.BasicModalLogicalConnective F]
{S : Type u_2}
[LO.System F S]
{𝓢 : S}
[LO.System.Classical 𝓢]
[LO.System.HasAxiomD 𝓢]
(Γ : LO.System.Context F 𝓢)
:
Equations
- LO.System.instHasAxiomDContext Γ = { D := fun (x : F) => LO.System.Context.of LO.System.axiomD }
def
LO.System.notbot
{F : Type u_1}
[LO.BasicModalLogicalConnective F]
{S : Type u_2}
[LO.System F S]
{𝓢 : S}
[LO.System.Classical 𝓢]
[LO.System.NegationEquiv 𝓢]
:
Equations
- LO.System.notbot = LO.System.neg_equiv'.mpr (LO.System.impId ⊥)
Instances For
instance
LO.System.instHasAxiomP
{F : Type u_1}
[LO.BasicModalLogicalConnective F]
[DecidableEq F]
{S : Type u_2}
[LO.System F S]
{𝓢 : S}
[LO.System.Classical 𝓢]
[LO.System.NegationEquiv 𝓢]
[LO.System.Necessitation 𝓢]
[LO.System.HasDiaDuality 𝓢]
[LO.System.HasAxiomD 𝓢]
:
Equations
- LO.System.instHasAxiomP = { P := LO.System.P_of_D }
def
LO.System.axiomP
{F : Type u_1}
[LO.BasicModalLogicalConnective F]
{S : Type u_2}
[LO.System F S]
{𝓢 : S}
[LO.System.HasAxiomP 𝓢]
:
Equations
- LO.System.axiomP = LO.System.HasAxiomP.P
Instances For
@[simp]
theorem
LO.System.axiomP!
{F : Type u_1}
[LO.BasicModalLogicalConnective F]
{S : Type u_2}
[LO.System F S]
{𝓢 : S}
[LO.System.HasAxiomP 𝓢]
:
instance
LO.System.instHasAxiomPFiniteContext
{F : Type u_1}
[LO.BasicModalLogicalConnective F]
{S : Type u_2}
[LO.System F S]
{𝓢 : S}
[LO.System.Classical 𝓢]
[LO.System.HasAxiomP 𝓢]
(Γ : LO.System.FiniteContext F 𝓢)
:
Equations
- LO.System.instHasAxiomPFiniteContext Γ = { P := LO.System.FiniteContext.of LO.System.axiomP }
instance
LO.System.instHasAxiomPContext
{F : Type u_1}
[LO.BasicModalLogicalConnective F]
{S : Type u_2}
[LO.System F S]
{𝓢 : S}
[LO.System.Classical 𝓢]
[LO.System.HasAxiomP 𝓢]
(Γ : LO.System.Context F 𝓢)
:
Equations
- LO.System.instHasAxiomPContext Γ = { P := LO.System.Context.of LO.System.axiomP }
instance
LO.System.instHasAxiomD
{F : Type u_1}
[LO.BasicModalLogicalConnective F]
[DecidableEq F]
{S : Type u_2}
[LO.System F S]
{𝓢 : S}
[LO.System.Classical 𝓢]
[LO.System.NegationEquiv 𝓢]
[LO.System.Necessitation 𝓢]
[LO.System.HasAxiomK 𝓢]
[LO.System.HasDiaDuality 𝓢]
[LO.System.HasAxiomP 𝓢]
:
Equations
- LO.System.instHasAxiomD = { D := fun (x : F) => LO.System.D_of_P }
def
LO.System.axiomFour
{F : Type u_1}
[LO.BasicModalLogicalConnective F]
{S : Type u_2}
[LO.System F S]
{p : F}
{𝓢 : S}
[LO.System.HasAxiomFour 𝓢]
:
Equations
- LO.System.axiomFour = LO.System.HasAxiomFour.Four p
Instances For
@[simp]
theorem
LO.System.axiomFour!
{F : Type u_1}
[LO.BasicModalLogicalConnective F]
{S : Type u_2}
[LO.System F S]
{p : F}
{𝓢 : S}
[LO.System.HasAxiomFour 𝓢]
:
instance
LO.System.instHasAxiomFourFiniteContext
{F : Type u_1}
[LO.BasicModalLogicalConnective F]
{S : Type u_2}
[LO.System F S]
{𝓢 : S}
[LO.System.Classical 𝓢]
[LO.System.HasAxiomFour 𝓢]
(Γ : LO.System.FiniteContext F 𝓢)
:
Equations
- LO.System.instHasAxiomFourFiniteContext Γ = { Four := fun (x : F) => LO.System.FiniteContext.of LO.System.axiomFour }
instance
LO.System.instHasAxiomFourContext
{F : Type u_1}
[LO.BasicModalLogicalConnective F]
{S : Type u_2}
[LO.System F S]
{𝓢 : S}
[LO.System.Classical 𝓢]
[LO.System.HasAxiomFour 𝓢]
(Γ : LO.System.Context F 𝓢)
:
Equations
- LO.System.instHasAxiomFourContext Γ = { Four := fun (x : F) => LO.System.Context.of LO.System.axiomFour }
def
LO.System.axiomFour'
{F : Type u_1}
[LO.BasicModalLogicalConnective F]
{S : Type u_2}
[LO.System F S]
{p : F}
{𝓢 : S}
[LO.System.Classical 𝓢]
[LO.System.HasAxiomFour 𝓢]
(h : 𝓢 ⊢ □p)
:
Equations
- LO.System.axiomFour' h = LO.System.axiomFour⨀h
Instances For
def
LO.System.axiomFour'!
{F : Type u_1}
[LO.BasicModalLogicalConnective F]
{S : Type u_2}
[LO.System F S]
{p : F}
{𝓢 : S}
[LO.System.Classical 𝓢]
[LO.System.HasAxiomFour 𝓢]
(h : 𝓢 ⊢! □p)
:
Equations
- ⋯ = ⋯
Instances For
def
LO.System.imply_BoxBoxdot_Box
{F : Type u_1}
[LO.BasicModalLogicalConnective F]
[DecidableEq F]
{S : Type u_2}
[LO.System F S]
{p : F}
{𝓢 : S}
[LO.System.Classical 𝓢]
[LO.System.Necessitation 𝓢]
[LO.System.HasAxiomK 𝓢]
:
Equations
- LO.System.imply_BoxBoxdot_Box = LO.System.impTrans'' LO.System.distribute_box_and LO.System.and₁
Instances For
@[simp]
theorem
LO.System.imply_boxboxdot_box
{F : Type u_1}
[LO.BasicModalLogicalConnective F]
[DecidableEq F]
{S : Type u_2}
[LO.System F S]
{p : F}
{𝓢 : S}
[LO.System.Classical 𝓢]
[LO.System.Necessitation 𝓢]
[LO.System.HasAxiomK 𝓢]
:
def
LO.System.imply_Box_BoxBoxdot
{F : Type u_1}
[LO.BasicModalLogicalConnective F]
[DecidableEq F]
{S : Type u_2}
[LO.System F S]
{p : F}
{𝓢 : S}
[LO.System.Classical 𝓢]
[LO.System.Necessitation 𝓢]
[LO.System.HasAxiomK 𝓢]
[LO.System.HasAxiomFour 𝓢]
:
Equations
- LO.System.imply_Box_BoxBoxdot = LO.System.impTrans'' (LO.System.implyRightAnd (LO.System.impId (□p)) LO.System.axiomFour) LO.System.collect_box_and
Instances For
@[simp]
theorem
LO.System.imply_box_boxboxdot!
{F : Type u_1}
[LO.BasicModalLogicalConnective F]
[DecidableEq F]
{S : Type u_2}
[LO.System F S]
{p : F}
{𝓢 : S}
[LO.System.Classical 𝓢]
[LO.System.Necessitation 𝓢]
[LO.System.HasAxiomK 𝓢]
[LO.System.HasAxiomFour 𝓢]
:
def
LO.System.imply_Box_BoxBoxdot'
{F : Type u_1}
[LO.BasicModalLogicalConnective F]
[DecidableEq F]
{S : Type u_2}
[LO.System F S]
{p : F}
{𝓢 : S}
[LO.System.Classical 𝓢]
[LO.System.Necessitation 𝓢]
[LO.System.HasAxiomK 𝓢]
[LO.System.HasAxiomFour 𝓢]
(h : 𝓢 ⊢ □p)
:
Equations
- LO.System.imply_Box_BoxBoxdot' h = LO.System.imply_Box_BoxBoxdot⨀h
Instances For
def
LO.System.imply_Box_BoxBoxdot'!
{F : Type u_1}
[LO.BasicModalLogicalConnective F]
[DecidableEq F]
{S : Type u_2}
[LO.System F S]
{p : F}
{𝓢 : S}
[LO.System.Classical 𝓢]
[LO.System.Necessitation 𝓢]
[LO.System.HasAxiomK 𝓢]
[LO.System.HasAxiomFour 𝓢]
(h : 𝓢 ⊢! □p)
:
Equations
- ⋯ = ⋯
Instances For
def
LO.System.iff_Box_BoxBoxdot
{F : Type u_1}
[LO.BasicModalLogicalConnective F]
[DecidableEq F]
{S : Type u_2}
[LO.System F S]
{p : F}
{𝓢 : S}
[LO.System.Classical 𝓢]
[LO.System.Necessitation 𝓢]
[LO.System.HasAxiomK 𝓢]
[LO.System.HasAxiomFour 𝓢]
:
Equations
- LO.System.iff_Box_BoxBoxdot = LO.System.iffIntro LO.System.imply_Box_BoxBoxdot LO.System.imply_BoxBoxdot_Box
Instances For
@[simp]
theorem
LO.System.iff_box_boxboxdot!
{F : Type u_1}
[LO.BasicModalLogicalConnective F]
[DecidableEq F]
{S : Type u_2}
[LO.System F S]
{p : F}
{𝓢 : S}
[LO.System.Classical 𝓢]
[LO.System.Necessitation 𝓢]
[LO.System.HasAxiomK 𝓢]
[LO.System.HasAxiomFour 𝓢]
:
def
LO.System.iff_Box_BoxdotBox
{F : Type u_1}
[LO.BasicModalLogicalConnective F]
[DecidableEq F]
{S : Type u_2}
[LO.System F S]
{p : F}
{𝓢 : S}
[LO.System.Classical 𝓢]
[LO.System.HasAxiomFour 𝓢]
:
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
LO.System.iff_box_boxdotbox!
{F : Type u_1}
[LO.BasicModalLogicalConnective F]
[DecidableEq F]
{S : Type u_2}
[LO.System F S]
{p : F}
{𝓢 : S}
[LO.System.Classical 𝓢]
[LO.System.HasAxiomFour 𝓢]
:
def
LO.System.iff_Boxdot_BoxdotBoxdot
{F : Type u_1}
[LO.BasicModalLogicalConnective F]
[DecidableEq F]
{S : Type u_2}
[LO.System F S]
{p : F}
{𝓢 : S}
[LO.System.Classical 𝓢]
[LO.System.Necessitation 𝓢]
[LO.System.HasAxiomK 𝓢]
[LO.System.HasAxiomFour 𝓢]
:
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
LO.System.iff_boxdot_boxdotboxdot
{F : Type u_1}
[LO.BasicModalLogicalConnective F]
[DecidableEq F]
{S : Type u_2}
[LO.System F S]
{p : F}
{𝓢 : S}
[LO.System.Classical 𝓢]
[LO.System.Necessitation 𝓢]
[LO.System.HasAxiomK 𝓢]
[LO.System.HasAxiomFour 𝓢]
:
def
LO.System.boxdotAxiomFour
{F : Type u_1}
[LO.BasicModalLogicalConnective F]
[DecidableEq F]
{S : Type u_2}
[LO.System F S]
{p : F}
{𝓢 : S}
[LO.System.Classical 𝓢]
[LO.System.Necessitation 𝓢]
[LO.System.HasAxiomK 𝓢]
[LO.System.HasAxiomFour 𝓢]
:
Equations
- LO.System.boxdotAxiomFour = LO.System.and₁' LO.System.iff_Boxdot_BoxdotBoxdot
Instances For
@[simp]
theorem
LO.System.boxdot_axiomFour!
{F : Type u_1}
[LO.BasicModalLogicalConnective F]
[DecidableEq F]
{S : Type u_2}
[LO.System F S]
{p : F}
{𝓢 : S}
[LO.System.Classical 𝓢]
[LO.System.Necessitation 𝓢]
[LO.System.HasAxiomK 𝓢]
[LO.System.HasAxiomFour 𝓢]
:
def
LO.System.iff_box_boxdot
{F : Type u_1}
[LO.BasicModalLogicalConnective F]
[DecidableEq F]
{S : Type u_2}
[LO.System F S]
{p : F}
{𝓢 : S}
[LO.System.Classical 𝓢]
[LO.System.HasAxiomT 𝓢]
:
Equations
- LO.System.iff_box_boxdot = LO.System.iffIntro (LO.System.implyRightAnd LO.System.axiomT (LO.System.impId (□p))) LO.System.and₂
Instances For
@[simp]
theorem
LO.System.iff_box_boxdot!
{F : Type u_1}
[LO.BasicModalLogicalConnective F]
[DecidableEq F]
{S : Type u_2}
[LO.System F S]
{p : F}
{𝓢 : S}
[LO.System.Classical 𝓢]
[LO.System.HasAxiomT 𝓢]
:
def
LO.System.iff_dia_diadot
{F : Type u_1}
[LO.BasicModalLogicalConnective F]
[DecidableEq F]
{S : Type u_2}
[LO.System F S]
{p : F}
{𝓢 : S}
[LO.System.Classical 𝓢]
[LO.System.NegationEquiv 𝓢]
[LO.System.HasDiaDuality 𝓢]
[LO.System.HasAxiomT 𝓢]
[LO.System.HasAxiomFour 𝓢]
:
Equations
- LO.System.iff_dia_diadot = LO.System.iffIntro LO.System.or₂ (LO.System.or₃'' LO.System.diaTc (LO.System.impId (◇p)))
Instances For
@[simp]
theorem
LO.System.iff_dia_diadot!
{F : Type u_1}
[LO.BasicModalLogicalConnective F]
[DecidableEq F]
{S : Type u_2}
[LO.System F S]
{p : F}
{𝓢 : S}
[LO.System.Classical 𝓢]
[LO.System.NegationEquiv 𝓢]
[LO.System.HasDiaDuality 𝓢]
[LO.System.HasAxiomT 𝓢]
[LO.System.HasAxiomFour 𝓢]
:
def
LO.System.axiomFive
{F : Type u_1}
[LO.BasicModalLogicalConnective F]
{S : Type u_2}
[LO.System F S]
{p : F}
{𝓢 : S}
[LO.System.HasAxiomFive 𝓢]
:
Equations
- LO.System.axiomFive = LO.System.HasAxiomFive.Five p
Instances For
@[simp]
theorem
LO.System.axiomFive!
{F : Type u_1}
[LO.BasicModalLogicalConnective F]
{S : Type u_2}
[LO.System F S]
{p : F}
{𝓢 : S}
[LO.System.HasAxiomFive 𝓢]
:
instance
LO.System.instHasAxiomFiveFiniteContext
{F : Type u_1}
[LO.BasicModalLogicalConnective F]
{S : Type u_2}
[LO.System F S]
{𝓢 : S}
[LO.System.Classical 𝓢]
[LO.System.HasAxiomFive 𝓢]
(Γ : LO.System.FiniteContext F 𝓢)
:
Equations
- LO.System.instHasAxiomFiveFiniteContext Γ = { Five := fun (x : F) => LO.System.FiniteContext.of LO.System.axiomFive }
instance
LO.System.instHasAxiomFiveContext
{F : Type u_1}
[LO.BasicModalLogicalConnective F]
{S : Type u_2}
[LO.System F S]
{𝓢 : S}
[LO.System.Classical 𝓢]
[LO.System.HasAxiomFive 𝓢]
(Γ : LO.System.Context F 𝓢)
:
Equations
- LO.System.instHasAxiomFiveContext Γ = { Five := fun (x : F) => LO.System.Context.of LO.System.axiomFive }
def
LO.System.diabox_box
{F : Type u_1}
[LO.BasicModalLogicalConnective F]
[DecidableEq F]
{S : Type u_2}
[LO.System F S]
{p : F}
{𝓢 : S}
[LO.System.Classical 𝓢]
[LO.System.NegationEquiv 𝓢]
[LO.System.Necessitation 𝓢]
[LO.System.HasAxiomK 𝓢]
[LO.System.HasDiaDuality 𝓢]
[LO.System.HasAxiomFive 𝓢]
:
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
LO.System.diabox_box!
{F : Type u_1}
[LO.BasicModalLogicalConnective F]
[DecidableEq F]
{S : Type u_2}
[LO.System F S]
{p : F}
{𝓢 : S}
[LO.System.Classical 𝓢]
[LO.System.NegationEquiv 𝓢]
[LO.System.Necessitation 𝓢]
[LO.System.HasAxiomK 𝓢]
[LO.System.HasDiaDuality 𝓢]
[LO.System.HasAxiomFive 𝓢]
:
def
LO.System.diabox_box'
{F : Type u_1}
[LO.BasicModalLogicalConnective F]
[DecidableEq F]
{S : Type u_2}
[LO.System F S]
{p : F}
{𝓢 : S}
[LO.System.Classical 𝓢]
[LO.System.NegationEquiv 𝓢]
[LO.System.Necessitation 𝓢]
[LO.System.HasAxiomK 𝓢]
[LO.System.HasDiaDuality 𝓢]
[LO.System.HasAxiomFive 𝓢]
(h : 𝓢 ⊢ ◇□p)
:
Equations
- LO.System.diabox_box' h = LO.System.diabox_box⨀h
Instances For
theorem
LO.System.diabox_box'!
{F : Type u_1}
[LO.BasicModalLogicalConnective F]
[DecidableEq F]
{S : Type u_2}
[LO.System F S]
{p : F}
{𝓢 : S}
[LO.System.Classical 𝓢]
[LO.System.NegationEquiv 𝓢]
[LO.System.Necessitation 𝓢]
[LO.System.HasAxiomK 𝓢]
[LO.System.HasDiaDuality 𝓢]
[LO.System.HasAxiomFive 𝓢]
(h : 𝓢 ⊢! ◇□p)
:
def
LO.System.rm_diabox
{F : Type u_1}
[LO.BasicModalLogicalConnective F]
[DecidableEq F]
{S : Type u_2}
[LO.System F S]
{p : F}
{𝓢 : S}
[LO.System.Classical 𝓢]
[LO.System.NegationEquiv 𝓢]
[LO.System.Necessitation 𝓢]
[LO.System.HasAxiomK 𝓢]
[LO.System.HasDiaDuality 𝓢]
[LO.System.HasAxiomFive 𝓢]
[LO.System.HasAxiomT 𝓢]
:
Equations
- LO.System.rm_diabox = LO.System.impTrans'' LO.System.diabox_box LO.System.axiomT
Instances For
@[simp]
theorem
LO.System.rm_diabox!
{F : Type u_1}
[LO.BasicModalLogicalConnective F]
[DecidableEq F]
{S : Type u_2}
[LO.System F S]
{p : F}
{𝓢 : S}
[LO.System.Classical 𝓢]
[LO.System.NegationEquiv 𝓢]
[LO.System.Necessitation 𝓢]
[LO.System.HasAxiomK 𝓢]
[LO.System.HasDiaDuality 𝓢]
[LO.System.HasAxiomFive 𝓢]
[LO.System.HasAxiomT 𝓢]
:
def
LO.System.rm_diabox'
{F : Type u_1}
[LO.BasicModalLogicalConnective F]
[DecidableEq F]
{S : Type u_2}
[LO.System F S]
{p : F}
{𝓢 : S}
[LO.System.Classical 𝓢]
[LO.System.NegationEquiv 𝓢]
[LO.System.Necessitation 𝓢]
[LO.System.HasAxiomK 𝓢]
[LO.System.HasDiaDuality 𝓢]
[LO.System.HasAxiomFive 𝓢]
[LO.System.HasAxiomT 𝓢]
(h : 𝓢 ⊢ ◇□p)
:
𝓢 ⊢ p
Equations
- LO.System.rm_diabox' h = LO.System.rm_diabox⨀h
Instances For
theorem
LO.System.rm_diabox'!
{F : Type u_1}
[LO.BasicModalLogicalConnective F]
[DecidableEq F]
{S : Type u_2}
[LO.System F S]
{p : F}
{𝓢 : S}
[LO.System.Classical 𝓢]
[LO.System.NegationEquiv 𝓢]
[LO.System.Necessitation 𝓢]
[LO.System.HasAxiomK 𝓢]
[LO.System.HasDiaDuality 𝓢]
[LO.System.HasAxiomFive 𝓢]
[LO.System.HasAxiomT 𝓢]
(h : 𝓢 ⊢! ◇□p)
:
𝓢 ⊢! p
def
LO.System.axiomTc
{F : Type u_1}
[LO.BasicModalLogicalConnective F]
{S : Type u_2}
[LO.System F S]
{p : F}
{𝓢 : S}
[LO.System.HasAxiomTc 𝓢]
:
Equations
- LO.System.axiomTc = LO.System.HasAxiomTc.Tc p
Instances For
@[simp]
theorem
LO.System.axiomTc!
{F : Type u_1}
[LO.BasicModalLogicalConnective F]
{S : Type u_2}
[LO.System F S]
{p : F}
{𝓢 : S}
[LO.System.HasAxiomTc 𝓢]
:
instance
LO.System.instHasAxiomTcFiniteContext
{F : Type u_1}
[LO.BasicModalLogicalConnective F]
{S : Type u_2}
[LO.System F S]
{𝓢 : S}
[LO.System.Classical 𝓢]
[LO.System.HasAxiomTc 𝓢]
(Γ : LO.System.FiniteContext F 𝓢)
:
Equations
- LO.System.instHasAxiomTcFiniteContext Γ = { Tc := fun (x : F) => LO.System.FiniteContext.of LO.System.axiomTc }
instance
LO.System.instHasAxiomTcContext
{F : Type u_1}
[LO.BasicModalLogicalConnective F]
{S : Type u_2}
[LO.System F S]
{𝓢 : S}
[LO.System.Classical 𝓢]
[LO.System.HasAxiomTc 𝓢]
(Γ : LO.System.Context F 𝓢)
:
Equations
- LO.System.instHasAxiomTcContext Γ = { Tc := fun (x : F) => LO.System.Context.of LO.System.axiomTc }
instance
LO.System.instHasAxiomFour
{F : Type u_1}
[LO.BasicModalLogicalConnective F]
{S : Type u_2}
[LO.System F S]
{𝓢 : S}
[LO.System.HasAxiomTc 𝓢]
:
Equations
- LO.System.instHasAxiomFour = { Four := fun (x : F) => LO.System.axiomFour_of_Tc }
def
LO.System.diaT
{F : Type u_1}
[LO.BasicModalLogicalConnective F]
[DecidableEq F]
{S : Type u_2}
[LO.System F S]
{p : F}
{𝓢 : S}
[LO.System.Classical 𝓢]
[LO.System.NegationEquiv 𝓢]
[LO.System.HasAxiomTc 𝓢]
[LO.System.HasDiaDuality 𝓢]
:
Equations
- LO.System.diaT = LO.System.impTrans'' (LO.System.and₁' LO.System.diaDuality) (LO.System.contra₂' LO.System.axiomTc)
Instances For
@[simp]
theorem
LO.System.diaT!
{F : Type u_1}
[LO.BasicModalLogicalConnective F]
[DecidableEq F]
{S : Type u_2}
[LO.System F S]
{p : F}
{𝓢 : S}
[LO.System.Classical 𝓢]
[LO.System.NegationEquiv 𝓢]
[LO.System.HasAxiomTc 𝓢]
[LO.System.HasDiaDuality 𝓢]
:
def
LO.System.diaT'
{F : Type u_1}
[LO.BasicModalLogicalConnective F]
[DecidableEq F]
{S : Type u_2}
[LO.System F S]
{p : F}
{𝓢 : S}
[LO.System.Classical 𝓢]
[LO.System.NegationEquiv 𝓢]
[LO.System.HasAxiomTc 𝓢]
[LO.System.HasDiaDuality 𝓢]
(h : 𝓢 ⊢ ◇p)
:
𝓢 ⊢ p
Equations
- LO.System.diaT' h = LO.System.diaT⨀h
Instances For
theorem
LO.System.diaT'!
{F : Type u_1}
[LO.BasicModalLogicalConnective F]
[DecidableEq F]
{S : Type u_2}
[LO.System F S]
{p : F}
{𝓢 : S}
[LO.System.Classical 𝓢]
[LO.System.NegationEquiv 𝓢]
[LO.System.HasAxiomTc 𝓢]
[LO.System.HasDiaDuality 𝓢]
(h : 𝓢 ⊢! ◇p)
:
𝓢 ⊢! p
instance
LO.System.instHasAxiomFive
{F : Type u_1}
[LO.BasicModalLogicalConnective F]
{S : Type u_2}
[LO.System F S]
{𝓢 : S}
[LO.System.HasAxiomTc 𝓢]
:
Equations
- LO.System.instHasAxiomFive = { Five := fun (x : F) => LO.System.axiomFive_of_Tc }
instance
LO.System.instHasAxiomGrzOfHasAxiomT
{F : Type u_1}
[LO.BasicModalLogicalConnective F]
[DecidableEq F]
{S : Type u_2}
[LO.System F S]
{𝓢 : S}
[LO.System.Classical 𝓢]
[LO.System.Necessitation 𝓢]
[LO.System.HasAxiomTc 𝓢]
[LO.System.HasAxiomT 𝓢]
:
Equations
- LO.System.instHasAxiomGrzOfHasAxiomT = { Grz := fun (x : F) => LO.System.axiomGrz_of_Tc_and_T }
def
LO.System.axiomVer
{F : Type u_1}
[LO.BasicModalLogicalConnective F]
{S : Type u_2}
[LO.System F S]
{p : F}
{𝓢 : S}
[LO.System.HasAxiomVer 𝓢]
:
Equations
- LO.System.axiomVer = LO.System.HasAxiomVer.Ver p
Instances For
@[simp]
theorem
LO.System.axiomVer!
{F : Type u_1}
[LO.BasicModalLogicalConnective F]
{S : Type u_2}
[LO.System F S]
{p : F}
{𝓢 : S}
[LO.System.HasAxiomVer 𝓢]
:
instance
LO.System.instHasAxiomVerFiniteContext
{F : Type u_1}
[LO.BasicModalLogicalConnective F]
{S : Type u_2}
[LO.System F S]
{𝓢 : S}
[LO.System.Classical 𝓢]
[LO.System.HasAxiomVer 𝓢]
(Γ : LO.System.FiniteContext F 𝓢)
:
Equations
- LO.System.instHasAxiomVerFiniteContext Γ = { Ver := fun (x : F) => LO.System.FiniteContext.of LO.System.axiomVer }
instance
LO.System.instHasAxiomVerContext
{F : Type u_1}
[LO.BasicModalLogicalConnective F]
{S : Type u_2}
[LO.System F S]
{𝓢 : S}
[LO.System.Classical 𝓢]
[LO.System.HasAxiomVer 𝓢]
(Γ : LO.System.Context F 𝓢)
:
Equations
- LO.System.instHasAxiomVerContext Γ = { Ver := fun (x : F) => LO.System.Context.of LO.System.axiomVer }
instance
LO.System.instHasAxiomTc
{F : Type u_1}
[LO.BasicModalLogicalConnective F]
{S : Type u_2}
[LO.System F S]
{𝓢 : S}
[LO.System.Classical 𝓢]
[LO.System.HasAxiomVer 𝓢]
:
Equations
- LO.System.instHasAxiomTc = { Tc := fun (x : F) => LO.System.axiomTc_of_Ver }
instance
LO.System.instHasAxiomL
{F : Type u_1}
[LO.BasicModalLogicalConnective F]
{S : Type u_2}
[LO.System F S]
{𝓢 : S}
[LO.System.Classical 𝓢]
[LO.System.HasAxiomVer 𝓢]
:
Equations
- LO.System.instHasAxiomL = { L := fun (x : F) => LO.System.axiomL_of_Ver }
def
LO.System.bot_of_dia
{F : Type u_1}
[LO.BasicModalLogicalConnective F]
[DecidableEq F]
{S : Type u_2}
[LO.System F S]
{p : F}
{𝓢 : S}
[LO.System.Classical 𝓢]
[LO.System.HasAxiomVer 𝓢]
[LO.System.NegationEquiv 𝓢]
[LO.System.HasDiaDuality 𝓢]
:
Equations
- LO.System.bot_of_dia = let_fun this := LO.System.and₁' LO.System.neg_equiv; this⨀(LO.System.contra₀' (LO.System.and₁' LO.System.diaDuality)⨀LO.System.dni' LO.System.axiomVer)
Instances For
theorem
LO.System.bot_of_dia!
{F : Type u_1}
[LO.BasicModalLogicalConnective F]
[DecidableEq F]
{S : Type u_2}
[LO.System F S]
{p : F}
{𝓢 : S}
[LO.System.Classical 𝓢]
[LO.System.HasAxiomVer 𝓢]
[LO.System.NegationEquiv 𝓢]
[LO.System.HasDiaDuality 𝓢]
:
def
LO.System.bot_of_dia'
{F : Type u_1}
[LO.BasicModalLogicalConnective F]
[DecidableEq F]
{S : Type u_2}
[LO.System F S]
{p : F}
{𝓢 : S}
[LO.System.Classical 𝓢]
[LO.System.HasAxiomVer 𝓢]
[LO.System.NegationEquiv 𝓢]
[LO.System.HasDiaDuality 𝓢]
(h : 𝓢 ⊢ ◇p)
:
Equations
- LO.System.bot_of_dia' h = LO.System.bot_of_dia⨀h
Instances For
theorem
LO.System.bot_of_dia'!
{F : Type u_1}
[LO.BasicModalLogicalConnective F]
[DecidableEq F]
{S : Type u_2}
[LO.System F S]
{p : F}
{𝓢 : S}
[LO.System.Classical 𝓢]
[LO.System.HasAxiomVer 𝓢]
[LO.System.NegationEquiv 𝓢]
[LO.System.HasDiaDuality 𝓢]
(h : 𝓢 ⊢! ◇p)
:
def
LO.System.axiomL
{F : Type u_1}
[LO.BasicModalLogicalConnective F]
{S : Type u_2}
[LO.System F S]
{p : F}
{𝓢 : S}
[LO.System.HasAxiomL 𝓢]
:
Equations
- LO.System.axiomL = LO.System.HasAxiomL.L p
Instances For
@[simp]
theorem
LO.System.axiomL!
{F : Type u_1}
[LO.BasicModalLogicalConnective F]
{S : Type u_2}
[LO.System F S]
{p : F}
{𝓢 : S}
[LO.System.HasAxiomL 𝓢]
:
instance
LO.System.instHasAxiomLFiniteContext
{F : Type u_1}
[LO.BasicModalLogicalConnective F]
{S : Type u_2}
[LO.System F S]
{𝓢 : S}
[LO.System.Classical 𝓢]
[LO.System.HasAxiomL 𝓢]
(Γ : LO.System.FiniteContext F 𝓢)
:
Equations
- LO.System.instHasAxiomLFiniteContext Γ = { L := fun (x : F) => LO.System.FiniteContext.of LO.System.axiomL }
instance
LO.System.instHasAxiomLContext
{F : Type u_1}
[LO.BasicModalLogicalConnective F]
{S : Type u_2}
[LO.System F S]
{𝓢 : S}
[LO.System.Classical 𝓢]
[LO.System.HasAxiomL 𝓢]
(Γ : LO.System.Context F 𝓢)
:
Equations
- LO.System.instHasAxiomLContext Γ = { L := fun (x : F) => LO.System.Context.of LO.System.axiomL }
instance
LO.System.instHasAxiomFour_1
{F : Type u_1}
[LO.BasicModalLogicalConnective F]
[DecidableEq F]
{S : Type u_2}
[LO.System F S]
{𝓢 : S}
[LO.System.Classical 𝓢]
[LO.System.Necessitation 𝓢]
[LO.System.HasAxiomK 𝓢]
[LO.System.HasAxiomL 𝓢]
:
Equations
- LO.System.instHasAxiomFour_1 = { Four := fun (x : F) => LO.System.axiomFour_of_L }
def
LO.System.goedel2
{F : Type u_1}
[LO.BasicModalLogicalConnective F]
[DecidableEq F]
{S : Type u_2}
[LO.System F S]
{𝓢 : S}
[LO.System.Classical 𝓢]
[LO.System.NegationEquiv 𝓢]
[LO.System.Necessitation 𝓢]
[LO.System.HasAxiomK 𝓢]
[LO.System.HasAxiomL 𝓢]
:
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
LO.System.goedel2!
{F : Type u_1}
[LO.BasicModalLogicalConnective F]
[DecidableEq F]
{S : Type u_2}
[LO.System F S]
{𝓢 : S}
[LO.System.Classical 𝓢]
[LO.System.NegationEquiv 𝓢]
[LO.System.Necessitation 𝓢]
[LO.System.HasAxiomK 𝓢]
[LO.System.HasAxiomL 𝓢]
:
def
LO.System.goedel2'.mp
{F : Type u_1}
[LO.BasicModalLogicalConnective F]
[DecidableEq F]
{S : Type u_2}
[LO.System F S]
{𝓢 : S}
[LO.System.Classical 𝓢]
[LO.System.NegationEquiv 𝓢]
[LO.System.Necessitation 𝓢]
[LO.System.HasAxiomK 𝓢]
[LO.System.HasAxiomL 𝓢]
:
Equations
- LO.System.goedel2'.mp h = LO.System.and₁' LO.System.goedel2⨀h
Instances For
def
LO.System.goedel2'.mpr
{F : Type u_1}
[LO.BasicModalLogicalConnective F]
[DecidableEq F]
{S : Type u_2}
[LO.System F S]
{𝓢 : S}
[LO.System.Classical 𝓢]
[LO.System.NegationEquiv 𝓢]
[LO.System.Necessitation 𝓢]
[LO.System.HasAxiomK 𝓢]
[LO.System.HasAxiomL 𝓢]
:
Equations
- LO.System.goedel2'.mpr h = LO.System.and₂' LO.System.goedel2⨀h
Instances For
theorem
LO.System.goedel2'!
{F : Type u_1}
[LO.BasicModalLogicalConnective F]
[DecidableEq F]
{S : Type u_2}
[LO.System F S]
{𝓢 : S}
[LO.System.Classical 𝓢]
[LO.System.NegationEquiv 𝓢]
[LO.System.Necessitation 𝓢]
[LO.System.HasAxiomK 𝓢]
[LO.System.HasAxiomL 𝓢]
:
instance
LO.System.instHasAxiomH
{F : Type u_1}
[LO.BasicModalLogicalConnective F]
{S : Type u_2}
[LO.System F S]
{𝓢 : S}
[LO.System.Classical 𝓢]
[LO.System.Necessitation 𝓢]
[LO.System.HasAxiomK 𝓢]
[LO.System.HasAxiomL 𝓢]
:
Equations
- LO.System.instHasAxiomH = { H := fun (x : F) => LO.System.axiomH_of_GL }
noncomputable def
LO.System.boxdot_Grz_of_L
{F : Type u_1}
[LO.BasicModalLogicalConnective F]
[DecidableEq F]
{S : Type u_2}
[LO.System F S]
{p : F}
{𝓢 : S}
[LO.System.Classical 𝓢]
[LO.System.NegationEquiv 𝓢]
[LO.System.Necessitation 𝓢]
[LO.System.HasAxiomK 𝓢]
[LO.System.HasAxiomFour 𝓢]
[LO.System.HasAxiomL 𝓢]
:
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
LO.System.boxdot_Grz_of_L!
{F : Type u_1}
[LO.BasicModalLogicalConnective F]
[DecidableEq F]
{S : Type u_2}
[LO.System F S]
{p : F}
{𝓢 : S}
[LO.System.Classical 𝓢]
[LO.System.NegationEquiv 𝓢]
[LO.System.Necessitation 𝓢]
[LO.System.HasAxiomK 𝓢]
[LO.System.HasAxiomFour 𝓢]
[LO.System.HasAxiomL 𝓢]
:
def
LO.System.axiomH
{F : Type u_1}
[LO.BasicModalLogicalConnective F]
{S : Type u_2}
[LO.System F S]
{p : F}
{𝓢 : S}
[LO.System.HasAxiomH 𝓢]
:
Equations
- LO.System.axiomH = LO.System.HasAxiomH.H p
Instances For
@[simp]
theorem
LO.System.axiomH!
{F : Type u_1}
[LO.BasicModalLogicalConnective F]
{S : Type u_2}
[LO.System F S]
{p : F}
{𝓢 : S}
[LO.System.HasAxiomH 𝓢]
:
instance
LO.System.instHasAxiomHFiniteContext
{F : Type u_1}
[LO.BasicModalLogicalConnective F]
{S : Type u_2}
[LO.System F S]
{𝓢 : S}
[LO.System.Classical 𝓢]
[LO.System.HasAxiomH 𝓢]
(Γ : LO.System.FiniteContext F 𝓢)
:
Equations
- LO.System.instHasAxiomHFiniteContext Γ = { H := fun (x : F) => LO.System.FiniteContext.of LO.System.axiomH }
instance
LO.System.instHasAxiomHContext
{F : Type u_1}
[LO.BasicModalLogicalConnective F]
{S : Type u_2}
[LO.System F S]
{𝓢 : S}
[LO.System.Classical 𝓢]
[LO.System.HasAxiomH 𝓢]
(Γ : LO.System.Context F 𝓢)
:
Equations
- LO.System.instHasAxiomHContext Γ = { H := fun (x : F) => LO.System.Context.of LO.System.axiomH }
def
LO.System.loeb
{S : Type u_1}
{F : Type u_2}
[LO.LogicalConnective F]
[LO.BasicModalLogicalConnective F]
[LO.System F S]
{𝓢 : S}
[self : LO.System.LoebRule 𝓢]
{p : F}
:
Alias of LO.System.LoebRule.loeb
.
Equations
Instances For
theorem
LO.System.loeb!
{F : Type u_1}
[LO.BasicModalLogicalConnective F]
{S : Type u_2}
[LO.System F S]
{p : F}
{𝓢 : S}
[LO.System.LoebRule 𝓢]
:
instance
LO.System.instHasAxiomLOfK4Loeb
{F : Type u_1}
[LO.BasicModalLogicalConnective F]
[DecidableEq F]
{S : Type u_2}
[LO.System F S]
{𝓢 : S}
[LO.System.Classical 𝓢]
[LO.System.HasAxiomK 𝓢]
[LO.System.HasAxiomFour 𝓢]
[LO.System.K4Loeb 𝓢]
:
Equations
- LO.System.instHasAxiomLOfK4Loeb = { L := fun (x : F) => LO.System.axiomL_of_K4Loeb }
def
LO.System.henkin
{S : Type u_1}
{F : Type u_2}
[LO.LogicalConnective F]
[LO.BasicModalLogicalConnective F]
[LO.System F S]
{𝓢 : S}
[self : LO.System.HenkinRule 𝓢]
{p : F}
:
Alias of LO.System.HenkinRule.henkin
.
Instances For
theorem
LO.System.henkin!
{F : Type u_1}
[LO.BasicModalLogicalConnective F]
{S : Type u_2}
[LO.System F S]
{p : F}
{𝓢 : S}
[LO.System.HenkinRule 𝓢]
:
instance
LO.System.instLoebRuleOfHasAxiomFourOfHenkinRule
{F : Type u_1}
[LO.BasicModalLogicalConnective F]
{S : Type u_2}
[LO.System F S]
{𝓢 : S}
[LO.System.Classical 𝓢]
[LO.System.Necessitation 𝓢]
[LO.System.HasAxiomK 𝓢]
[LO.System.HasAxiomFour 𝓢]
[LO.System.HenkinRule 𝓢]
:
Equations
- One or more equations did not get rendered due to their size.
instance
LO.System.instHenkinRuleOfHasAxiomFourOfHasAxiomH
{F : Type u_1}
[LO.BasicModalLogicalConnective F]
{S : Type u_2}
[LO.System F S]
{𝓢 : S}
[LO.System.Classical 𝓢]
[LO.System.Necessitation 𝓢]
[LO.System.HasAxiomFour 𝓢]
[LO.System.HasAxiomH 𝓢]
:
Equations
- LO.System.instHenkinRuleOfHasAxiomFourOfHasAxiomH = { henkin := fun {p : F} (h : 𝓢 ⊢ □p ⭤ p) => LO.System.and₁' h⨀(LO.System.axiomH⨀LO.System.nec h) }
def
LO.System.unnec
{S : Type u_1}
{F : Type u_2}
[LO.BasicModalLogicalConnective F]
[LO.System F S]
{𝓢 : S}
[self : LO.System.Unnecessitation 𝓢]
{p : F}
:
Alias of LO.System.Unnecessitation.unnec
.
Instances For
theorem
LO.System.unnec!
{F : Type u_1}
[LO.BasicModalLogicalConnective F]
{S : Type u_2}
[LO.System F S]
{p : F}
{𝓢 : S}
[LO.System.Unnecessitation 𝓢]
:
def
LO.System.multiunnec
{F : Type u_1}
[LO.BasicModalLogicalConnective F]
{S : Type u_2}
[LO.System F S]
{p : F}
{𝓢 : S}
[LO.System.Unnecessitation 𝓢]
{n : ℕ}
:
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
LO.System.multiunnec!
{F : Type u_1}
[LO.BasicModalLogicalConnective F]
{S : Type u_2}
[LO.System F S]
{p : F}
{𝓢 : S}
[LO.System.Unnecessitation 𝓢]
{n : ℕ}
:
instance
LO.System.instUnnecessitationOfHasAxiomT
{F : Type u_1}
[LO.BasicModalLogicalConnective F]
{S : Type u_2}
[LO.System F S]
{𝓢 : S}
[LO.System.Classical 𝓢]
[LO.System.HasAxiomT 𝓢]
:
def
LO.System.imply_boxdot_boxdot_of_imply_boxdot_plain
{F : Type u_1}
[LO.BasicModalLogicalConnective F]
[DecidableEq F]
{S : Type u_2}
[LO.System F S]
{p : F}
{q : F}
{𝓢 : S}
[LO.System.Classical 𝓢]
[LO.System.Necessitation 𝓢]
[LO.System.HasAxiomK 𝓢]
[LO.System.HasAxiomFour 𝓢]
(h : 𝓢 ⊢ ⊡p ➝ q)
:
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
LO.System.imply_boxdot_boxdot_of_imply_boxdot_plain!
{F : Type u_1}
[LO.BasicModalLogicalConnective F]
[DecidableEq F]
{S : Type u_2}
[LO.System F S]
{p : F}
{q : F}
{𝓢 : S}
[LO.System.Classical 𝓢]
[LO.System.Necessitation 𝓢]
[LO.System.HasAxiomK 𝓢]
[LO.System.HasAxiomFour 𝓢]
(h : 𝓢 ⊢! ⊡p ➝ q)
:
def
LO.System.imply_boxdot_axiomT_of_imply_boxdot_boxdot
{F : Type u_1}
[LO.BasicModalLogicalConnective F]
[DecidableEq F]
{S : Type u_2}
[LO.System F S]
{p : F}
{q : F}
{𝓢 : S}
[LO.System.Classical 𝓢]
(h : 𝓢 ⊢ ⊡p ➝ ⊡q)
:
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
LO.System.imply_boxdot_axiomT_of_imply_boxdot_boxdot!
{F : Type u_1}
[LO.BasicModalLogicalConnective F]
[DecidableEq F]
{S : Type u_2}
[LO.System F S]
{p : F}
{q : F}
{𝓢 : S}
[LO.System.Classical 𝓢]
(h : 𝓢 ⊢! ⊡p ➝ ⊡q)
:
def
LO.System.imply_box_box_of_imply_boxdot_axiomT
{F : Type u_1}
[LO.BasicModalLogicalConnective F]
[DecidableEq F]
{S : Type u_2}
[LO.System F S]
{p : F}
{q : F}
{𝓢 : S}
[LO.System.Classical 𝓢]
[LO.System.Necessitation 𝓢]
[LO.System.HasAxiomK 𝓢]
[LO.System.HasAxiomFour 𝓢]
[LO.System.HasAxiomL 𝓢]
(h : 𝓢 ⊢ ⊡p ➝ □q ➝ q)
:
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
LO.System.imply_box_box_of_imply_boxdot_axiomT!
{F : Type u_1}
[LO.BasicModalLogicalConnective F]
[DecidableEq F]
{S : Type u_2}
[LO.System F S]
{p : F}
{q : F}
{𝓢 : S}
[LO.System.Classical 𝓢]
[LO.System.Necessitation 𝓢]
[LO.System.HasAxiomK 𝓢]
[LO.System.HasAxiomFour 𝓢]
[LO.System.HasAxiomL 𝓢]
(h : 𝓢 ⊢! ⊡p ➝ □q ➝ q)
:
theorem
LO.System.imply_box_box_of_imply_boxdot_plain!
{F : Type u_1}
[LO.BasicModalLogicalConnective F]
[DecidableEq F]
{S : Type u_2}
[LO.System F S]
{p : F}
{q : F}
{𝓢 : S}
[LO.System.Classical 𝓢]
[LO.System.Necessitation 𝓢]
[LO.System.HasAxiomK 𝓢]
[LO.System.HasAxiomFour 𝓢]
[LO.System.HasAxiomL 𝓢]
(h : 𝓢 ⊢! ⊡p ➝ q)
:
def
LO.System.axiomGrz
{F : Type u_1}
[LO.BasicModalLogicalConnective F]
{S : Type u_2}
[LO.System F S]
{p : F}
{𝓢 : S}
[LO.System.HasAxiomGrz 𝓢]
:
Equations
- LO.System.axiomGrz = LO.System.HasAxiomGrz.Grz p
Instances For
@[simp]
theorem
LO.System.axiomGrz!
{F : Type u_1}
[LO.BasicModalLogicalConnective F]
{S : Type u_2}
[LO.System F S]
{p : F}
{𝓢 : S}
[LO.System.HasAxiomGrz 𝓢]
:
instance
LO.System.instHasAxiomGrzFiniteContext
{F : Type u_1}
[LO.BasicModalLogicalConnective F]
{S : Type u_2}
[LO.System F S]
{𝓢 : S}
[LO.System.Classical 𝓢]
[LO.System.HasAxiomGrz 𝓢]
(Γ : LO.System.FiniteContext F 𝓢)
:
Equations
- LO.System.instHasAxiomGrzFiniteContext Γ = { Grz := fun (x : F) => LO.System.FiniteContext.of LO.System.axiomGrz }
instance
LO.System.instHasAxiomGrzContext
{F : Type u_1}
[LO.BasicModalLogicalConnective F]
{S : Type u_2}
[LO.System F S]
{𝓢 : S}
[LO.System.Classical 𝓢]
[LO.System.HasAxiomGrz 𝓢]
(Γ : LO.System.Context F 𝓢)
:
Equations
- LO.System.instHasAxiomGrzContext Γ = { Grz := fun (x : F) => LO.System.Context.of LO.System.axiomGrz }
noncomputable def
LO.System.lemma_Grz₁
{F : Type u_1}
[LO.BasicModalLogicalConnective F]
[DecidableEq F]
{S : Type u_2}
[LO.System F S]
{p : F}
{𝓢 : S}
[LO.System.Classical 𝓢]
[LO.System.NegationEquiv 𝓢]
[LO.System.Necessitation 𝓢]
[LO.System.HasAxiomK 𝓢]
:
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
LO.System.lemma_Grz₁!
{F : Type u_1}
[LO.BasicModalLogicalConnective F]
[DecidableEq F]
{S : Type u_2}
[LO.System F S]
{p : F}
{𝓢 : S}
[LO.System.Classical 𝓢]
[LO.System.NegationEquiv 𝓢]
[LO.System.Necessitation 𝓢]
[LO.System.HasAxiomK 𝓢]
:
noncomputable def
LO.System.lemma_Grz₂
{F : Type u_1}
[LO.BasicModalLogicalConnective F]
[DecidableEq F]
{S : Type u_2}
[LO.System F S]
{p : F}
{𝓢 : S}
[LO.System.Classical 𝓢]
[LO.System.NegationEquiv 𝓢]
[LO.System.Necessitation 𝓢]
[LO.System.HasAxiomK 𝓢]
[LO.System.HasAxiomGrz 𝓢]
:
Equations
- LO.System.lemma_Grz₂ = LO.System.impTrans'' LO.System.lemma_Grz₁ LO.System.axiomGrz
Instances For
noncomputable instance
LO.System.instHasAxiomFour_2
{F : Type u_1}
[LO.BasicModalLogicalConnective F]
[DecidableEq F]
{S : Type u_2}
[LO.System F S]
{𝓢 : S}
[LO.System.Classical 𝓢]
[LO.System.NegationEquiv 𝓢]
[LO.System.Necessitation 𝓢]
[LO.System.HasAxiomK 𝓢]
[LO.System.HasAxiomGrz 𝓢]
:
Equations
- LO.System.instHasAxiomFour_2 = { Four := fun (x : F) => LO.System.Four_of_Grz }
noncomputable instance
LO.System.instHasAxiomT
{F : Type u_1}
[LO.BasicModalLogicalConnective F]
[DecidableEq F]
{S : Type u_2}
[LO.System F S]
{𝓢 : S}
[LO.System.Classical 𝓢]
[LO.System.NegationEquiv 𝓢]
[LO.System.Necessitation 𝓢]
[LO.System.HasAxiomK 𝓢]
[LO.System.HasAxiomGrz 𝓢]
:
Equations
- LO.System.instHasAxiomT = { T := fun (x : F) => LO.System.T_of_Grz }
instance
LO.System.instHasAxiomTcOfHasAxiomTOfHasAxiomFiveOfHasAxiomGrzOfHasDiaDuality
{F : Type u_1}
[LO.BasicModalLogicalConnective F]
[DecidableEq F]
{S : Type u_2}
[LO.System F S]
{𝓢 : S}
[LO.System.Classical 𝓢]
[LO.System.NegationEquiv 𝓢]
[LO.System.Necessitation 𝓢]
[LO.System.HasAxiomK 𝓢]
[LO.System.HasAxiomT 𝓢]
[LO.System.HasAxiomFive 𝓢]
[LO.System.HasAxiomGrz 𝓢]
[LO.System.HasDiaDuality 𝓢]
:
Equations
- LO.System.instHasAxiomTcOfHasAxiomTOfHasAxiomFiveOfHasAxiomGrzOfHasDiaDuality = { Tc := fun (x : F) => LO.System.Tc_of_S5Grz }
theorem
LO.System.contextual_nec!
{F : Type u_1}
[LO.BasicModalLogicalConnective F]
[DecidableEq F]
{S : Type u_2}
[LO.System F S]
{p : F}
{Γ : List F}
{𝓢 : S}
[LO.System.Classical 𝓢]
[LO.System.Necessitation 𝓢]
[LO.System.HasAxiomK 𝓢]
(h : Γ ⊢[𝓢]! p)
:
theorem
LO.System.ModalDisjunctive.modal_disjunctive
{F : Type u_1}
[LO.LogicalConnective F]
[LO.Box F]
{S : Type u_2}
[LO.System F S]
{𝓢 : S}
[self : LO.System.ModalDisjunctive 𝓢]
{p : F}
{q : F}
: