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

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)

• nec : {p : F} → 𝓢 ⊢ p → 𝓢 ⊢ □p

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)

• unnec : {p : F} → 𝓢 ⊢ □p → 𝓢 ⊢ p

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)

• loeb : {p : F} → 𝓢 ⊢ □p ⟶ p → 𝓢 ⊢ p

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)

• henkin : {p : F} → 𝓢 ⊢ □p ⟷ p → 𝓢 ⊢ p

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

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

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

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

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

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

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

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

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

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

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

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

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

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)

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)

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)

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)

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)

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)

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)

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)

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)

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)

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)

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)

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)

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)

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)

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)

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} : 𝓢 ⊢ p → 𝓢 ⊢ □p

Alias of LO.System.Necessitation.nec.

Equations

• @LO.System.nec = @LO.System.Necessitation.nec

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 𝓢] : 𝓢 ⊢! p → 𝓢 ⊢! □p

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 : ℕ} : 𝓢 ⊢ p → 𝓢 ⊢ □^[n]p

Equations

• LO.System.multinec h = Nat.recAux (id h) (fun (n : ℕ) (ih : 𝓢 ⊢ □^[n]p) => ⋯.mpr (LO.System.nec ih)) n

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 : ℕ} : 𝓢 ⊢! p → 𝓢 ⊢! □^[n]p

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 𝓢] : 𝓢 ⊢ □(p ⟶ q) ⟶ □p ⟶ □q

Equations

• LO.System.axiomK = LO.System.HasAxiomK.K p q

@[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 𝓢] : 𝓢 ⊢! □(p ⟶ q) ⟶ □p ⟶ □q

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 𝓢) : LO.System.HasAxiomK Γ

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 𝓢) : LO.System.HasAxiomK Γ

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)) : 𝓢 ⊢ □p ⟶ □q

Equations

• LO.System.axiomK' h = LO.System.axiomK⨀h

@[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)) : 𝓢 ⊢! □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) : 𝓢 ⊢ □q

Equations

• LO.System.axiomK'' h₁ h₂ = LO.System.axiomK' h₁⨀h₂

@[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) : 𝓢 ⊢! □q

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 : ℕ} : 𝓢 ⊢ □^[n](p ⟶ q) ⟶ □^[n]p ⟶ □^[n]q

Equations

• One or more equations did not get rendered due to their size.

@[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 : ℕ} : 𝓢 ⊢! □^[n](p ⟶ q) ⟶ □^[n]p ⟶ □^[n]q

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)) : 𝓢 ⊢ □^[n]p ⟶ □^[n]q

Equations

• LO.System.multibox_axiomK' h = LO.System.multibox_axiomK⨀h

@[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)) : 𝓢 ⊢! □^[n]p ⟶ □^[n]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)) : 𝓢 ⊢ □^[n]p ⟶ □^[n]q

Alias of LO.System.multibox_axiomK'.

Equations

• @LO.System.multiboxedImplyDistribute = @LO.System.multibox_axiomK'

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)) : 𝓢 ⊢! □^[n]p ⟶ □^[n]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) : 𝓢 ⊢ □p ⟷ □q

Equations

• LO.System.boxIff' h = LO.System.iffIntro (LO.System.axiomK' (LO.System.nec (LO.System.and₁' h))) (LO.System.axiomK' (LO.System.nec (LO.System.and₂' h)))

@[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) : 𝓢 ⊢! □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) : 𝓢 ⊢ □^[n]p ⟷ □^[n]q

Equations

• LO.System.multiboxIff' h = Nat.recAux (id h) (fun (n : ℕ) (ih : 𝓢 ⊢ □^[n]p ⟷ □^[n]q) => ⋯.mpr (LO.System.boxIff' ih)) n

@[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) : 𝓢 ⊢! □^[n]p ⟷ □^[n]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 𝓢] : LO.System.HasDiaDuality 𝓢

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] : LO.System.HasDiaDuality 𝓢

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 𝓢] : 𝓢 ⊢ ◇p ⟷ ~□(~p)

Equations

• LO.System.diaDuality = LO.System.HasDiaDuality.dia_dual p

@[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 𝓢] : 𝓢 ⊢! ◇p ⟷ ~□(~p)

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) : 𝓢 ⊢ ~□(~p)

Equations

• LO.System.diaDuality'.mp h = LO.System.and₁' LO.System.diaDuality⨀h

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)) : 𝓢 ⊢ ◇p

Equations

• LO.System.diaDuality'.mpr h = LO.System.and₂' LO.System.diaDuality⨀h

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 𝓢] : 𝓢 ⊢! ◇p ↔ 𝓢 ⊢! ~□(~p)

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 𝓢] {n : ℕ} [LO.System.HasDiaDuality 𝓢] : 𝓢 ⊢ ◇^[n]p ⟷ ~□^[n](~p)

Equations

• One or more equations did not get rendered due to their size.

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 𝓢] {n : ℕ} [LO.System.HasDiaDuality 𝓢] : 𝓢 ⊢! ◇^[n]p ⟷ ~□^[n](~p)

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 : ℕ} : 𝓢 ⊢! ◇^[n]p ↔ 𝓢 ⊢! ~□^[n](~p)

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) : 𝓢 ⊢ ◇p ⟷ ◇q

Equations

• One or more equations did not get rendered due to their size.

@[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) : 𝓢 ⊢! ◇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) : 𝓢 ⊢ ◇^[n]p ⟷ ◇^[n]q

Equations

• LO.System.multidiaIff' h = Nat.recAux (id h) (fun (n : ℕ) (ih : 𝓢 ⊢ ◇^[n]p ⟷ ◇^[n]q) => ⋯.mpr (LO.System.diaIff' ih)) n

@[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) : 𝓢 ⊢! ◇^[n]p ⟷ ◇^[n]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 : ℕ} : 𝓢 ⊢ □^[n]p ⟷ ~◇^[n](~p)

Equations

• One or more equations did not get rendered due to their size.

@[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 : ℕ} : 𝓢 ⊢! □^[n]p ⟷ ~◇^[n](~p)

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 𝓢] : 𝓢 ⊢ □p ⟷ ~◇(~p)

Equations

• LO.System.boxDuality = LO.System.multiboxDuality

@[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 𝓢] : 𝓢 ⊢! □p ⟷ ~◇(~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 : ℕ} : 𝓢 ⊢! □^[n]p ↔ 𝓢 ⊢! ~◇^[n](~p)

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 𝓢] : 𝓢 ⊢! □p ↔ 𝓢 ⊢! ~◇(~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 : ℕ} : 𝓢 ⊢ □^[n]⊤

Equations

• LO.System.multiboxverum = LO.System.multinec LO.System.verum

@[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 : ℕ} : 𝓢 ⊢! □^[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

@[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

@[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) : 𝓢 ⊢ □^[n]p ⟶ □^[n]q

Equations

• LO.System.implyMultiboxDistribute' h = LO.System.multibox_axiomK' (LO.System.multinec h)

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) : 𝓢 ⊢! □^[n]p ⟶ □^[n]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) : 𝓢 ⊢ □p ⟶ □q

Equations

• LO.System.implyBoxDistribute' h = LO.System.implyMultiboxDistribute' h

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) : 𝓢 ⊢! □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 : ℕ} : 𝓢 ⊢ □^[n](p ⋏ q) ⟶ □^[n]p ⋏ □^[n]q

Equations

• LO.System.distribute_multibox_and = LO.System.implyRightAnd (LO.System.implyMultiboxDistribute' LO.System.and₁) (LO.System.implyMultiboxDistribute' LO.System.and₂)

@[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 : ℕ} : 𝓢 ⊢! □^[n](p ⋏ q) ⟶ □^[n]p ⋏ □^[n]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 𝓢] : 𝓢 ⊢ □(p ⋏ q) ⟶ □p ⋏ □q

Equations

• LO.System.distribute_box_and = LO.System.distribute_multibox_and

@[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 𝓢] : 𝓢 ⊢! □(p ⋏ q) ⟶ □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 : ℕ} (h : 𝓢 ⊢ □^[n](p ⋏ q)) : 𝓢 ⊢ □^[n]p ⋏ □^[n]q

Equations

• LO.System.distribute_multibox_and' h = LO.System.distribute_multibox_and⨀h

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)) : 𝓢 ⊢! □^[n]p ⋏ □^[n]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)) : 𝓢 ⊢ □p ⋏ □q

Equations

• LO.System.distribute_box_and' h = LO.System.distribute_multibox_and' h

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)) : 𝓢 ⊢! □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 𝓢] : 𝓢 ⊢! p ⋏ ⋀Γ ⟷ ⋀(p :: Γ)

@[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 : ℕ} : 𝓢 ⊢! □^[n]⋀Γ ⟶ ⋀□'^[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 : ℕ} : 𝓢 ⊢ □^[n]p ⋏ □^[n]q ⟶ □^[n](p ⋏ q)

Equations

• One or more equations did not get rendered due to their size.

@[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 : ℕ} : 𝓢 ⊢! □^[n]p ⋏ □^[n]q ⟶ □^[n](p ⋏ 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 𝓢] : 𝓢 ⊢ □p ⋏ □q ⟶ □(p ⋏ q)

Equations

• LO.System.collect_box_and = LO.System.collect_multibox_and

@[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 𝓢] : 𝓢 ⊢! □p ⋏ □q ⟶ □(p ⋏ q)

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) : 𝓢 ⊢ □^[n](p ⋏ q)

Equations

• LO.System.collect_multibox_and' h = LO.System.collect_multibox_and⨀h

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) : 𝓢 ⊢! □^[n](p ⋏ 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) : 𝓢 ⊢ □(p ⋏ q)

Equations

• LO.System.collect_box_and' h = LO.System.collect_multibox_and' h

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) : 𝓢 ⊢! □(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 : ℕ} : 𝓢 ⊢! □^[n]⋀Γ ↔ ∀ p ∈ Γ, 𝓢 ⊢! □^[n]p

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 𝓢] : 𝓢 ⊢! □⋀Γ ↔ ∀ p ∈ Γ, 𝓢 ⊢! □p

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]Γ) : 𝓢 ⊢! □^[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 : ℕ} : 𝓢 ⊢! ⋀□'^[n](p :: Γ) ⟶ ⋀□'^[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 : ℕ} : 𝓢 ⊢! ⋀□'^[n](p :: Γ) ⟶ □^[n]p

@[simp]

theorem LO.System.multibox_cons_conj! {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 : ℕ} : 𝓢 ⊢! ⋀□'^[n](p :: Γ) ⟶ ⋀□'^[n]Γ ⋏ □^[n]p

@[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 : ℕ} : 𝓢 ⊢! ⋀□'^[n]Γ ⟶ □^[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 : ℕ} : 𝓢 ⊢ □^[n]p ⋎ □^[n]q ⟶ □^[n](p ⋎ q)

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₂))

@[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 : ℕ} : 𝓢 ⊢! □^[n]p ⋎ □^[n]q ⟶ □^[n](p ⋎ 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 𝓢] : 𝓢 ⊢ □p ⋎ □q ⟶ □(p ⋎ q)

Equations

• LO.System.collect_box_or = LO.System.collect_multibox_or

@[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 𝓢] : 𝓢 ⊢! □p ⋎ □q ⟶ □(p ⋎ q)

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) : 𝓢 ⊢ □^[n](p ⋎ q)

Equations

• LO.System.collect_multibox_or' h = LO.System.collect_multibox_or⨀h

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) : 𝓢 ⊢! □^[n](p ⋎ 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) : 𝓢 ⊢ □(p ⋎ q)

Equations

• LO.System.collect_box_or' h = LO.System.collect_multibox_or' h

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) : 𝓢 ⊢! □(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 𝓢] : 𝓢 ⊢ ◇p ⟶ ◇(p ⋎ q)

Equations

• One or more equations did not get rendered due to their size.

@[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 𝓢] : 𝓢 ⊢! ◇p ⟶ ◇(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 𝓢] : 𝓢 ⊢ ◇q ⟶ ◇(p ⋎ q)

Equations

• One or more equations did not get rendered due to their size.

@[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 𝓢] : 𝓢 ⊢! ◇q ⟶ ◇(p ⋎ q)

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 𝓢] : 𝓢 ⊢ ◇p ⋎ ◇q ⟶ ◇(p ⋎ q)

Equations

• LO.System.collect_dia_or = LO.System.or₃'' LO.System.diaOrInst₁ LO.System.diaOrInst₂

@[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 𝓢] : 𝓢 ⊢! ◇p ⋎ ◇q ⟶ ◇(p ⋎ q)

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) : 𝓢 ⊢ ◇(p ⋎ q)

Equations

• LO.System.collect_dia_or' h = LO.System.collect_dia_or⨀h

@[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) : 𝓢 ⊢! ◇(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 : ℕ} : 𝓢 ⊢! ◇^[n](p ⋏ q) ⟶ ◇^[n]p ⋏ ◇^[n]q

@[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 𝓢] : 𝓢 ⊢! ◇(p ⋏ q) ⟶ ◇p ⋏ ◇q

@[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 : ℕ} : 𝓢 ⊢! ◇^[n]⋀Γ ⟶ ⋀◇'^[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)) : 𝓢 ⊢! ◇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 𝓢] : 𝓢 ⊢ ⊡(p ⟶ q) ⟶ ⊡p ⟶ ⊡q

Equations

• One or more equations did not get rendered due to their size.

@[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 𝓢] : 𝓢 ⊢! ⊡(p ⟶ q) ⟶ ⊡p ⟶ ⊡q

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 𝓢] : 𝓢 ⊢ ⊡p ⟶ p

Equations

• LO.System.boxdotAxiomT = LO.System.and₁

@[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 𝓢] : 𝓢 ⊢! ⊡p ⟶ p

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) : 𝓢 ⊢ ⊡p

Equations

• LO.System.boxdotNec d = LO.System.and₃' d (LO.System.nec d)

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) : 𝓢 ⊢! ⊡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 𝓢] : 𝓢 ⊢ ⊡p ⟶ □p

Equations

• LO.System.boxdotBox = LO.System.and₂

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 𝓢] : 𝓢 ⊢! ⊡p ⟶ □p

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 𝓢] : 𝓢 ⊢ □⊡p ⟶ ⊡□p

Equations

• LO.System.BoxBoxdot_BoxDotbox = LO.System.impTrans'' LO.System.distribute_box_and (LO.System.impId (□p ⋏ □□p))

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 𝓢] : 𝓢 ⊢! □⊡p ⟶ ⊡□p

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 𝓢] : 𝓢 ⊢ □p ⟶ p

Equations

• LO.System.axiomT = LO.System.HasAxiomT.T p

@[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 𝓢] : 𝓢 ⊢! □p ⟶ p

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 𝓢) : LO.System.HasAxiomT Γ

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 𝓢) : LO.System.HasAxiomT Γ

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

@[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 𝓢] : 𝓢 ⊢ p ⟶ ◇p

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)

@[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 𝓢] : 𝓢 ⊢! 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 𝓢] (h : 𝓢 ⊢ p) : 𝓢 ⊢ ◇p

Equations

• LO.System.diaTc' h = LO.System.diaTc⨀h

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) : 𝓢 ⊢! ◇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 𝓢] : 𝓢 ⊢ p ⟶ □◇p

Equations

• LO.System.axiomB = LO.System.HasAxiomB.B p

@[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 𝓢] : 𝓢 ⊢! p ⟶ □◇p

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 𝓢) : LO.System.HasAxiomB Γ

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 𝓢) : LO.System.HasAxiomB Γ

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 𝓢] : 𝓢 ⊢ □p ⟶ ◇p

Equations

• LO.System.axiomD = LO.System.HasAxiomD.D p

@[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 𝓢] : 𝓢 ⊢! □p ⟶ ◇p

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 𝓢) : LO.System.HasAxiomD Γ

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 𝓢) : LO.System.HasAxiomD Γ

Equations

• LO.System.instHasAxiomDContext Γ = { D := fun (x : F) => LO.System.Context.of LO.System.axiomD }

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 𝓢] : 𝓢 ⊢ □p ⟶ □□p

Equations

• LO.System.axiomFour = LO.System.HasAxiomFour.Four p

@[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 𝓢] : 𝓢 ⊢! □p ⟶ □□p

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 𝓢) : LO.System.HasAxiomFour Γ

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 𝓢) : LO.System.HasAxiomFour Γ

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) : 𝓢 ⊢ □□p

Equations

• LO.System.axiomFour' h = LO.System.axiomFour⨀h

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) : 𝓢 ⊢! □□p

Equations

• ⋯ = ⋯

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 𝓢] : 𝓢 ⊢ □⊡p ⟶ □p

Equations

• LO.System.imply_BoxBoxdot_Box = LO.System.impTrans'' LO.System.distribute_box_and LO.System.and₁

@[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 𝓢] : 𝓢 ⊢! □⊡p ⟶ □p

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 𝓢] : 𝓢 ⊢ □p ⟶ □⊡p

Equations

• LO.System.imply_Box_BoxBoxdot = LO.System.impTrans'' (LO.System.implyRightAnd (LO.System.impId (□p)) LO.System.axiomFour) LO.System.collect_box_and

@[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 𝓢] : 𝓢 ⊢! □p ⟶ □⊡p

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) : 𝓢 ⊢ □⊡p

Equations

• LO.System.imply_Box_BoxBoxdot' h = LO.System.imply_Box_BoxBoxdot⨀h

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) : 𝓢 ⊢! □⊡p

Equations

• ⋯ = ⋯

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 𝓢] : 𝓢 ⊢ □p ⟷ □⊡p

Equations

• LO.System.iff_Box_BoxBoxdot = LO.System.iffIntro LO.System.imply_Box_BoxBoxdot LO.System.imply_BoxBoxdot_Box

@[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 𝓢] : 𝓢 ⊢! □p ⟷ □⊡p

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 𝓢] : 𝓢 ⊢ □p ⟷ ⊡□p

Equations

• One or more equations did not get rendered due to their size.

@[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 𝓢] : 𝓢 ⊢! □p ⟷ ⊡□p

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 𝓢] : 𝓢 ⊢ ⊡p ⟷ ⊡⊡p

Equations

• One or more equations did not get rendered due to their size.

@[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 𝓢] : 𝓢 ⊢! ⊡p ⟷ ⊡⊡p

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 𝓢] : 𝓢 ⊢ ⊡p ⟶ ⊡⊡p

Equations

• LO.System.boxdotAxiomFour = LO.System.and₁' LO.System.iff_Boxdot_BoxdotBoxdot

@[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 𝓢] : 𝓢 ⊢! ⊡p ⟶ ⊡⊡p

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 𝓢] [LO.System.HasAxiomFour 𝓢] : 𝓢 ⊢ □p ⟷ ⊡p

Equations

• LO.System.iff_box_boxdot = LO.System.iffIntro (LO.System.implyRightAnd LO.System.axiomT (LO.System.impId (□p))) LO.System.and₂

@[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 𝓢] [LO.System.HasAxiomFour 𝓢] : 𝓢 ⊢! □p ⟷ ⊡p

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 𝓢] : 𝓢 ⊢ ◇p ⟷ ⟐p

Equations

• LO.System.iff_dia_diadot = LO.System.iffIntro LO.System.or₂ (LO.System.or₃'' LO.System.diaTc (LO.System.impId (◇p)))

@[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 𝓢] : 𝓢 ⊢! ◇p ⟷ ⟐p

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 𝓢] : 𝓢 ⊢ ◇p ⟶ □◇p

Equations

• LO.System.axiomFive = LO.System.HasAxiomFive.Five p

@[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 𝓢] : 𝓢 ⊢! ◇p ⟶ □◇p

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 𝓢) : LO.System.HasAxiomFive Γ

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 𝓢) : LO.System.HasAxiomFive Γ

Equations

• LO.System.instHasAxiomFiveContext Γ = { Five := fun (x : F) => LO.System.Context.of LO.System.axiomFive }

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 𝓢] : 𝓢 ⊢ p ⟶ □p

Equations

• LO.System.axiomTc = LO.System.HasAxiomTc.Tc p

@[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 𝓢] : 𝓢 ⊢! p ⟶ □p

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 𝓢) : LO.System.HasAxiomTc Γ

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 𝓢) : LO.System.HasAxiomTc Γ

Equations

• LO.System.instHasAxiomTcContext Γ = { Tc := fun (x : F) => LO.System.Context.of LO.System.axiomTc }

instance LO.System.instHasAxiomFourOfHasAxiomTc {F : Type u_1} [LO.BasicModalLogicalConnective F] {S : Type u_2} [LO.System F S] {𝓢 : S} [LO.System.HasAxiomTc 𝓢] : LO.System.HasAxiomFour 𝓢

Equations

• LO.System.instHasAxiomFourOfHasAxiomTc = { 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.HasDiaDuality 𝓢] [LO.System.HasAxiomTc 𝓢] : 𝓢 ⊢ ◇p ⟶ p

Equations

• LO.System.diaT = LO.System.impTrans'' (LO.System.and₁' LO.System.diaDuality) (LO.System.contra₂' LO.System.axiomTc)

@[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.HasDiaDuality 𝓢] [LO.System.HasAxiomTc 𝓢] : 𝓢 ⊢! ◇p ⟶ p

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.HasDiaDuality 𝓢] [LO.System.HasAxiomTc 𝓢] (h : 𝓢 ⊢ ◇p) : 𝓢 ⊢ p

Equations

• LO.System.diaT' h = LO.System.diaT⨀h

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.HasDiaDuality 𝓢] [LO.System.HasAxiomTc 𝓢] (h : 𝓢 ⊢! ◇p) : 𝓢 ⊢! p

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 𝓢] : 𝓢 ⊢ □p

Equations

• LO.System.axiomVer = LO.System.HasAxiomVer.Ver p

@[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 𝓢] : 𝓢 ⊢! □p

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 𝓢) : LO.System.HasAxiomVer Γ

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 𝓢) : LO.System.HasAxiomVer Γ

Equations

• LO.System.instHasAxiomVerContext Γ = { Ver := fun (x : F) => LO.System.Context.of LO.System.axiomVer }

instance LO.System.instHasAxiomTcOfHasAxiomVer {F : Type u_1} [LO.BasicModalLogicalConnective F] {S : Type u_2} [LO.System F S] {𝓢 : S} [LO.System.Classical 𝓢] [LO.System.HasAxiomVer 𝓢] : LO.System.HasAxiomTc 𝓢

Equations

• LO.System.instHasAxiomTcOfHasAxiomVer = { Tc := fun (x : F) => LO.System.axiomTc_of_Ver }

instance LO.System.instHasAxiomLOfHasAxiomVer {F : Type u_1} [LO.BasicModalLogicalConnective F] {S : Type u_2} [LO.System F S] {𝓢 : S} [LO.System.Classical 𝓢] [LO.System.HasAxiomVer 𝓢] : LO.System.HasAxiomL 𝓢

Equations

• LO.System.instHasAxiomLOfHasAxiomVer = { 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.NegationEquiv 𝓢] [LO.System.HasDiaDuality 𝓢] [LO.System.HasAxiomVer 𝓢] : 𝓢 ⊢ ◇p ⟶ ⊥

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)

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.NegationEquiv 𝓢] [LO.System.HasDiaDuality 𝓢] [LO.System.HasAxiomVer 𝓢] : 𝓢 ⊢! ◇p ⟶ ⊥

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.NegationEquiv 𝓢] [LO.System.HasDiaDuality 𝓢] [LO.System.HasAxiomVer 𝓢] (h : 𝓢 ⊢ ◇p) : 𝓢 ⊢ ⊥

Equations

• LO.System.bot_of_dia' h = LO.System.bot_of_dia⨀h

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.NegationEquiv 𝓢] [LO.System.HasDiaDuality 𝓢] [LO.System.HasAxiomVer 𝓢] (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 𝓢] : 𝓢 ⊢ □(□p ⟶ p) ⟶ □p

Equations

• LO.System.axiomL = LO.System.HasAxiomL.L p

@[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 𝓢] : 𝓢 ⊢! □(□p ⟶ p) ⟶ □p

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 𝓢) : LO.System.HasAxiomL Γ

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 𝓢) : LO.System.HasAxiomL Γ

Equations

• LO.System.instHasAxiomLContext Γ = { L := fun (x : F) => LO.System.Context.of LO.System.axiomL }

instance LO.System.instHasAxiomFourOfHasAxiomL {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 𝓢] : LO.System.HasAxiomFour 𝓢

Equations

• LO.System.instHasAxiomFourOfHasAxiomL = { 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.

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

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

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.axiomH {F : Type u_1} [LO.BasicModalLogicalConnective F] {S : Type u_2} [LO.System F S] {p : F} {𝓢 : S} [LO.System.HasAxiomH 𝓢] : 𝓢 ⊢ □(□p ⟷ p) ⟶ □p

Equations

• LO.System.axiomH = LO.System.HasAxiomH.H p

@[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 𝓢] : 𝓢 ⊢! □(□p ⟷ p) ⟶ □p

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 𝓢) : LO.System.HasAxiomH Γ

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 𝓢) : LO.System.HasAxiomH Γ

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} : 𝓢 ⊢ □p ⟶ p → 𝓢 ⊢ p

Alias of LO.System.LoebRule.loeb.

Equations

• @LO.System.loeb = @LO.System.LoebRule.loeb

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 𝓢] : 𝓢 ⊢! □p ⟶ p → 𝓢 ⊢! p

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} : 𝓢 ⊢ □p ⟷ p → 𝓢 ⊢ p

Alias of LO.System.HenkinRule.henkin.

Equations

• @LO.System.henkin = @LO.System.HenkinRule.henkin

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 𝓢] : 𝓢 ⊢! □p ⟷ p → 𝓢 ⊢! p

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 𝓢] : LO.System.HasAxiomL 𝓢

Equations

• LO.System.instHasAxiomLOfK4Loeb = { L := fun (x : F) => LO.System.axiomL_of_K4Loeb }

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 𝓢] : LO.System.LoebRule 𝓢

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 𝓢] : LO.System.HenkinRule 𝓢

Equations

• LO.System.instHenkinRuleOfHasAxiomFourOfHasAxiomH = { henkin := fun {p : F} (h : 𝓢 ⊢ □p ⟷ p) => LO.System.and₁' h⨀(LO.System.axiomH⨀LO.System.nec h) }

instance LO.System.instHasAxiomHOfHasAxiomL {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 𝓢] : LO.System.HasAxiomH 𝓢

Equations

• LO.System.instHasAxiomHOfHasAxiomL = { H := fun (x : F) => LO.System.axiomH_of_GL }

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} : 𝓢 ⊢ □p → 𝓢 ⊢ p

Alias of LO.System.Unnecessitation.unnec.

Equations

• @LO.System.unnec = @LO.System.Unnecessitation.unnec

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 𝓢] : 𝓢 ⊢! □p → 𝓢 ⊢! p

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 : ℕ} : 𝓢 ⊢ □^[n]p → 𝓢 ⊢ p

Equations

• One or more equations did not get rendered due to their size.

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 : ℕ} : 𝓢 ⊢! □^[n]p → 𝓢 ⊢! p

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 𝓢] : LO.System.Unnecessitation 𝓢

Equations

• LO.System.instUnnecessitationOfHasAxiomT = { unnec := fun {p : F} (hp : 𝓢 ⊢ □p) => LO.System.axiomT⨀hp }

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) : 𝓢 ⊢ ⊡p ⟶ ⊡q

Equations

• One or more equations did not get rendered due to their size.

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) : 𝓢 ⊢! ⊡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) : 𝓢 ⊢ ⊡p ⟶ □q ⟶ q

Equations

• One or more equations did not get rendered due to their size.

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) : 𝓢 ⊢! ⊡p ⟶ □q ⟶ 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) : 𝓢 ⊢ □p ⟶ □q

Equations

• One or more equations did not get rendered due to their size.

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) : 𝓢 ⊢! □p ⟶ □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) : 𝓢 ⊢! □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 𝓢] : 𝓢 ⊢ □(□(p ⟶ □p) ⟶ p) ⟶ p

Equations

• LO.System.axiomGrz = LO.System.HasAxiomGrz.Grz p

@[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 𝓢] : 𝓢 ⊢! □(□(p ⟶ □p) ⟶ p) ⟶ p

def LO.System.dhyp_imp {F : Type u_1} [LO.BasicModalLogicalConnective F] {S : Type u_2} [LO.System F S] {p : F} {q : F} {r : F} {𝓢 : S} [LO.System.Classical 𝓢] (h : 𝓢 ⊢ p ⟶ q) : 𝓢 ⊢ (r ⟶ p) ⟶ r ⟶ q

Equations

• LO.System.dhyp_imp h = LO.System.imply₂⨀LO.System.dhyp r h

def LO.System.ppq {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 ⟶ p ⟶ q) : 𝓢 ⊢ p ⟶ q

Equations

• LO.System.ppq h = LO.System.FiniteContext.deduct' (let_fun this := LO.System.FiniteContext.of h; this⨀LO.System.FiniteContext.byAxm ⋯⨀LO.System.FiniteContext.byAxm ⋯)

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 𝓢] : 𝓢 ⊢ □p ⟶ □(□(p ⋏ (□p ⟶ □□p) ⟶ □(p ⋏ (□p ⟶ □□p))) ⟶ p ⋏ (□p ⟶ □□p))

Equations

• One or more equations did not get rendered due to their size.

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 𝓢] : 𝓢 ⊢! □p ⟶ □(□(p ⋏ (□p ⟶ □□p) ⟶ □(p ⋏ (□p ⟶ □□p))) ⟶ p ⋏ (□p ⟶ □□p))

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 𝓢] : 𝓢 ⊢ □p ⟶ p ⋏ (□p ⟶ □□p)

Equations

• LO.System.lemma_Grz₂ = LO.System.impTrans'' LO.System.lemma_Grz₁ LO.System.axiomGrz

noncomputable instance LO.System.instHasAxiomFour {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 𝓢] : LO.System.HasAxiomFour 𝓢

Equations

• LO.System.instHasAxiomFour = { 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 𝓢] : LO.System.HasAxiomT 𝓢

Equations

• LO.System.instHasAxiomT = { T := fun (x : F) => LO.System.T_of_Grz }

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 𝓢] : 𝓢 ⊢ ⊡(⊡(p ⟶ ⊡p) ⟶ p) ⟶ p

Equations

• One or more equations did not get rendered due to their size.

@[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 𝓢] : 𝓢 ⊢! ⊡(⊡(p ⟶ ⊡p) ⟶ p) ⟶ p

class LO.System.ModalDisjunctive {F : Type u_1} [LO.LogicalConnective F] [LO.Box F] {S : Type u_2} [LO.System F S] (𝓢 : S) : Prop

• modal_disjunctive : ∀ {p q : F}, 𝓢 ⊢! □p ⋎ □q → 𝓢 ⊢! p ∨ 𝓢 ⊢! q

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} : 𝓢 ⊢! □p ⋎ □q → 𝓢 ⊢! p ∨ 𝓢 ⊢! q

theorem LO.System.Context.provable_iff_boxed {F : Type u_1} [LO.LogicalConnective F] [LO.Box F] {S : Type u_2} [LO.System F S] [DecidableEq F] {𝓢 : S} [LO.System.Minimal 𝓢] {X : Set F} {p : F} : (□''X) *⊢[𝓢]! p ↔ ∃ (Δ : List F), (∀ q ∈ □'Δ, q ∈ □''X) ∧ (□'Δ) ⊢[𝓢]! p