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 : {φ : F} → 𝓢 ⊢ φ → 𝓢 ⊢ □φ

def LO.System.nec {S : Type u_1} {F : Type u_2} {inst✝ : LO.BasicModalLogicalConnective F} {inst✝¹ : LO.System F S} {𝓢 : S} [self : LO.System.Necessitation 𝓢] {φ : F} : 𝓢 ⊢ φ → 𝓢 ⊢ □φ

Alias of LO.System.Necessitation.nec.

Equations

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

theorem LO.System.nec! {S : Type u_1} {F : Type u_2} [LO.BasicModalLogicalConnective F] [LO.System F S] {𝓢 : S} [LO.System.Necessitation 𝓢] {φ : F} : 𝓢 ⊢! φ → 𝓢 ⊢! □φ

def LO.System.multinec {S : Type u_1} {F : Type u_2} [LO.BasicModalLogicalConnective F] [LO.System F S] {𝓢 : S} [LO.System.Necessitation 𝓢] {φ : F} {n : ℕ} : 𝓢 ⊢ φ → 𝓢 ⊢ □^[n]φ

Equations

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

theorem LO.System.multinec! {S : Type u_1} {F : Type u_2} [LO.BasicModalLogicalConnective F] [LO.System F S] {𝓢 : S} [LO.System.Necessitation 𝓢] {φ : F} {n : ℕ} : 𝓢 ⊢! φ → 𝓢 ⊢! □^[n]φ

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 : {φ : F} → 𝓢 ⊢ □φ → 𝓢 ⊢ φ

def LO.System.unnec {S : Type u_1} {F : Type u_2} {inst✝ : LO.BasicModalLogicalConnective F} {inst✝¹ : LO.System F S} {𝓢 : S} [self : LO.System.Unnecessitation 𝓢] {φ : F} : 𝓢 ⊢ □φ → 𝓢 ⊢ φ

Alias of LO.System.Unnecessitation.unnec.

Equations

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

theorem LO.System.unnec! {S : Type u_1} {F : Type u_2} [LO.BasicModalLogicalConnective F] [LO.System F S] {𝓢 : S} [LO.System.Unnecessitation 𝓢] {φ : F} : 𝓢 ⊢! □φ → 𝓢 ⊢! φ

def LO.System.multiunnec {S : Type u_1} {F : Type u_2} [LO.BasicModalLogicalConnective F] [LO.System F S] {𝓢 : S} [LO.System.Unnecessitation 𝓢] {n : ℕ} {φ : F} : 𝓢 ⊢ □^[n]φ → 𝓢 ⊢ φ

Equations

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

theorem LO.System.multiunnec! {S : Type u_1} {F : Type u_2} [LO.BasicModalLogicalConnective F] [LO.System F S] {𝓢 : S} [LO.System.Unnecessitation 𝓢] {n : ℕ} {φ : F} : 𝓢 ⊢! □^[n]φ → 𝓢 ⊢! φ

class LO.System.LoebRule {S : Type u_1} {F : Type u_2} [LO.BasicModalLogicalConnective F] [LO.System F S] [LO.LogicalConnective F] (𝓢 : S) : Type (max u_2 u_3)

• loeb : {φ : F} → 𝓢 ⊢ □φ ➝ φ → 𝓢 ⊢ φ

def LO.System.loeb {S : Type u_1} {F : Type u_2} {inst✝ : LO.BasicModalLogicalConnective F} {inst✝¹ : LO.System F S} {inst✝² : LO.LogicalConnective F} {𝓢 : S} [self : LO.System.LoebRule 𝓢] {φ : F} : 𝓢 ⊢ □φ ➝ φ → 𝓢 ⊢ φ

Alias of LO.System.LoebRule.loeb.

Equations

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

theorem LO.System.loeb! {S : Type u_1} {F : Type u_2} [LO.BasicModalLogicalConnective F] [LO.System F S] {𝓢 : S} [LO.System.LoebRule 𝓢] {φ : F} : 𝓢 ⊢! □φ ➝ φ → 𝓢 ⊢! φ

class LO.System.HenkinRule {S : Type u_1} {F : Type u_2} [LO.BasicModalLogicalConnective F] [LO.System F S] [LO.LogicalConnective F] (𝓢 : S) : Type (max u_2 u_3)

• henkin : {φ : F} → 𝓢 ⊢ □φ ⭤ φ → 𝓢 ⊢ φ

def LO.System.henkin {S : Type u_1} {F : Type u_2} {inst✝ : LO.BasicModalLogicalConnective F} {inst✝¹ : LO.System F S} {inst✝² : LO.LogicalConnective F} {𝓢 : S} [self : LO.System.HenkinRule 𝓢] {φ : F} : 𝓢 ⊢ □φ ⭤ φ → 𝓢 ⊢ φ

Alias of LO.System.HenkinRule.henkin.

Equations

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

theorem LO.System.henkin! {S : Type u_1} {F : Type u_2} [LO.BasicModalLogicalConnective F] [LO.System F S] {𝓢 : S} [LO.System.HenkinRule 𝓢] {φ : F} : 𝓢 ⊢! □φ ⭤ φ → 𝓢 ⊢! φ

class LO.System.HasDiaDuality {S : Type u_1} {F : Type u_2} [LO.BasicModalLogicalConnective F] [LO.System F S] (𝓢 : S) : Type (max u_2 u_3)

• dia_dual : (φ : F) → 𝓢 ⊢ LO.Axioms.DiaDuality φ

def LO.System.diaDuality {S : Type u_1} {F : Type u_2} [LO.BasicModalLogicalConnective F] [LO.System F S] {𝓢 : S} [LO.System.HasDiaDuality 𝓢] {φ : F} : 𝓢 ⊢ ◇φ ⭤ ∼□(∼φ)

Equations

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

@[simp]

theorem LO.System.dia_duality! {S : Type u_1} {F : Type u_2} [LO.BasicModalLogicalConnective F] [LO.System F S] {𝓢 : S} [LO.System.HasDiaDuality 𝓢] {φ : F} : 𝓢 ⊢! ◇φ ⭤ ∼□(∼φ)

class LO.System.HasAxiomK {S : Type u_1} {F : Type u_2} [LO.BasicModalLogicalConnective F] [LO.System F S] [LO.LogicalConnective F] [LO.Box F] (𝓢 : S) : Type (max u_2 u_3)

• K : (φ ψ : F) → 𝓢 ⊢ LO.Axioms.K φ ψ

def LO.System.axiomK {S : Type u_1} {F : Type u_2} [LO.BasicModalLogicalConnective F] [LO.System F S] {𝓢 : S} [LO.System.HasAxiomK 𝓢] {φ ψ : F} : 𝓢 ⊢ □(φ ➝ ψ) ➝ □φ ➝ □ψ

Equations

• LO.System.axiomK = LO.System.HasAxiomK.K φ ψ

@[simp]

theorem LO.System.axiomK! {S : Type u_1} {F : Type u_2} [LO.BasicModalLogicalConnective F] [LO.System F S] {𝓢 : S} [LO.System.HasAxiomK 𝓢] {φ ψ : F} : 𝓢 ⊢! □(φ ➝ ψ) ➝ □φ ➝ □ψ

instance LO.System.instHasAxiomKFiniteContext {S : Type u_1} {F : Type u_2} [LO.BasicModalLogicalConnective F] [LO.System F S] {𝓢 : S} [LO.System.HasAxiomK 𝓢] [LO.System.Minimal 𝓢] (Γ : 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 {S : Type u_1} {F : Type u_2} [LO.BasicModalLogicalConnective F] [LO.System F S] {𝓢 : S} [LO.System.HasAxiomK 𝓢] [LO.System.Minimal 𝓢] (Γ : 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' {S : Type u_1} {F : Type u_2} [LO.BasicModalLogicalConnective F] [LO.System F S] {𝓢 : S} [LO.System.HasAxiomK 𝓢] [LO.System.Minimal 𝓢] {φ ψ : F} (h : 𝓢 ⊢ □(φ ➝ ψ)) : 𝓢 ⊢ □φ ➝ □ψ

Equations

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

@[simp]

theorem LO.System.axiomK'! {S : Type u_1} {F : Type u_2} [LO.BasicModalLogicalConnective F] [LO.System F S] {𝓢 : S} [LO.System.HasAxiomK 𝓢] [LO.System.Minimal 𝓢] {φ ψ : F} (h : 𝓢 ⊢! □(φ ➝ ψ)) : 𝓢 ⊢! □φ ➝ □ψ

def LO.System.axiomK'' {S : Type u_1} {F : Type u_2} [LO.BasicModalLogicalConnective F] [LO.System F S] {𝓢 : S} [LO.System.HasAxiomK 𝓢] [LO.System.Minimal 𝓢] {φ ψ : F} (h₁ : 𝓢 ⊢ □(φ ➝ ψ)) (h₂ : 𝓢 ⊢ □φ) : 𝓢 ⊢ □ψ

Equations

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

@[simp]

theorem LO.System.axiomK''! {S : Type u_1} {F : Type u_2} [LO.BasicModalLogicalConnective F] [LO.System F S] {𝓢 : S} [LO.System.HasAxiomK 𝓢] [LO.System.Minimal 𝓢] {φ ψ : F} (h₁ : 𝓢 ⊢! □(φ ➝ ψ)) (h₂ : 𝓢 ⊢! □φ) : 𝓢 ⊢! □ψ

class LO.System.HasAxiomT {S : Type u_1} {F : Type u_2} [LO.BasicModalLogicalConnective F] [LO.System F S] (𝓢 : S) : Type (max u_2 u_3)

• T : (φ : F) → 𝓢 ⊢ LO.Axioms.T φ

def LO.System.axiomT {S : Type u_1} {F : Type u_2} [LO.BasicModalLogicalConnective F] [LO.System F S] {𝓢 : S} [LO.System.HasAxiomT 𝓢] {φ : F} : 𝓢 ⊢ □φ ➝ φ

Equations

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

@[simp]

theorem LO.System.axiomT! {S : Type u_1} {F : Type u_2} [LO.BasicModalLogicalConnective F] [LO.System F S] {𝓢 : S} [LO.System.HasAxiomT 𝓢] {φ : F} : 𝓢 ⊢! □φ ➝ φ

instance LO.System.instHasAxiomTFiniteContext {S : Type u_1} {F : Type u_2} [LO.BasicModalLogicalConnective F] [LO.System F S] {𝓢 : S} [LO.System.HasAxiomT 𝓢] [LO.System.Minimal 𝓢] (Γ : 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 {S : Type u_1} {F : Type u_2} [LO.BasicModalLogicalConnective F] [LO.System F S] {𝓢 : S} [LO.System.HasAxiomT 𝓢] [LO.System.Minimal 𝓢] (Γ : 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' {S : Type u_1} {F : Type u_2} [LO.BasicModalLogicalConnective F] [LO.System F S] {𝓢 : S} [LO.System.HasAxiomT 𝓢] [LO.System.Minimal 𝓢] {φ : F} (h : 𝓢 ⊢ □φ) : 𝓢 ⊢ φ

Equations

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

@[simp]

theorem LO.System.axiomT'! {S : Type u_1} {F : Type u_2} [LO.BasicModalLogicalConnective F] [LO.System F S] {𝓢 : S} [LO.System.HasAxiomT 𝓢] [LO.System.Minimal 𝓢] {φ : F} (h : 𝓢 ⊢! □φ) : 𝓢 ⊢! φ

class LO.System.HasAxiomD {S : Type u_1} {F : Type u_2} [LO.BasicModalLogicalConnective F] [LO.System F S] [LO.Dia F] (𝓢 : S) : Type (max u_2 u_3)

• D : (φ : F) → 𝓢 ⊢ LO.Axioms.D φ

def LO.System.axiomD {S : Type u_1} {F : Type u_2} [LO.BasicModalLogicalConnective F] [LO.System F S] {𝓢 : S} [LO.Dia F] [LO.System.HasAxiomD 𝓢] {φ : F} : 𝓢 ⊢ □φ ➝ ◇φ

Equations

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

@[simp]

theorem LO.System.axiomD! {S : Type u_1} {F : Type u_2} [LO.BasicModalLogicalConnective F] [LO.System F S] {𝓢 : S} [LO.Dia F] [LO.System.HasAxiomD 𝓢] {φ : F} : 𝓢 ⊢! □φ ➝ ◇φ

instance LO.System.instHasAxiomDFiniteContext {S : Type u_1} {F : Type u_2} [LO.BasicModalLogicalConnective F] [LO.System F S] {𝓢 : S} [LO.Dia F] [LO.System.HasAxiomD 𝓢] [LO.System.Minimal 𝓢] (Γ : 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 {S : Type u_1} {F : Type u_2} [LO.BasicModalLogicalConnective F] [LO.System F S] {𝓢 : S} [LO.Dia F] [LO.System.HasAxiomD 𝓢] [LO.System.Minimal 𝓢] (Γ : 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.axiomD' {S : Type u_1} {F : Type u_2} [LO.BasicModalLogicalConnective F] [LO.System F S] {𝓢 : S} [LO.Dia F] [LO.System.HasAxiomD 𝓢] [LO.System.Minimal 𝓢] {φ : F} (h : 𝓢 ⊢ □φ) : 𝓢 ⊢ ◇φ

Equations

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

theorem LO.System.axiomD'! {S : Type u_1} {F : Type u_2} [LO.BasicModalLogicalConnective F] [LO.System F S] {𝓢 : S} [LO.Dia F] [LO.System.HasAxiomD 𝓢] [LO.System.Minimal 𝓢] {φ : F} (h : 𝓢 ⊢! □φ) : 𝓢 ⊢! ◇φ

class LO.System.HasAxiomP {S : Type u_1} {F : Type u_2} [LO.BasicModalLogicalConnective F] [LO.System F S] (𝓢 : S) : Type u_3

• P : 𝓢 ⊢ LO.Axioms.P

def LO.System.axiomP {S : Type u_1} {F : Type u_2} [LO.BasicModalLogicalConnective F] [LO.System F S] {𝓢 : S} [LO.System.HasAxiomP 𝓢] : 𝓢 ⊢ ∼□⊥

Equations

• LO.System.axiomP = LO.System.HasAxiomP.P

@[simp]

theorem LO.System.axiomP! {S : Type u_1} {F : Type u_2} [LO.BasicModalLogicalConnective F] [LO.System F S] {𝓢 : S} [LO.System.HasAxiomP 𝓢] : 𝓢 ⊢! ∼□⊥

instance LO.System.instHasAxiomPFiniteContext {S : Type u_1} {F : Type u_2} [LO.BasicModalLogicalConnective F] [LO.System F S] {𝓢 : S} [LO.System.HasAxiomP 𝓢] [LO.System.Minimal 𝓢] (Γ : LO.System.FiniteContext F 𝓢) : LO.System.HasAxiomP Γ

Equations

• LO.System.instHasAxiomPFiniteContext Γ = { P := LO.System.FiniteContext.of LO.System.axiomP }

instance LO.System.instHasAxiomPContext {S : Type u_1} {F : Type u_2} [LO.BasicModalLogicalConnective F] [LO.System F S] {𝓢 : S} [LO.System.HasAxiomP 𝓢] [LO.System.Minimal 𝓢] (Γ : LO.System.Context F 𝓢) : LO.System.HasAxiomP Γ

Equations

• LO.System.instHasAxiomPContext Γ = { P := LO.System.Context.of LO.System.axiomP }

class LO.System.HasAxiomB {S : Type u_1} {F : Type u_2} [LO.BasicModalLogicalConnective F] [LO.System F S] [LO.Dia F] (𝓢 : S) : Type (max u_2 u_3)

• B : (φ : F) → 𝓢 ⊢ LO.Axioms.B φ

def LO.System.axiomB {S : Type u_1} {F : Type u_2} [LO.BasicModalLogicalConnective F] [LO.System F S] {𝓢 : S} [LO.Dia F] [LO.System.HasAxiomB 𝓢] {φ : F} : 𝓢 ⊢ φ ➝ □◇φ

Equations

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

@[simp]

theorem LO.System.axiomB! {S : Type u_1} {F : Type u_2} [LO.BasicModalLogicalConnective F] [LO.System F S] {𝓢 : S} [LO.Dia F] [LO.System.HasAxiomB 𝓢] {φ : F} : 𝓢 ⊢! φ ➝ □◇φ

instance LO.System.instHasAxiomBFiniteContext {S : Type u_1} {F : Type u_2} [LO.BasicModalLogicalConnective F] [LO.System F S] {𝓢 : S} [LO.Dia F] [LO.System.HasAxiomB 𝓢] [LO.System.Minimal 𝓢] (Γ : 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 {S : Type u_1} {F : Type u_2} [LO.BasicModalLogicalConnective F] [LO.System F S] {𝓢 : S} [LO.Dia F] [LO.System.HasAxiomB 𝓢] [LO.System.Minimal 𝓢] (Γ : 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.axiomB' {S : Type u_1} {F : Type u_2} [LO.BasicModalLogicalConnective F] [LO.System F S] {𝓢 : S} [LO.Dia F] [LO.System.HasAxiomB 𝓢] [LO.System.Minimal 𝓢] {φ : F} (h : 𝓢 ⊢ φ) : 𝓢 ⊢ □◇φ

Equations

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

@[simp]

theorem LO.System.axiomB'! {S : Type u_1} {F : Type u_2} [LO.BasicModalLogicalConnective F] [LO.System F S] {𝓢 : S} [LO.Dia F] [LO.System.HasAxiomB 𝓢] [LO.System.Minimal 𝓢] {φ : F} (h : 𝓢 ⊢! φ) : 𝓢 ⊢! □◇φ

class LO.System.HasAxiomFour {S : Type u_1} {F : Type u_2} [LO.BasicModalLogicalConnective F] [LO.System F S] (𝓢 : S) : Type (max u_2 u_3)

• Four : (φ : F) → 𝓢 ⊢ LO.Axioms.Four φ

def LO.System.axiomFour {S : Type u_1} {F : Type u_2} [LO.BasicModalLogicalConnective F] [LO.System F S] {𝓢 : S} [LO.System.HasAxiomFour 𝓢] {φ : F} : 𝓢 ⊢ □φ ➝ □□φ

Equations

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

@[simp]

theorem LO.System.axiomFour! {S : Type u_1} {F : Type u_2} [LO.BasicModalLogicalConnective F] [LO.System F S] {𝓢 : S} [LO.System.HasAxiomFour 𝓢] {φ : F} : 𝓢 ⊢! □φ ➝ □□φ

instance LO.System.instHasAxiomFourFiniteContext {S : Type u_1} {F : Type u_2} [LO.BasicModalLogicalConnective F] [LO.System F S] {𝓢 : S} [LO.System.HasAxiomFour 𝓢] [LO.System.Minimal 𝓢] (Γ : 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 {S : Type u_1} {F : Type u_2} [LO.BasicModalLogicalConnective F] [LO.System F S] {𝓢 : S} [LO.System.HasAxiomFour 𝓢] [LO.System.Minimal 𝓢] (Γ : 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' {S : Type u_1} {F : Type u_2} [LO.BasicModalLogicalConnective F] [LO.System F S] {𝓢 : S} [LO.System.HasAxiomFour 𝓢] [LO.System.Minimal 𝓢] {φ : F} (h : 𝓢 ⊢ □φ) : 𝓢 ⊢ □□φ

Equations

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

def LO.System.axiomFour'! {S : Type u_1} {F : Type u_2} [LO.BasicModalLogicalConnective F] [LO.System F S] {𝓢 : S} [LO.System.HasAxiomFour 𝓢] [LO.System.Minimal 𝓢] {φ : F} (h : 𝓢 ⊢! □φ) : 𝓢 ⊢! □□φ

Equations

• ⋯ = ⋯

class LO.System.HasAxiomFive {S : Type u_1} {F : Type u_2} [LO.BasicModalLogicalConnective F] [LO.System F S] [LO.Dia F] (𝓢 : S) : Type (max u_2 u_3)

• Five : (φ : F) → 𝓢 ⊢ LO.Axioms.Five φ

def LO.System.axiomFive {S : Type u_1} {F : Type u_2} [LO.BasicModalLogicalConnective F] [LO.System F S] {𝓢 : S} [LO.Dia F] [LO.System.HasAxiomFive 𝓢] {φ : F} : 𝓢 ⊢ ◇φ ➝ □◇φ

Equations

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

@[simp]

theorem LO.System.axiomFive! {S : Type u_1} {F : Type u_2} [LO.BasicModalLogicalConnective F] [LO.System F S] {𝓢 : S} [LO.Dia F] [LO.System.HasAxiomFive 𝓢] {φ : F} : 𝓢 ⊢! ◇φ ➝ □◇φ

instance LO.System.instHasAxiomFiveFiniteContext {S : Type u_1} {F : Type u_2} [LO.BasicModalLogicalConnective F] [LO.System F S] {𝓢 : S} [LO.Dia F] [LO.System.HasAxiomFive 𝓢] [LO.System.Minimal 𝓢] (Γ : 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 {S : Type u_1} {F : Type u_2} [LO.BasicModalLogicalConnective F] [LO.System F S] {𝓢 : S} [LO.Dia F] [LO.System.HasAxiomFive 𝓢] [LO.System.Minimal 𝓢] (Γ : LO.System.Context F 𝓢) : LO.System.HasAxiomFive Γ

Equations

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

class LO.System.HasAxiomL {S : Type u_1} {F : Type u_2} [LO.BasicModalLogicalConnective F] [LO.System F S] (𝓢 : S) : Type (max u_2 u_3)

• L : (φ : F) → 𝓢 ⊢ LO.Axioms.L φ

def LO.System.axiomL {S : Type u_1} {F : Type u_2} [LO.BasicModalLogicalConnective F] [LO.System F S] {𝓢 : S} [LO.System.HasAxiomL 𝓢] {φ : F} : 𝓢 ⊢ □(□φ ➝ φ) ➝ □φ

Equations

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

@[simp]

theorem LO.System.axiomL! {S : Type u_1} {F : Type u_2} [LO.BasicModalLogicalConnective F] [LO.System F S] {𝓢 : S} [LO.System.HasAxiomL 𝓢] {φ : F} : 𝓢 ⊢! □(□φ ➝ φ) ➝ □φ

instance LO.System.instHasAxiomLFiniteContext {S : Type u_1} {F : Type u_2} [LO.BasicModalLogicalConnective F] [LO.System F S] {𝓢 : S} [LO.System.HasAxiomL 𝓢] [LO.System.Minimal 𝓢] (Γ : 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 {S : Type u_1} {F : Type u_2} [LO.BasicModalLogicalConnective F] [LO.System F S] {𝓢 : S} [LO.System.HasAxiomL 𝓢] [LO.System.Minimal 𝓢] (Γ : LO.System.Context F 𝓢) : LO.System.HasAxiomL Γ

Equations

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

class LO.System.HasAxiomDot2 {S : Type u_1} {F : Type u_2} [LO.BasicModalLogicalConnective F] [LO.System F S] [LO.Dia F] (𝓢 : S) : Type (max u_2 u_3)

• Dot2 : (φ : F) → 𝓢 ⊢ LO.Axioms.Dot2 φ

class LO.System.HasAxiomDot3 {S : Type u_1} {F : Type u_2} [LO.BasicModalLogicalConnective F] [LO.System F S] (𝓢 : S) : Type (max u_2 u_3)

• Dot3 : (φ ψ : F) → 𝓢 ⊢ LO.Axioms.Dot3 φ ψ

class LO.System.HasAxiomGrz {S : Type u_1} {F : Type u_2} [LO.BasicModalLogicalConnective F] [LO.System F S] (𝓢 : S) : Type (max u_2 u_3)

• Grz : (φ : F) → 𝓢 ⊢ LO.Axioms.Grz φ

def LO.System.axiomGrz {S : Type u_1} {F : Type u_2} [LO.BasicModalLogicalConnective F] [LO.System F S] {𝓢 : S} [LO.System.HasAxiomGrz 𝓢] {φ : F} : 𝓢 ⊢ □(□(φ ➝ □φ) ➝ φ) ➝ φ

Equations

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

@[simp]

theorem LO.System.axiomGrz! {S : Type u_1} {F : Type u_2} [LO.BasicModalLogicalConnective F] [LO.System F S] {𝓢 : S} [LO.System.HasAxiomGrz 𝓢] {φ : F} : 𝓢 ⊢! □(□(φ ➝ □φ) ➝ φ) ➝ φ

instance LO.System.instHasAxiomGrzFiniteContext {S : Type u_1} {F : Type u_2} [LO.BasicModalLogicalConnective F] [LO.System F S] {𝓢 : S} [LO.System.HasAxiomGrz 𝓢] [LO.System.Minimal 𝓢] (Γ : LO.System.FiniteContext F 𝓢) : LO.System.HasAxiomGrz Γ

Equations

• LO.System.instHasAxiomGrzFiniteContext Γ = { Grz := fun (x : F) => LO.System.FiniteContext.of LO.System.axiomGrz }

instance LO.System.instHasAxiomGrzContext {S : Type u_1} {F : Type u_2} [LO.BasicModalLogicalConnective F] [LO.System F S] {𝓢 : S} [LO.System.HasAxiomGrz 𝓢] [LO.System.Minimal 𝓢] (Γ : LO.System.Context F 𝓢) : LO.System.HasAxiomGrz Γ

Equations

• LO.System.instHasAxiomGrzContext Γ = { Grz := fun (x : F) => LO.System.Context.of LO.System.axiomGrz }

class LO.System.HasAxiomTc {S : Type u_1} {F : Type u_2} [LO.BasicModalLogicalConnective F] [LO.System F S] (𝓢 : S) : Type (max u_2 u_3)

• Tc : (φ : F) → 𝓢 ⊢ LO.Axioms.Tc φ

def LO.System.axiomTc {S : Type u_1} {F : Type u_2} [LO.BasicModalLogicalConnective F] [LO.System F S] {𝓢 : S} [LO.System.HasAxiomTc 𝓢] {φ : F} : 𝓢 ⊢ φ ➝ □φ

Equations

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

@[simp]

theorem LO.System.axiomTc! {S : Type u_1} {F : Type u_2} [LO.BasicModalLogicalConnective F] [LO.System F S] {𝓢 : S} [LO.System.HasAxiomTc 𝓢] {φ : F} : 𝓢 ⊢! φ ➝ □φ

instance LO.System.instHasAxiomTcFiniteContext {S : Type u_1} {F : Type u_2} [LO.BasicModalLogicalConnective F] [LO.System F S] {𝓢 : S} [LO.System.HasAxiomTc 𝓢] [LO.System.Minimal 𝓢] (Γ : 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 {S : Type u_1} {F : Type u_2} [LO.BasicModalLogicalConnective F] [LO.System F S] {𝓢 : S} [LO.System.HasAxiomTc 𝓢] [LO.System.Minimal 𝓢] (Γ : LO.System.Context F 𝓢) : LO.System.HasAxiomTc Γ

Equations

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

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 : (φ : F) → 𝓢 ⊢ LO.Axioms.Ver φ

def LO.System.axiomVer {S : Type u_1} {F : Type u_2} [LO.BasicModalLogicalConnective F] [LO.System F S] {𝓢 : S} [LO.System.HasAxiomVer 𝓢] {φ : F} : 𝓢 ⊢ □φ

Equations

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

@[simp]

theorem LO.System.axiomVer! {S : Type u_1} {F : Type u_2} [LO.BasicModalLogicalConnective F] [LO.System F S] {𝓢 : S} [LO.System.HasAxiomVer 𝓢] {φ : F} : 𝓢 ⊢! □φ

instance LO.System.instHasAxiomVerFiniteContext {S : Type u_1} {F : Type u_2} [LO.BasicModalLogicalConnective F] [LO.System F S] {𝓢 : S} [LO.System.HasAxiomVer 𝓢] [LO.System.Minimal 𝓢] (Γ : 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 {S : Type u_1} {F : Type u_2} [LO.BasicModalLogicalConnective F] [LO.System F S] {𝓢 : S} [LO.System.HasAxiomVer 𝓢] [LO.System.Minimal 𝓢] (Γ : LO.System.Context F 𝓢) : LO.System.HasAxiomVer Γ

Equations

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

class LO.System.HasAxiomH {S : Type u_1} {F : Type u_2} [LO.BasicModalLogicalConnective F] [LO.System F S] (𝓢 : S) : Type (max u_2 u_3)

• H : (φ : F) → 𝓢 ⊢ LO.Axioms.H φ

def LO.System.axiomH {S : Type u_1} {F : Type u_2} [LO.BasicModalLogicalConnective F] [LO.System F S] {𝓢 : S} [LO.System.HasAxiomH 𝓢] {φ : F} : 𝓢 ⊢ □(□φ ⭤ φ) ➝ □φ

Equations

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

@[simp]

theorem LO.System.axiomH! {S : Type u_1} {F : Type u_2} [LO.BasicModalLogicalConnective F] [LO.System F S] {𝓢 : S} [LO.System.HasAxiomH 𝓢] {φ : F} : 𝓢 ⊢! □(□φ ⭤ φ) ➝ □φ

instance LO.System.instHasAxiomHFiniteContext {S : Type u_1} {F : Type u_2} [LO.BasicModalLogicalConnective F] [LO.System F S] {𝓢 : S} [LO.System.HasAxiomH 𝓢] [LO.System.Minimal 𝓢] (Γ : 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 {S : Type u_1} {F : Type u_2} [LO.BasicModalLogicalConnective F] [LO.System F S] {𝓢 : S} [LO.System.HasAxiomH 𝓢] [LO.System.Minimal 𝓢] (Γ : LO.System.Context F 𝓢) : LO.System.HasAxiomH Γ

Equations

• LO.System.instHasAxiomHContext Γ = { H := fun (x : F) => LO.System.Context.of LO.System.axiomH }

instance LO.System.instHasDiaDualityOfMinimalOfModalDeMorganOfHasAxiomDNE {S : Type u_1} {F : Type u_2} [LO.System F S] [LO.BasicModalLogicalConnective F] {𝓢 : S} [LO.System.Minimal 𝓢] [LO.ModalDeMorgan F] [LO.System.HasAxiomDNE 𝓢] : LO.System.HasDiaDuality 𝓢

Equations

• LO.System.instHasDiaDualityOfMinimalOfModalDeMorganOfHasAxiomDNE = { dia_dual := fun (φ : F) => ⋯.mpr (LO.System.iffId (◇φ)) }

instance LO.System.instHasDiaDualityOfMinimalOfDiaAbbrev {S : Type u_1} {F : Type u_2} [LO.System F S] [LO.BasicModalLogicalConnective F] {𝓢 : S} [LO.System.Minimal 𝓢] [LO.DiaAbbrev F] : LO.System.HasDiaDuality 𝓢

Equations

• LO.System.instHasDiaDualityOfMinimalOfDiaAbbrev = { dia_dual := fun (φ : F) => ⋯.mpr (LO.System.iffId (∼□(∼φ))) }

instance LO.System.instUnnecessitationOfModusPonensOfHasAxiomT {S : Type u_1} {F : Type u_2} [LO.System F S] [LO.BasicModalLogicalConnective F] {𝓢 : S} [LO.System.ModusPonens 𝓢] [LO.System.HasAxiomT 𝓢] : LO.System.Unnecessitation 𝓢

Equations

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

class LO.System.K {S : Type u_1} {F : Type u_2} [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)

• mdp : {φ ψ : F} → 𝓢 ⊢ φ ➝ ψ → 𝓢 ⊢ φ → 𝓢 ⊢ ψ
• neg_equiv : (φ : F) → 𝓢 ⊢ LO.Axioms.NegEquiv φ
• verum : 𝓢 ⊢ LO.Axioms.Verum
• imply₁ : (φ ψ : F) → 𝓢 ⊢ LO.Axioms.Imply₁ φ ψ
• imply₂ : (φ ψ χ : F) → 𝓢 ⊢ LO.Axioms.Imply₂ φ ψ χ
• and₁ : (φ ψ : F) → 𝓢 ⊢ LO.Axioms.AndElim₁ φ ψ
• and₂ : (φ ψ : F) → 𝓢 ⊢ LO.Axioms.AndElim₂ φ ψ
• and₃ : (φ ψ : F) → 𝓢 ⊢ LO.Axioms.AndInst φ ψ
• or₁ : (φ ψ : F) → 𝓢 ⊢ LO.Axioms.OrInst₁ φ ψ
• or₂ : (φ ψ : F) → 𝓢 ⊢ LO.Axioms.OrInst₂ φ ψ
• or₃ : (φ ψ χ : F) → 𝓢 ⊢ LO.Axioms.OrElim φ ψ χ
• dne : (φ : F) → 𝓢 ⊢ LO.Axioms.DNE φ
• nec : {φ : F} → 𝓢 ⊢ φ → 𝓢 ⊢ □φ
• K : (φ ψ : F) → 𝓢 ⊢ LO.Axioms.K φ ψ
• dia_dual : (φ : F) → 𝓢 ⊢ LO.Axioms.DiaDuality φ

class LO.System.KD {S : Type u_1} {F : Type u_2} [LO.BasicModalLogicalConnective F] [LO.System F S] (𝓢 : S) extends LO.System.K 𝓢, LO.System.HasAxiomD 𝓢 : Type (max u_2 u_3)

• mdp : {φ ψ : F} → 𝓢 ⊢ φ ➝ ψ → 𝓢 ⊢ φ → 𝓢 ⊢ ψ
• neg_equiv : (φ : F) → 𝓢 ⊢ LO.Axioms.NegEquiv φ
• verum : 𝓢 ⊢ LO.Axioms.Verum
• imply₁ : (φ ψ : F) → 𝓢 ⊢ LO.Axioms.Imply₁ φ ψ
• imply₂ : (φ ψ χ : F) → 𝓢 ⊢ LO.Axioms.Imply₂ φ ψ χ
• and₁ : (φ ψ : F) → 𝓢 ⊢ LO.Axioms.AndElim₁ φ ψ
• and₂ : (φ ψ : F) → 𝓢 ⊢ LO.Axioms.AndElim₂ φ ψ
• and₃ : (φ ψ : F) → 𝓢 ⊢ LO.Axioms.AndInst φ ψ
• or₁ : (φ ψ : F) → 𝓢 ⊢ LO.Axioms.OrInst₁ φ ψ
• or₂ : (φ ψ : F) → 𝓢 ⊢ LO.Axioms.OrInst₂ φ ψ
• or₃ : (φ ψ χ : F) → 𝓢 ⊢ LO.Axioms.OrElim φ ψ χ
• dne : (φ : F) → 𝓢 ⊢ LO.Axioms.DNE φ
• nec : {φ : F} → 𝓢 ⊢ φ → 𝓢 ⊢ □φ
• K : (φ ψ : F) → 𝓢 ⊢ LO.Axioms.K φ ψ
• dia_dual : (φ : F) → 𝓢 ⊢ LO.Axioms.DiaDuality φ
• D : (φ : F) → 𝓢 ⊢ LO.Axioms.D φ

class LO.System.KP {S : Type u_1} {F : Type u_2} [LO.BasicModalLogicalConnective F] [LO.System F S] (𝓢 : S) extends LO.System.K 𝓢, LO.System.HasAxiomP 𝓢 : Type (max u_2 u_3)

• mdp : {φ ψ : F} → 𝓢 ⊢ φ ➝ ψ → 𝓢 ⊢ φ → 𝓢 ⊢ ψ
• neg_equiv : (φ : F) → 𝓢 ⊢ LO.Axioms.NegEquiv φ
• verum : 𝓢 ⊢ LO.Axioms.Verum
• imply₁ : (φ ψ : F) → 𝓢 ⊢ LO.Axioms.Imply₁ φ ψ
• imply₂ : (φ ψ χ : F) → 𝓢 ⊢ LO.Axioms.Imply₂ φ ψ χ
• and₁ : (φ ψ : F) → 𝓢 ⊢ LO.Axioms.AndElim₁ φ ψ
• and₂ : (φ ψ : F) → 𝓢 ⊢ LO.Axioms.AndElim₂ φ ψ
• and₃ : (φ ψ : F) → 𝓢 ⊢ LO.Axioms.AndInst φ ψ
• or₁ : (φ ψ : F) → 𝓢 ⊢ LO.Axioms.OrInst₁ φ ψ
• or₂ : (φ ψ : F) → 𝓢 ⊢ LO.Axioms.OrInst₂ φ ψ
• or₃ : (φ ψ χ : F) → 𝓢 ⊢ LO.Axioms.OrElim φ ψ χ
• dne : (φ : F) → 𝓢 ⊢ LO.Axioms.DNE φ
• nec : {φ : F} → 𝓢 ⊢ φ → 𝓢 ⊢ □φ
• K : (φ ψ : F) → 𝓢 ⊢ LO.Axioms.K φ ψ
• dia_dual : (φ : F) → 𝓢 ⊢ LO.Axioms.DiaDuality φ
• P : 𝓢 ⊢ LO.Axioms.P

class LO.System.KB {S : Type u_1} {F : Type u_2} [LO.BasicModalLogicalConnective F] [LO.System F S] (𝓢 : S) extends LO.System.K 𝓢, LO.System.HasAxiomB 𝓢 : Type (max u_2 u_3)

• mdp : {φ ψ : F} → 𝓢 ⊢ φ ➝ ψ → 𝓢 ⊢ φ → 𝓢 ⊢ ψ
• neg_equiv : (φ : F) → 𝓢 ⊢ LO.Axioms.NegEquiv φ
• verum : 𝓢 ⊢ LO.Axioms.Verum
• imply₁ : (φ ψ : F) → 𝓢 ⊢ LO.Axioms.Imply₁ φ ψ
• imply₂ : (φ ψ χ : F) → 𝓢 ⊢ LO.Axioms.Imply₂ φ ψ χ
• and₁ : (φ ψ : F) → 𝓢 ⊢ LO.Axioms.AndElim₁ φ ψ
• and₂ : (φ ψ : F) → 𝓢 ⊢ LO.Axioms.AndElim₂ φ ψ
• and₃ : (φ ψ : F) → 𝓢 ⊢ LO.Axioms.AndInst φ ψ
• or₁ : (φ ψ : F) → 𝓢 ⊢ LO.Axioms.OrInst₁ φ ψ
• or₂ : (φ ψ : F) → 𝓢 ⊢ LO.Axioms.OrInst₂ φ ψ
• or₃ : (φ ψ χ : F) → 𝓢 ⊢ LO.Axioms.OrElim φ ψ χ
• dne : (φ : F) → 𝓢 ⊢ LO.Axioms.DNE φ
• nec : {φ : F} → 𝓢 ⊢ φ → 𝓢 ⊢ □φ
• K : (φ ψ : F) → 𝓢 ⊢ LO.Axioms.K φ ψ
• dia_dual : (φ : F) → 𝓢 ⊢ LO.Axioms.DiaDuality φ
• B : (φ : F) → 𝓢 ⊢ LO.Axioms.B φ

class LO.System.KT {S : Type u_1} {F : Type u_2} [LO.BasicModalLogicalConnective F] [LO.System F S] (𝓢 : S) extends LO.System.K 𝓢, LO.System.HasAxiomT 𝓢 : Type (max u_2 u_3)

• mdp : {φ ψ : F} → 𝓢 ⊢ φ ➝ ψ → 𝓢 ⊢ φ → 𝓢 ⊢ ψ
• neg_equiv : (φ : F) → 𝓢 ⊢ LO.Axioms.NegEquiv φ
• verum : 𝓢 ⊢ LO.Axioms.Verum
• imply₁ : (φ ψ : F) → 𝓢 ⊢ LO.Axioms.Imply₁ φ ψ
• imply₂ : (φ ψ χ : F) → 𝓢 ⊢ LO.Axioms.Imply₂ φ ψ χ
• and₁ : (φ ψ : F) → 𝓢 ⊢ LO.Axioms.AndElim₁ φ ψ
• and₂ : (φ ψ : F) → 𝓢 ⊢ LO.Axioms.AndElim₂ φ ψ
• and₃ : (φ ψ : F) → 𝓢 ⊢ LO.Axioms.AndInst φ ψ
• or₁ : (φ ψ : F) → 𝓢 ⊢ LO.Axioms.OrInst₁ φ ψ
• or₂ : (φ ψ : F) → 𝓢 ⊢ LO.Axioms.OrInst₂ φ ψ
• or₃ : (φ ψ χ : F) → 𝓢 ⊢ LO.Axioms.OrElim φ ψ χ
• dne : (φ : F) → 𝓢 ⊢ LO.Axioms.DNE φ
• nec : {φ : F} → 𝓢 ⊢ φ → 𝓢 ⊢ □φ
• K : (φ ψ : F) → 𝓢 ⊢ LO.Axioms.K φ ψ
• dia_dual : (φ : F) → 𝓢 ⊢ LO.Axioms.DiaDuality φ
• T : (φ : F) → 𝓢 ⊢ LO.Axioms.T φ

class LO.System.KTc {S : Type u_1} {F : Type u_2} [LO.BasicModalLogicalConnective F] [LO.System F S] (𝓢 : S) extends LO.System.K 𝓢, LO.System.HasAxiomTc 𝓢 : Type (max u_2 u_3)

• mdp : {φ ψ : F} → 𝓢 ⊢ φ ➝ ψ → 𝓢 ⊢ φ → 𝓢 ⊢ ψ
• neg_equiv : (φ : F) → 𝓢 ⊢ LO.Axioms.NegEquiv φ
• verum : 𝓢 ⊢ LO.Axioms.Verum
• imply₁ : (φ ψ : F) → 𝓢 ⊢ LO.Axioms.Imply₁ φ ψ
• imply₂ : (φ ψ χ : F) → 𝓢 ⊢ LO.Axioms.Imply₂ φ ψ χ
• and₁ : (φ ψ : F) → 𝓢 ⊢ LO.Axioms.AndElim₁ φ ψ
• and₂ : (φ ψ : F) → 𝓢 ⊢ LO.Axioms.AndElim₂ φ ψ
• and₃ : (φ ψ : F) → 𝓢 ⊢ LO.Axioms.AndInst φ ψ
• or₁ : (φ ψ : F) → 𝓢 ⊢ LO.Axioms.OrInst₁ φ ψ
• or₂ : (φ ψ : F) → 𝓢 ⊢ LO.Axioms.OrInst₂ φ ψ
• or₃ : (φ ψ χ : F) → 𝓢 ⊢ LO.Axioms.OrElim φ ψ χ
• dne : (φ : F) → 𝓢 ⊢ LO.Axioms.DNE φ
• nec : {φ : F} → 𝓢 ⊢ φ → 𝓢 ⊢ □φ
• K : (φ ψ : F) → 𝓢 ⊢ LO.Axioms.K φ ψ
• dia_dual : (φ : F) → 𝓢 ⊢ LO.Axioms.DiaDuality φ
• Tc : (φ : F) → 𝓢 ⊢ LO.Axioms.Tc φ

class LO.System.KTB {S : Type u_1} {F : Type u_2} [LO.BasicModalLogicalConnective F] [LO.System F S] (𝓢 : S) extends LO.System.K 𝓢, LO.System.HasAxiomT 𝓢, LO.System.HasAxiomB 𝓢 : Type (max u_2 u_3)

• mdp : {φ ψ : F} → 𝓢 ⊢ φ ➝ ψ → 𝓢 ⊢ φ → 𝓢 ⊢ ψ
• neg_equiv : (φ : F) → 𝓢 ⊢ LO.Axioms.NegEquiv φ
• verum : 𝓢 ⊢ LO.Axioms.Verum
• imply₁ : (φ ψ : F) → 𝓢 ⊢ LO.Axioms.Imply₁ φ ψ
• imply₂ : (φ ψ χ : F) → 𝓢 ⊢ LO.Axioms.Imply₂ φ ψ χ
• and₁ : (φ ψ : F) → 𝓢 ⊢ LO.Axioms.AndElim₁ φ ψ
• and₂ : (φ ψ : F) → 𝓢 ⊢ LO.Axioms.AndElim₂ φ ψ
• and₃ : (φ ψ : F) → 𝓢 ⊢ LO.Axioms.AndInst φ ψ
• or₁ : (φ ψ : F) → 𝓢 ⊢ LO.Axioms.OrInst₁ φ ψ
• or₂ : (φ ψ : F) → 𝓢 ⊢ LO.Axioms.OrInst₂ φ ψ
• or₃ : (φ ψ χ : F) → 𝓢 ⊢ LO.Axioms.OrElim φ ψ χ
• dne : (φ : F) → 𝓢 ⊢ LO.Axioms.DNE φ
• nec : {φ : F} → 𝓢 ⊢ φ → 𝓢 ⊢ □φ
• K : (φ ψ : F) → 𝓢 ⊢ LO.Axioms.K φ ψ
• dia_dual : (φ : F) → 𝓢 ⊢ LO.Axioms.DiaDuality φ
• T : (φ : F) → 𝓢 ⊢ LO.Axioms.T φ
• B : (φ : F) → 𝓢 ⊢ LO.Axioms.B φ

class LO.System.KD45 {S : Type u_1} {F : Type u_2} [LO.BasicModalLogicalConnective F] [LO.System F S] (𝓢 : S) extends LO.System.K 𝓢, LO.System.HasAxiomD 𝓢, LO.System.HasAxiomFour 𝓢, LO.System.HasAxiomFive 𝓢 : Type (max u_2 u_3)

• mdp : {φ ψ : F} → 𝓢 ⊢ φ ➝ ψ → 𝓢 ⊢ φ → 𝓢 ⊢ ψ
• neg_equiv : (φ : F) → 𝓢 ⊢ LO.Axioms.NegEquiv φ
• verum : 𝓢 ⊢ LO.Axioms.Verum
• imply₁ : (φ ψ : F) → 𝓢 ⊢ LO.Axioms.Imply₁ φ ψ
• imply₂ : (φ ψ χ : F) → 𝓢 ⊢ LO.Axioms.Imply₂ φ ψ χ
• and₁ : (φ ψ : F) → 𝓢 ⊢ LO.Axioms.AndElim₁ φ ψ
• and₂ : (φ ψ : F) → 𝓢 ⊢ LO.Axioms.AndElim₂ φ ψ
• and₃ : (φ ψ : F) → 𝓢 ⊢ LO.Axioms.AndInst φ ψ
• or₁ : (φ ψ : F) → 𝓢 ⊢ LO.Axioms.OrInst₁ φ ψ
• or₂ : (φ ψ : F) → 𝓢 ⊢ LO.Axioms.OrInst₂ φ ψ
• or₃ : (φ ψ χ : F) → 𝓢 ⊢ LO.Axioms.OrElim φ ψ χ
• dne : (φ : F) → 𝓢 ⊢ LO.Axioms.DNE φ
• nec : {φ : F} → 𝓢 ⊢ φ → 𝓢 ⊢ □φ
• K : (φ ψ : F) → 𝓢 ⊢ LO.Axioms.K φ ψ
• dia_dual : (φ : F) → 𝓢 ⊢ LO.Axioms.DiaDuality φ
• D : (φ : F) → 𝓢 ⊢ LO.Axioms.D φ
• Four : (φ : F) → 𝓢 ⊢ LO.Axioms.Four φ
• Five : (φ : F) → 𝓢 ⊢ LO.Axioms.Five φ

class LO.System.KB4 {S : Type u_1} {F : Type u_2} [LO.BasicModalLogicalConnective F] [LO.System F S] (𝓢 : S) extends LO.System.K 𝓢, LO.System.HasAxiomB 𝓢, LO.System.HasAxiomFour 𝓢 : Type (max u_2 u_3)

• mdp : {φ ψ : F} → 𝓢 ⊢ φ ➝ ψ → 𝓢 ⊢ φ → 𝓢 ⊢ ψ
• neg_equiv : (φ : F) → 𝓢 ⊢ LO.Axioms.NegEquiv φ
• verum : 𝓢 ⊢ LO.Axioms.Verum
• imply₁ : (φ ψ : F) → 𝓢 ⊢ LO.Axioms.Imply₁ φ ψ
• imply₂ : (φ ψ χ : F) → 𝓢 ⊢ LO.Axioms.Imply₂ φ ψ χ
• and₁ : (φ ψ : F) → 𝓢 ⊢ LO.Axioms.AndElim₁ φ ψ
• and₂ : (φ ψ : F) → 𝓢 ⊢ LO.Axioms.AndElim₂ φ ψ
• and₃ : (φ ψ : F) → 𝓢 ⊢ LO.Axioms.AndInst φ ψ
• or₁ : (φ ψ : F) → 𝓢 ⊢ LO.Axioms.OrInst₁ φ ψ
• or₂ : (φ ψ : F) → 𝓢 ⊢ LO.Axioms.OrInst₂ φ ψ
• or₃ : (φ ψ χ : F) → 𝓢 ⊢ LO.Axioms.OrElim φ ψ χ
• dne : (φ : F) → 𝓢 ⊢ LO.Axioms.DNE φ
• nec : {φ : F} → 𝓢 ⊢ φ → 𝓢 ⊢ □φ
• K : (φ ψ : F) → 𝓢 ⊢ LO.Axioms.K φ ψ
• dia_dual : (φ : F) → 𝓢 ⊢ LO.Axioms.DiaDuality φ
• B : (φ : F) → 𝓢 ⊢ LO.Axioms.B φ
• Four : (φ : F) → 𝓢 ⊢ LO.Axioms.Four φ

class LO.System.KDB {S : Type u_1} {F : Type u_2} [LO.BasicModalLogicalConnective F] [LO.System F S] (𝓢 : S) extends LO.System.K 𝓢, LO.System.HasAxiomD 𝓢, LO.System.HasAxiomB 𝓢 : Type (max u_2 u_3)

• mdp : {φ ψ : F} → 𝓢 ⊢ φ ➝ ψ → 𝓢 ⊢ φ → 𝓢 ⊢ ψ
• neg_equiv : (φ : F) → 𝓢 ⊢ LO.Axioms.NegEquiv φ
• verum : 𝓢 ⊢ LO.Axioms.Verum
• imply₁ : (φ ψ : F) → 𝓢 ⊢ LO.Axioms.Imply₁ φ ψ
• imply₂ : (φ ψ χ : F) → 𝓢 ⊢ LO.Axioms.Imply₂ φ ψ χ
• and₁ : (φ ψ : F) → 𝓢 ⊢ LO.Axioms.AndElim₁ φ ψ
• and₂ : (φ ψ : F) → 𝓢 ⊢ LO.Axioms.AndElim₂ φ ψ
• and₃ : (φ ψ : F) → 𝓢 ⊢ LO.Axioms.AndInst φ ψ
• or₁ : (φ ψ : F) → 𝓢 ⊢ LO.Axioms.OrInst₁ φ ψ
• or₂ : (φ ψ : F) → 𝓢 ⊢ LO.Axioms.OrInst₂ φ ψ
• or₃ : (φ ψ χ : F) → 𝓢 ⊢ LO.Axioms.OrElim φ ψ χ
• dne : (φ : F) → 𝓢 ⊢ LO.Axioms.DNE φ
• nec : {φ : F} → 𝓢 ⊢ φ → 𝓢 ⊢ □φ
• K : (φ ψ : F) → 𝓢 ⊢ LO.Axioms.K φ ψ
• dia_dual : (φ : F) → 𝓢 ⊢ LO.Axioms.DiaDuality φ
• D : (φ : F) → 𝓢 ⊢ LO.Axioms.D φ
• B : (φ : F) → 𝓢 ⊢ LO.Axioms.B φ

class LO.System.KD4 {S : Type u_1} {F : Type u_2} [LO.BasicModalLogicalConnective F] [LO.System F S] (𝓢 : S) extends LO.System.K 𝓢, LO.System.HasAxiomD 𝓢, LO.System.HasAxiomFour 𝓢 : Type (max u_2 u_3)

• mdp : {φ ψ : F} → 𝓢 ⊢ φ ➝ ψ → 𝓢 ⊢ φ → 𝓢 ⊢ ψ
• neg_equiv : (φ : F) → 𝓢 ⊢ LO.Axioms.NegEquiv φ
• verum : 𝓢 ⊢ LO.Axioms.Verum
• imply₁ : (φ ψ : F) → 𝓢 ⊢ LO.Axioms.Imply₁ φ ψ
• imply₂ : (φ ψ χ : F) → 𝓢 ⊢ LO.Axioms.Imply₂ φ ψ χ
• and₁ : (φ ψ : F) → 𝓢 ⊢ LO.Axioms.AndElim₁ φ ψ
• and₂ : (φ ψ : F) → 𝓢 ⊢ LO.Axioms.AndElim₂ φ ψ
• and₃ : (φ ψ : F) → 𝓢 ⊢ LO.Axioms.AndInst φ ψ
• or₁ : (φ ψ : F) → 𝓢 ⊢ LO.Axioms.OrInst₁ φ ψ
• or₂ : (φ ψ : F) → 𝓢 ⊢ LO.Axioms.OrInst₂ φ ψ
• or₃ : (φ ψ χ : F) → 𝓢 ⊢ LO.Axioms.OrElim φ ψ χ
• dne : (φ : F) → 𝓢 ⊢ LO.Axioms.DNE φ
• nec : {φ : F} → 𝓢 ⊢ φ → 𝓢 ⊢ □φ
• K : (φ ψ : F) → 𝓢 ⊢ LO.Axioms.K φ ψ
• dia_dual : (φ : F) → 𝓢 ⊢ LO.Axioms.DiaDuality φ
• D : (φ : F) → 𝓢 ⊢ LO.Axioms.D φ
• Four : (φ : F) → 𝓢 ⊢ LO.Axioms.Four φ

class LO.System.KD5 {S : Type u_1} {F : Type u_2} [LO.BasicModalLogicalConnective F] [LO.System F S] (𝓢 : S) extends LO.System.K 𝓢, LO.System.HasAxiomD 𝓢, LO.System.HasAxiomFive 𝓢 : Type (max u_2 u_3)

• mdp : {φ ψ : F} → 𝓢 ⊢ φ ➝ ψ → 𝓢 ⊢ φ → 𝓢 ⊢ ψ
• neg_equiv : (φ : F) → 𝓢 ⊢ LO.Axioms.NegEquiv φ
• verum : 𝓢 ⊢ LO.Axioms.Verum
• imply₁ : (φ ψ : F) → 𝓢 ⊢ LO.Axioms.Imply₁ φ ψ
• imply₂ : (φ ψ χ : F) → 𝓢 ⊢ LO.Axioms.Imply₂ φ ψ χ
• and₁ : (φ ψ : F) → 𝓢 ⊢ LO.Axioms.AndElim₁ φ ψ
• and₂ : (φ ψ : F) → 𝓢 ⊢ LO.Axioms.AndElim₂ φ ψ
• and₃ : (φ ψ : F) → 𝓢 ⊢ LO.Axioms.AndInst φ ψ
• or₁ : (φ ψ : F) → 𝓢 ⊢ LO.Axioms.OrInst₁ φ ψ
• or₂ : (φ ψ : F) → 𝓢 ⊢ LO.Axioms.OrInst₂ φ ψ
• or₃ : (φ ψ χ : F) → 𝓢 ⊢ LO.Axioms.OrElim φ ψ χ
• dne : (φ : F) → 𝓢 ⊢ LO.Axioms.DNE φ
• nec : {φ : F} → 𝓢 ⊢ φ → 𝓢 ⊢ □φ
• K : (φ ψ : F) → 𝓢 ⊢ LO.Axioms.K φ ψ
• dia_dual : (φ : F) → 𝓢 ⊢ LO.Axioms.DiaDuality φ
• D : (φ : F) → 𝓢 ⊢ LO.Axioms.D φ
• Five : (φ : F) → 𝓢 ⊢ LO.Axioms.Five φ

class LO.System.K45 {S : Type u_1} {F : Type u_2} [LO.BasicModalLogicalConnective F] [LO.System F S] (𝓢 : S) extends LO.System.K 𝓢, LO.System.HasAxiomFour 𝓢, LO.System.HasAxiomFive 𝓢 : Type (max u_2 u_3)

• mdp : {φ ψ : F} → 𝓢 ⊢ φ ➝ ψ → 𝓢 ⊢ φ → 𝓢 ⊢ ψ
• neg_equiv : (φ : F) → 𝓢 ⊢ LO.Axioms.NegEquiv φ
• verum : 𝓢 ⊢ LO.Axioms.Verum
• imply₁ : (φ ψ : F) → 𝓢 ⊢ LO.Axioms.Imply₁ φ ψ
• imply₂ : (φ ψ χ : F) → 𝓢 ⊢ LO.Axioms.Imply₂ φ ψ χ
• and₁ : (φ ψ : F) → 𝓢 ⊢ LO.Axioms.AndElim₁ φ ψ
• and₂ : (φ ψ : F) → 𝓢 ⊢ LO.Axioms.AndElim₂ φ ψ
• and₃ : (φ ψ : F) → 𝓢 ⊢ LO.Axioms.AndInst φ ψ
• or₁ : (φ ψ : F) → 𝓢 ⊢ LO.Axioms.OrInst₁ φ ψ
• or₂ : (φ ψ : F) → 𝓢 ⊢ LO.Axioms.OrInst₂ φ ψ
• or₃ : (φ ψ χ : F) → 𝓢 ⊢ LO.Axioms.OrElim φ ψ χ
• dne : (φ : F) → 𝓢 ⊢ LO.Axioms.DNE φ
• nec : {φ : F} → 𝓢 ⊢ φ → 𝓢 ⊢ □φ
• K : (φ ψ : F) → 𝓢 ⊢ LO.Axioms.K φ ψ
• dia_dual : (φ : F) → 𝓢 ⊢ LO.Axioms.DiaDuality φ
• Four : (φ : F) → 𝓢 ⊢ LO.Axioms.Four φ
• Five : (φ : F) → 𝓢 ⊢ LO.Axioms.Five φ

class LO.System.Triv {S : Type u_1} {F : Type u_2} [LO.BasicModalLogicalConnective F] [LO.System F S] (𝓢 : S) extends LO.System.K 𝓢, LO.System.HasAxiomT 𝓢, LO.System.HasAxiomTc 𝓢 : Type (max u_2 u_3)

• mdp : {φ ψ : F} → 𝓢 ⊢ φ ➝ ψ → 𝓢 ⊢ φ → 𝓢 ⊢ ψ
• neg_equiv : (φ : F) → 𝓢 ⊢ LO.Axioms.NegEquiv φ
• verum : 𝓢 ⊢ LO.Axioms.Verum
• imply₁ : (φ ψ : F) → 𝓢 ⊢ LO.Axioms.Imply₁ φ ψ
• imply₂ : (φ ψ χ : F) → 𝓢 ⊢ LO.Axioms.Imply₂ φ ψ χ
• and₁ : (φ ψ : F) → 𝓢 ⊢ LO.Axioms.AndElim₁ φ ψ
• and₂ : (φ ψ : F) → 𝓢 ⊢ LO.Axioms.AndElim₂ φ ψ
• and₃ : (φ ψ : F) → 𝓢 ⊢ LO.Axioms.AndInst φ ψ
• or₁ : (φ ψ : F) → 𝓢 ⊢ LO.Axioms.OrInst₁ φ ψ
• or₂ : (φ ψ : F) → 𝓢 ⊢ LO.Axioms.OrInst₂ φ ψ
• or₃ : (φ ψ χ : F) → 𝓢 ⊢ LO.Axioms.OrElim φ ψ χ
• dne : (φ : F) → 𝓢 ⊢ LO.Axioms.DNE φ
• nec : {φ : F} → 𝓢 ⊢ φ → 𝓢 ⊢ □φ
• K : (φ ψ : F) → 𝓢 ⊢ LO.Axioms.K φ ψ
• dia_dual : (φ : F) → 𝓢 ⊢ LO.Axioms.DiaDuality φ
• T : (φ : F) → 𝓢 ⊢ LO.Axioms.T φ
• Tc : (φ : F) → 𝓢 ⊢ LO.Axioms.Tc φ

instance LO.System.instKTOfTriv {S : Type u_1} {F : Type u_2} [LO.BasicModalLogicalConnective F] [LO.System F S] (𝓢 : S) [LO.System.Triv 𝓢] : LO.System.KT 𝓢

Equations

• LO.System.instKTOfTriv 𝓢 = LO.System.KT.mk

instance LO.System.instKTcOfTriv {S : Type u_1} {F : Type u_2} [LO.BasicModalLogicalConnective F] [LO.System F S] (𝓢 : S) [LO.System.Triv 𝓢] : LO.System.KTc 𝓢

Equations

• LO.System.instKTcOfTriv 𝓢 = LO.System.KTc.mk

class LO.System.Ver {S : Type u_1} {F : Type u_2} [LO.BasicModalLogicalConnective F] [LO.System F S] (𝓢 : S) extends LO.System.K 𝓢, LO.System.HasAxiomVer 𝓢 : Type (max u_2 u_3)

• mdp : {φ ψ : F} → 𝓢 ⊢ φ ➝ ψ → 𝓢 ⊢ φ → 𝓢 ⊢ ψ
• neg_equiv : (φ : F) → 𝓢 ⊢ LO.Axioms.NegEquiv φ
• verum : 𝓢 ⊢ LO.Axioms.Verum
• imply₁ : (φ ψ : F) → 𝓢 ⊢ LO.Axioms.Imply₁ φ ψ
• imply₂ : (φ ψ χ : F) → 𝓢 ⊢ LO.Axioms.Imply₂ φ ψ χ
• and₁ : (φ ψ : F) → 𝓢 ⊢ LO.Axioms.AndElim₁ φ ψ
• and₂ : (φ ψ : F) → 𝓢 ⊢ LO.Axioms.AndElim₂ φ ψ
• and₃ : (φ ψ : F) → 𝓢 ⊢ LO.Axioms.AndInst φ ψ
• or₁ : (φ ψ : F) → 𝓢 ⊢ LO.Axioms.OrInst₁ φ ψ
• or₂ : (φ ψ : F) → 𝓢 ⊢ LO.Axioms.OrInst₂ φ ψ
• or₃ : (φ ψ χ : F) → 𝓢 ⊢ LO.Axioms.OrElim φ ψ χ
• dne : (φ : F) → 𝓢 ⊢ LO.Axioms.DNE φ
• nec : {φ : F} → 𝓢 ⊢ φ → 𝓢 ⊢ □φ
• K : (φ ψ : F) → 𝓢 ⊢ LO.Axioms.K φ ψ
• dia_dual : (φ : F) → 𝓢 ⊢ LO.Axioms.DiaDuality φ
• Ver : (φ : F) → 𝓢 ⊢ LO.Axioms.Ver φ

class LO.System.K4 {S : Type u_1} {F : Type u_2} [LO.BasicModalLogicalConnective F] [LO.System F S] (𝓢 : S) extends LO.System.K 𝓢, LO.System.HasAxiomFour 𝓢 : Type (max u_2 u_3)

• mdp : {φ ψ : F} → 𝓢 ⊢ φ ➝ ψ → 𝓢 ⊢ φ → 𝓢 ⊢ ψ
• neg_equiv : (φ : F) → 𝓢 ⊢ LO.Axioms.NegEquiv φ
• verum : 𝓢 ⊢ LO.Axioms.Verum
• imply₁ : (φ ψ : F) → 𝓢 ⊢ LO.Axioms.Imply₁ φ ψ
• imply₂ : (φ ψ χ : F) → 𝓢 ⊢ LO.Axioms.Imply₂ φ ψ χ
• and₁ : (φ ψ : F) → 𝓢 ⊢ LO.Axioms.AndElim₁ φ ψ
• and₂ : (φ ψ : F) → 𝓢 ⊢ LO.Axioms.AndElim₂ φ ψ
• and₃ : (φ ψ : F) → 𝓢 ⊢ LO.Axioms.AndInst φ ψ
• or₁ : (φ ψ : F) → 𝓢 ⊢ LO.Axioms.OrInst₁ φ ψ
• or₂ : (φ ψ : F) → 𝓢 ⊢ LO.Axioms.OrInst₂ φ ψ
• or₃ : (φ ψ χ : F) → 𝓢 ⊢ LO.Axioms.OrElim φ ψ χ
• dne : (φ : F) → 𝓢 ⊢ LO.Axioms.DNE φ
• nec : {φ : F} → 𝓢 ⊢ φ → 𝓢 ⊢ □φ
• K : (φ ψ : F) → 𝓢 ⊢ LO.Axioms.K φ ψ
• dia_dual : (φ : F) → 𝓢 ⊢ LO.Axioms.DiaDuality φ
• Four : (φ : F) → 𝓢 ⊢ LO.Axioms.Four φ

class LO.System.K5 {S : Type u_1} {F : Type u_2} [LO.BasicModalLogicalConnective F] [LO.System F S] (𝓢 : S) extends LO.System.K 𝓢, LO.System.HasAxiomFive 𝓢 : Type (max u_2 u_3)

• mdp : {φ ψ : F} → 𝓢 ⊢ φ ➝ ψ → 𝓢 ⊢ φ → 𝓢 ⊢ ψ
• neg_equiv : (φ : F) → 𝓢 ⊢ LO.Axioms.NegEquiv φ
• verum : 𝓢 ⊢ LO.Axioms.Verum
• imply₁ : (φ ψ : F) → 𝓢 ⊢ LO.Axioms.Imply₁ φ ψ
• imply₂ : (φ ψ χ : F) → 𝓢 ⊢ LO.Axioms.Imply₂ φ ψ χ
• and₁ : (φ ψ : F) → 𝓢 ⊢ LO.Axioms.AndElim₁ φ ψ
• and₂ : (φ ψ : F) → 𝓢 ⊢ LO.Axioms.AndElim₂ φ ψ
• and₃ : (φ ψ : F) → 𝓢 ⊢ LO.Axioms.AndInst φ ψ
• or₁ : (φ ψ : F) → 𝓢 ⊢ LO.Axioms.OrInst₁ φ ψ
• or₂ : (φ ψ : F) → 𝓢 ⊢ LO.Axioms.OrInst₂ φ ψ
• or₃ : (φ ψ χ : F) → 𝓢 ⊢ LO.Axioms.OrElim φ ψ χ
• dne : (φ : F) → 𝓢 ⊢ LO.Axioms.DNE φ
• nec : {φ : F} → 𝓢 ⊢ φ → 𝓢 ⊢ □φ
• K : (φ ψ : F) → 𝓢 ⊢ LO.Axioms.K φ ψ
• dia_dual : (φ : F) → 𝓢 ⊢ LO.Axioms.DiaDuality φ
• Five : (φ : F) → 𝓢 ⊢ LO.Axioms.Five φ

class LO.System.S4 {S : Type u_1} {F : Type u_2} [LO.BasicModalLogicalConnective F] [LO.System F S] (𝓢 : S) extends LO.System.K 𝓢, LO.System.HasAxiomT 𝓢, LO.System.HasAxiomFour 𝓢 : Type (max u_2 u_3)

• mdp : {φ ψ : F} → 𝓢 ⊢ φ ➝ ψ → 𝓢 ⊢ φ → 𝓢 ⊢ ψ
• neg_equiv : (φ : F) → 𝓢 ⊢ LO.Axioms.NegEquiv φ
• verum : 𝓢 ⊢ LO.Axioms.Verum
• imply₁ : (φ ψ : F) → 𝓢 ⊢ LO.Axioms.Imply₁ φ ψ
• imply₂ : (φ ψ χ : F) → 𝓢 ⊢ LO.Axioms.Imply₂ φ ψ χ
• and₁ : (φ ψ : F) → 𝓢 ⊢ LO.Axioms.AndElim₁ φ ψ
• and₂ : (φ ψ : F) → 𝓢 ⊢ LO.Axioms.AndElim₂ φ ψ
• and₃ : (φ ψ : F) → 𝓢 ⊢ LO.Axioms.AndInst φ ψ
• or₁ : (φ ψ : F) → 𝓢 ⊢ LO.Axioms.OrInst₁ φ ψ
• or₂ : (φ ψ : F) → 𝓢 ⊢ LO.Axioms.OrInst₂ φ ψ
• or₃ : (φ ψ χ : F) → 𝓢 ⊢ LO.Axioms.OrElim φ ψ χ
• dne : (φ : F) → 𝓢 ⊢ LO.Axioms.DNE φ
• nec : {φ : F} → 𝓢 ⊢ φ → 𝓢 ⊢ □φ
• K : (φ ψ : F) → 𝓢 ⊢ LO.Axioms.K φ ψ
• dia_dual : (φ : F) → 𝓢 ⊢ LO.Axioms.DiaDuality φ
• T : (φ : F) → 𝓢 ⊢ LO.Axioms.T φ
• Four : (φ : F) → 𝓢 ⊢ LO.Axioms.Four φ

instance LO.System.instK4OfS4 {S : Type u_1} {F : Type u_2} [LO.BasicModalLogicalConnective F] [LO.System F S] (𝓢 : S) [LO.System.S4 𝓢] : LO.System.K4 𝓢

Equations

• LO.System.instK4OfS4 𝓢 = LO.System.K4.mk

instance LO.System.instKTOfS4 {S : Type u_1} {F : Type u_2} [LO.BasicModalLogicalConnective F] [LO.System F S] (𝓢 : S) [LO.System.S4 𝓢] : LO.System.KT 𝓢

Equations

• LO.System.instKTOfS4 𝓢 = LO.System.KT.mk

class LO.System.S4Dot2 {S : Type u_1} {F : Type u_2} [LO.BasicModalLogicalConnective F] [LO.System F S] (𝓢 : S) extends LO.System.S4 𝓢, LO.System.HasAxiomDot2 𝓢 : Type (max u_2 u_3)

• mdp : {φ ψ : F} → 𝓢 ⊢ φ ➝ ψ → 𝓢 ⊢ φ → 𝓢 ⊢ ψ
• neg_equiv : (φ : F) → 𝓢 ⊢ LO.Axioms.NegEquiv φ
• verum : 𝓢 ⊢ LO.Axioms.Verum
• imply₁ : (φ ψ : F) → 𝓢 ⊢ LO.Axioms.Imply₁ φ ψ
• imply₂ : (φ ψ χ : F) → 𝓢 ⊢ LO.Axioms.Imply₂ φ ψ χ
• and₁ : (φ ψ : F) → 𝓢 ⊢ LO.Axioms.AndElim₁ φ ψ
• and₂ : (φ ψ : F) → 𝓢 ⊢ LO.Axioms.AndElim₂ φ ψ
• and₃ : (φ ψ : F) → 𝓢 ⊢ LO.Axioms.AndInst φ ψ
• or₁ : (φ ψ : F) → 𝓢 ⊢ LO.Axioms.OrInst₁ φ ψ
• or₂ : (φ ψ : F) → 𝓢 ⊢ LO.Axioms.OrInst₂ φ ψ
• or₃ : (φ ψ χ : F) → 𝓢 ⊢ LO.Axioms.OrElim φ ψ χ
• dne : (φ : F) → 𝓢 ⊢ LO.Axioms.DNE φ
• nec : {φ : F} → 𝓢 ⊢ φ → 𝓢 ⊢ □φ
• K : (φ ψ : F) → 𝓢 ⊢ LO.Axioms.K φ ψ
• dia_dual : (φ : F) → 𝓢 ⊢ LO.Axioms.DiaDuality φ
• T : (φ : F) → 𝓢 ⊢ LO.Axioms.T φ
• Four : (φ : F) → 𝓢 ⊢ LO.Axioms.Four φ
• Dot2 : (φ : F) → 𝓢 ⊢ LO.Axioms.Dot2 φ

class LO.System.S4Dot3 {S : Type u_1} {F : Type u_2} [LO.BasicModalLogicalConnective F] [LO.System F S] (𝓢 : S) extends LO.System.S4 𝓢, LO.System.HasAxiomDot3 𝓢 : Type (max u_2 u_3)

• mdp : {φ ψ : F} → 𝓢 ⊢ φ ➝ ψ → 𝓢 ⊢ φ → 𝓢 ⊢ ψ
• neg_equiv : (φ : F) → 𝓢 ⊢ LO.Axioms.NegEquiv φ
• verum : 𝓢 ⊢ LO.Axioms.Verum
• imply₁ : (φ ψ : F) → 𝓢 ⊢ LO.Axioms.Imply₁ φ ψ
• imply₂ : (φ ψ χ : F) → 𝓢 ⊢ LO.Axioms.Imply₂ φ ψ χ
• and₁ : (φ ψ : F) → 𝓢 ⊢ LO.Axioms.AndElim₁ φ ψ
• and₂ : (φ ψ : F) → 𝓢 ⊢ LO.Axioms.AndElim₂ φ ψ
• and₃ : (φ ψ : F) → 𝓢 ⊢ LO.Axioms.AndInst φ ψ
• or₁ : (φ ψ : F) → 𝓢 ⊢ LO.Axioms.OrInst₁ φ ψ
• or₂ : (φ ψ : F) → 𝓢 ⊢ LO.Axioms.OrInst₂ φ ψ
• or₃ : (φ ψ χ : F) → 𝓢 ⊢ LO.Axioms.OrElim φ ψ χ
• dne : (φ : F) → 𝓢 ⊢ LO.Axioms.DNE φ
• nec : {φ : F} → 𝓢 ⊢ φ → 𝓢 ⊢ □φ
• K : (φ ψ : F) → 𝓢 ⊢ LO.Axioms.K φ ψ
• dia_dual : (φ : F) → 𝓢 ⊢ LO.Axioms.DiaDuality φ
• T : (φ : F) → 𝓢 ⊢ LO.Axioms.T φ
• Four : (φ : F) → 𝓢 ⊢ LO.Axioms.Four φ
• Dot3 : (φ ψ : F) → 𝓢 ⊢ LO.Axioms.Dot3 φ ψ

class LO.System.S5 {S : Type u_1} {F : Type u_2} [LO.BasicModalLogicalConnective F] [LO.System F S] (𝓢 : S) extends LO.System.K 𝓢, LO.System.HasAxiomT 𝓢, LO.System.HasAxiomFive 𝓢 : Type (max u_2 u_3)

• mdp : {φ ψ : F} → 𝓢 ⊢ φ ➝ ψ → 𝓢 ⊢ φ → 𝓢 ⊢ ψ
• neg_equiv : (φ : F) → 𝓢 ⊢ LO.Axioms.NegEquiv φ
• verum : 𝓢 ⊢ LO.Axioms.Verum
• imply₁ : (φ ψ : F) → 𝓢 ⊢ LO.Axioms.Imply₁ φ ψ
• imply₂ : (φ ψ χ : F) → 𝓢 ⊢ LO.Axioms.Imply₂ φ ψ χ
• and₁ : (φ ψ : F) → 𝓢 ⊢ LO.Axioms.AndElim₁ φ ψ
• and₂ : (φ ψ : F) → 𝓢 ⊢ LO.Axioms.AndElim₂ φ ψ
• and₃ : (φ ψ : F) → 𝓢 ⊢ LO.Axioms.AndInst φ ψ
• or₁ : (φ ψ : F) → 𝓢 ⊢ LO.Axioms.OrInst₁ φ ψ
• or₂ : (φ ψ : F) → 𝓢 ⊢ LO.Axioms.OrInst₂ φ ψ
• or₃ : (φ ψ χ : F) → 𝓢 ⊢ LO.Axioms.OrElim φ ψ χ
• dne : (φ : F) → 𝓢 ⊢ LO.Axioms.DNE φ
• nec : {φ : F} → 𝓢 ⊢ φ → 𝓢 ⊢ □φ
• K : (φ ψ : F) → 𝓢 ⊢ LO.Axioms.K φ ψ
• dia_dual : (φ : F) → 𝓢 ⊢ LO.Axioms.DiaDuality φ
• T : (φ : F) → 𝓢 ⊢ LO.Axioms.T φ
• Five : (φ : F) → 𝓢 ⊢ LO.Axioms.Five φ

instance LO.System.instKTOfS5 {S : Type u_1} {F : Type u_2} [LO.BasicModalLogicalConnective F] [LO.System F S] (𝓢 : S) [LO.System.S5 𝓢] : LO.System.KT 𝓢

Equations

• LO.System.instKTOfS5 𝓢 = LO.System.KT.mk

instance LO.System.instK5OfS5 {S : Type u_1} {F : Type u_2} [LO.BasicModalLogicalConnective F] [LO.System F S] (𝓢 : S) [LO.System.S5 𝓢] : LO.System.K5 𝓢

Equations

• LO.System.instK5OfS5 𝓢 = LO.System.K5.mk

class LO.System.GL {S : Type u_1} {F : Type u_2} [LO.BasicModalLogicalConnective F] [LO.System F S] (𝓢 : S) extends LO.System.K 𝓢, LO.System.HasAxiomL 𝓢 : Type (max u_2 u_3)

• mdp : {φ ψ : F} → 𝓢 ⊢ φ ➝ ψ → 𝓢 ⊢ φ → 𝓢 ⊢ ψ
• neg_equiv : (φ : F) → 𝓢 ⊢ LO.Axioms.NegEquiv φ
• verum : 𝓢 ⊢ LO.Axioms.Verum
• imply₁ : (φ ψ : F) → 𝓢 ⊢ LO.Axioms.Imply₁ φ ψ
• imply₂ : (φ ψ χ : F) → 𝓢 ⊢ LO.Axioms.Imply₂ φ ψ χ
• and₁ : (φ ψ : F) → 𝓢 ⊢ LO.Axioms.AndElim₁ φ ψ
• and₂ : (φ ψ : F) → 𝓢 ⊢ LO.Axioms.AndElim₂ φ ψ
• and₃ : (φ ψ : F) → 𝓢 ⊢ LO.Axioms.AndInst φ ψ
• or₁ : (φ ψ : F) → 𝓢 ⊢ LO.Axioms.OrInst₁ φ ψ
• or₂ : (φ ψ : F) → 𝓢 ⊢ LO.Axioms.OrInst₂ φ ψ
• or₃ : (φ ψ χ : F) → 𝓢 ⊢ LO.Axioms.OrElim φ ψ χ
• dne : (φ : F) → 𝓢 ⊢ LO.Axioms.DNE φ
• nec : {φ : F} → 𝓢 ⊢ φ → 𝓢 ⊢ □φ
• K : (φ ψ : F) → 𝓢 ⊢ LO.Axioms.K φ ψ
• dia_dual : (φ : F) → 𝓢 ⊢ LO.Axioms.DiaDuality φ
• L : (φ : F) → 𝓢 ⊢ LO.Axioms.L φ

class LO.System.Grz {S : Type u_1} {F : Type u_2} [LO.BasicModalLogicalConnective F] [LO.System F S] (𝓢 : S) extends LO.System.K 𝓢, LO.System.HasAxiomGrz 𝓢 : Type (max u_2 u_3)

• mdp : {φ ψ : F} → 𝓢 ⊢ φ ➝ ψ → 𝓢 ⊢ φ → 𝓢 ⊢ ψ
• neg_equiv : (φ : F) → 𝓢 ⊢ LO.Axioms.NegEquiv φ
• verum : 𝓢 ⊢ LO.Axioms.Verum
• imply₁ : (φ ψ : F) → 𝓢 ⊢ LO.Axioms.Imply₁ φ ψ
• imply₂ : (φ ψ χ : F) → 𝓢 ⊢ LO.Axioms.Imply₂ φ ψ χ
• and₁ : (φ ψ : F) → 𝓢 ⊢ LO.Axioms.AndElim₁ φ ψ
• and₂ : (φ ψ : F) → 𝓢 ⊢ LO.Axioms.AndElim₂ φ ψ
• and₃ : (φ ψ : F) → 𝓢 ⊢ LO.Axioms.AndInst φ ψ
• or₁ : (φ ψ : F) → 𝓢 ⊢ LO.Axioms.OrInst₁ φ ψ
• or₂ : (φ ψ : F) → 𝓢 ⊢ LO.Axioms.OrInst₂ φ ψ
• or₃ : (φ ψ χ : F) → 𝓢 ⊢ LO.Axioms.OrElim φ ψ χ
• dne : (φ : F) → 𝓢 ⊢ LO.Axioms.DNE φ
• nec : {φ : F} → 𝓢 ⊢ φ → 𝓢 ⊢ □φ
• K : (φ ψ : F) → 𝓢 ⊢ LO.Axioms.K φ ψ
• dia_dual : (φ : F) → 𝓢 ⊢ LO.Axioms.DiaDuality φ
• Grz : (φ : F) → 𝓢 ⊢ LO.Axioms.Grz φ

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

• modal_disjunctive : ∀ {φ ψ : F}, 𝓢 ⊢! □φ ⋎ □ψ → 𝓢 ⊢! φ ∨ 𝓢 ⊢! ψ

theorem LO.System.modal_disjunctive {S : Type u_1} {F : Type u_2} {inst✝ : LO.BasicModalLogicalConnective F} {inst✝¹ : LO.System F S} {𝓢 : S} [self : LO.System.ModalDisjunctive 𝓢] {φ ψ : F} : 𝓢 ⊢! □φ ⋎ □ψ → 𝓢 ⊢! φ ∨ 𝓢 ⊢! ψ

Alias of LO.System.ModalDisjunctive.modal_disjunctive.

instance LO.System.instModalDisjunctiveOfDisjunctiveOfUnnecessitation {S : Type u_1} {F : Type u_2} [LO.BasicModalLogicalConnective F] [LO.System F S] {𝓢 : S} [LO.System.Disjunctive 𝓢] [LO.System.Unnecessitation 𝓢] : LO.System.ModalDisjunctive 𝓢

Equations

• ⋯ = ⋯

noncomputable instance LO.System.unnecessitation_of_modalDisjunctive {S : Type u_1} {F : Type u_2} [LO.BasicModalLogicalConnective F] [LO.System F S] {𝓢 : S} [LO.System.Minimal 𝓢] [LO.System.ModalDisjunctive 𝓢] : LO.System.Unnecessitation 𝓢

Equations

• LO.System.unnecessitation_of_modalDisjunctive = { unnec := fun {φ : F} (h : 𝓢 ⊢ □φ) => Nonempty.some ⋯ }