Foundation.Modal.System.Basic

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

Type (max u_2 u_3)

nec {φ : F} : 𝓢 ⊢ φ → 𝓢 ⊢ □φ

Instances

LO.Modal.Hilbert.instNecessitationFormulaOfHasNecessitation

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

𝓢 ⊢ φ → 𝓢 ⊢ □φ

Alias of LO.System.Necessitation.nec.

Equations

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

source

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

𝓢 ⊢! φ → 𝓢 ⊢! □φ

source

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

𝓢 ⊢ φ → 𝓢 ⊢ □^[n]φ

Equations

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

source

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

𝓢 ⊢! φ → 𝓢 ⊢! □^[n]φ

source

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

Type (max u_2 u_3)

unnec {φ : F} : 𝓢 ⊢ □φ → 𝓢 ⊢ φ

Instances

source

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

𝓢 ⊢ □φ → 𝓢 ⊢ φ

Alias of LO.System.Unnecessitation.unnec.

Equations

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

source

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

𝓢 ⊢! □φ → 𝓢 ⊢! φ

source

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

𝓢 ⊢ □^[n]φ → 𝓢 ⊢ φ

Equations

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

source

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

𝓢 ⊢! □^[n]φ → 𝓢 ⊢! φ

source

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

Type (max u_2 u_3)

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

Instances

source

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

𝓢 ⊢ □φ ➝ φ → 𝓢 ⊢ φ

Alias of LO.System.LoebRule.loeb.

Equations

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

source

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

𝓢 ⊢! □φ ➝ φ → 𝓢 ⊢! φ

source

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

Type (max u_2 u_3)

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

Instances

source

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

𝓢 ⊢ □φ ⭤ φ → 𝓢 ⊢ φ

Alias of LO.System.HenkinRule.henkin.

Equations

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

source

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

𝓢 ⊢! □φ ⭤ φ → 𝓢 ⊢! φ

source

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

Type (max u_2 u_3)

dia_dual (φ : F) : 𝓢 ⊢ Axioms.DiaDuality φ

Instances

source

def LO.System.diaDuality {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [System F S] {𝓢 : S} [HasDiaDuality 𝓢] {φ : F} :

𝓢 ⊢ ◇φ ⭤ ∼□(∼φ)

Equations

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

source

@[simp]

theorem LO.System.dia_duality! {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [System F S] {𝓢 : S} [HasDiaDuality 𝓢] {φ : F} :

𝓢 ⊢! ◇φ ⭤ ∼□(∼φ)

source

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

Type (max u_2 u_3)

K (φ ψ : F) : 𝓢 ⊢ Axioms.K φ ψ

Instances

source

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

𝓢 ⊢ □(φ ➝ ψ) ➝ □φ ➝ □ψ

Equations

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

source

@[simp]

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

𝓢 ⊢! □(φ ➝ ψ) ➝ □φ ➝ □ψ

source

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

HasAxiomK Γ

Equations

LO.System.instHasAxiomKFiniteContext Γ = { K := fun (x x_1 : F) => LO.System.FiniteContext.of LO.System.axiomK }

source

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

HasAxiomK Γ

Equations

LO.System.instHasAxiomKContext Γ = { K := fun (x x_1 : F) => LO.System.Context.of LO.System.axiomK }

source

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

𝓢 ⊢ □φ ➝ □ψ

Equations

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

source

@[simp]

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

𝓢 ⊢! □φ ➝ □ψ

source

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

𝓢 ⊢ □ψ

Equations

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

source

@[simp]

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

𝓢 ⊢! □ψ

source

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

Type (max u_2 u_3)

T (φ : F) : 𝓢 ⊢ Axioms.T φ

Instances

source

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

𝓢 ⊢ □φ ➝ φ

Equations

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

source

@[simp]

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

𝓢 ⊢! □φ ➝ φ

source

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

HasAxiomT Γ

Equations

LO.System.instHasAxiomTFiniteContext Γ = { T := fun (x : F) => LO.System.FiniteContext.of LO.System.axiomT }

source

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

HasAxiomT Γ

Equations

LO.System.instHasAxiomTContext Γ = { T := fun (x : F) => LO.System.Context.of LO.System.axiomT }

source

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

𝓢 ⊢ φ

Equations

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

source

@[simp]

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

𝓢 ⊢! φ

source

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

Type (max u_2 u_3)

D (φ : F) : 𝓢 ⊢ Axioms.D φ

Instances

source

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

𝓢 ⊢ □φ ➝ ◇φ

Equations

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

source

@[simp]

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

𝓢 ⊢! □φ ➝ ◇φ

source

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

HasAxiomD Γ

Equations

LO.System.instHasAxiomDFiniteContext Γ = { D := fun (x : F) => LO.System.FiniteContext.of LO.System.axiomD }

source

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

HasAxiomD Γ

Equations

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

source

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

𝓢 ⊢ ◇φ

Equations

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

source

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

𝓢 ⊢! ◇φ

source

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

Type u_3

P : 𝓢 ⊢ Axioms.P

Instances

source

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

𝓢 ⊢ ∼□⊥

Equations

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

source

@[simp]

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

𝓢 ⊢! ∼□⊥

source

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

HasAxiomP Γ

Equations

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

source

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

HasAxiomP Γ

Equations

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

source

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

Type (max u_2 u_3)

B (φ : F) : 𝓢 ⊢ Axioms.B φ

Instances

source

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

𝓢 ⊢ φ ➝ □◇φ

Equations

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

source

@[simp]

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

𝓢 ⊢! φ ➝ □◇φ

source

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

HasAxiomB Γ

Equations

LO.System.instHasAxiomBFiniteContext Γ = { B := fun (x : F) => LO.System.FiniteContext.of LO.System.axiomB }

source

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

HasAxiomB Γ

Equations

LO.System.instHasAxiomBContext Γ = { B := fun (x : F) => LO.System.Context.of LO.System.axiomB }

source

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

𝓢 ⊢ □◇φ

Equations

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

source

@[simp]

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

𝓢 ⊢! □◇φ

source

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

Type (max u_2 u_3)

Four (φ : F) : 𝓢 ⊢ Axioms.Four φ

Instances

source

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

𝓢 ⊢ □φ ➝ □□φ

Equations

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

source

@[simp]

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

𝓢 ⊢! □φ ➝ □□φ

source

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

HasAxiomFour Γ

Equations

LO.System.instHasAxiomFourFiniteContext Γ = { Four := fun (x : F) => LO.System.FiniteContext.of LO.System.axiomFour }

source

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

HasAxiomFour Γ

Equations

LO.System.instHasAxiomFourContext Γ = { Four := fun (x : F) => LO.System.Context.of LO.System.axiomFour }

source

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

𝓢 ⊢ □□φ

Equations

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

source

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

𝓢 ⊢! □□φ

Equations

⋯ = ⋯

source

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

Type (max u_2 u_3)

Five (φ : F) : 𝓢 ⊢ Axioms.Five φ

Instances

source

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

𝓢 ⊢ ◇φ ➝ □◇φ

Equations

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

source

@[simp]

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

𝓢 ⊢! ◇φ ➝ □◇φ

source

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

HasAxiomFive Γ

Equations

LO.System.instHasAxiomFiveFiniteContext Γ = { Five := fun (x : F) => LO.System.FiniteContext.of LO.System.axiomFive }

source

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

HasAxiomFive Γ

Equations

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

source

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

Type (max u_2 u_3)

L (φ : F) : 𝓢 ⊢ Axioms.L φ

Instances

source

def LO.System.axiomL {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [System F S] {𝓢 : S} [HasAxiomL 𝓢] {φ : F} :

𝓢 ⊢ □(□φ ➝ φ) ➝ □φ

Equations

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

source

@[simp]

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

𝓢 ⊢! □(□φ ➝ φ) ➝ □φ

source

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

HasAxiomL Γ

Equations

LO.System.instHasAxiomLFiniteContext Γ = { L := fun (x : F) => LO.System.FiniteContext.of LO.System.axiomL }

source

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

HasAxiomL Γ

Equations

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

source

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

Type (max u_2 u_3)

Dot2 (φ : F) : 𝓢 ⊢ Axioms.Dot2 φ

Instances

source

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

Type (max u_2 u_3)

Dot3 (φ ψ : F) : 𝓢 ⊢ Axioms.Dot3 φ ψ

Instances

source

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

Type (max u_2 u_3)

Grz (φ : F) : 𝓢 ⊢ Axioms.Grz φ

Instances

source

def LO.System.axiomGrz {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [System F S] {𝓢 : S} [HasAxiomGrz 𝓢] {φ : F} :

𝓢 ⊢ □(□(φ ➝ □φ) ➝ φ) ➝ φ

Equations

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

source

@[simp]

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

𝓢 ⊢! □(□(φ ➝ □φ) ➝ φ) ➝ φ

source

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

HasAxiomGrz Γ

Equations

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

source

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

HasAxiomGrz Γ

Equations

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

source

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

Type (max u_2 u_3)

Tc (φ : F) : 𝓢 ⊢ Axioms.Tc φ

Instances

source

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

𝓢 ⊢ φ ➝ □φ

Equations

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

source

@[simp]

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

𝓢 ⊢! φ ➝ □φ

source

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

HasAxiomTc Γ

Equations

LO.System.instHasAxiomTcFiniteContext Γ = { Tc := fun (x : F) => LO.System.FiniteContext.of LO.System.axiomTc }

source

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

HasAxiomTc Γ

Equations

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

source

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

Type (max u_2 u_3)

Ver (φ : F) : 𝓢 ⊢ Axioms.Ver φ

Instances

source

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

𝓢 ⊢ □φ

Equations

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

source

@[simp]

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

𝓢 ⊢! □φ

source

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

HasAxiomVer Γ

Equations

LO.System.instHasAxiomVerFiniteContext Γ = { Ver := fun (x : F) => LO.System.FiniteContext.of LO.System.axiomVer }

source

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

HasAxiomVer Γ

Equations

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

source

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

Type (max u_2 u_3)

H (φ : F) : 𝓢 ⊢ Axioms.H φ

Instances

source

def LO.System.axiomH {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [System F S] {𝓢 : S} [HasAxiomH 𝓢] {φ : F} :

𝓢 ⊢ □(□φ ⭤ φ) ➝ □φ

Equations

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

source

@[simp]

theorem LO.System.axiomH! {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [System F S] {𝓢 : S} [HasAxiomH 𝓢] {φ : F} :

𝓢 ⊢! □(□φ ⭤ φ) ➝ □φ

source

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

HasAxiomH Γ

Equations

LO.System.instHasAxiomHFiniteContext Γ = { H := fun (x : F) => LO.System.FiniteContext.of LO.System.axiomH }

source

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

HasAxiomH Γ

Equations

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

source

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

HasDiaDuality 𝓢

Equations

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

source

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

HasDiaDuality 𝓢

Equations

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

source

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

Unnecessitation 𝓢

Equations

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

source

class LO.System.K {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [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) : 𝓢 ⊢ Axioms.NegEquiv φ
verum : 𝓢 ⊢ Axioms.Verum
imply₁ (φ ψ : F) : 𝓢 ⊢ Axioms.Imply₁ φ ψ
imply₂ (φ ψ χ : F) : 𝓢 ⊢ Axioms.Imply₂ φ ψ χ
and₁ (φ ψ : F) : 𝓢 ⊢ Axioms.AndElim₁ φ ψ
and₂ (φ ψ : F) : 𝓢 ⊢ Axioms.AndElim₂ φ ψ
and₃ (φ ψ : F) : 𝓢 ⊢ Axioms.AndInst φ ψ
or₁ (φ ψ : F) : 𝓢 ⊢ Axioms.OrInst₁ φ ψ
or₂ (φ ψ : F) : 𝓢 ⊢ Axioms.OrInst₂ φ ψ
or₃ (φ ψ χ : F) : 𝓢 ⊢ Axioms.OrElim φ ψ χ
dne (φ : F) : 𝓢 ⊢ Axioms.DNE φ
nec {φ : F} : 𝓢 ⊢ φ → 𝓢 ⊢ □φ
K (φ ψ : F) : 𝓢 ⊢ Axioms.K φ ψ
dia_dual (φ : F) : 𝓢 ⊢ Axioms.DiaDuality φ

Instances

LO.Modal.Hilbert.instKFormulaOfIsNormal

source

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

Type (max u_2 u_3)

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

Instances

LO.Modal.Hilbert.instKDFormulaKD

source

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

Type (max u_2 u_3)

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

Instances

LO.Modal.Hilbert.instKPFormulaKP

source

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

Type (max u_2 u_3)

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

Instances

LO.Modal.Hilbert.instKBFormulaKB

source

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

Type (max u_2 u_3)

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

Instances

source

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

Type (max u_2 u_3)

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

Instances

LO.System.instKTcOfTriv

source

class LO.System.KTB {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [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) : 𝓢 ⊢ Axioms.NegEquiv φ
verum : 𝓢 ⊢ Axioms.Verum
imply₁ (φ ψ : F) : 𝓢 ⊢ Axioms.Imply₁ φ ψ
imply₂ (φ ψ χ : F) : 𝓢 ⊢ Axioms.Imply₂ φ ψ χ
and₁ (φ ψ : F) : 𝓢 ⊢ Axioms.AndElim₁ φ ψ
and₂ (φ ψ : F) : 𝓢 ⊢ Axioms.AndElim₂ φ ψ
and₃ (φ ψ : F) : 𝓢 ⊢ Axioms.AndInst φ ψ
or₁ (φ ψ : F) : 𝓢 ⊢ Axioms.OrInst₁ φ ψ
or₂ (φ ψ : F) : 𝓢 ⊢ Axioms.OrInst₂ φ ψ
or₃ (φ ψ χ : F) : 𝓢 ⊢ Axioms.OrElim φ ψ χ
dne (φ : F) : 𝓢 ⊢ Axioms.DNE φ
nec {φ : F} : 𝓢 ⊢ φ → 𝓢 ⊢ □φ
K (φ ψ : F) : 𝓢 ⊢ Axioms.K φ ψ
dia_dual (φ : F) : 𝓢 ⊢ Axioms.DiaDuality φ
T (φ : F) : 𝓢 ⊢ Axioms.T φ
B (φ : F) : 𝓢 ⊢ Axioms.B φ

Instances

source

class LO.System.KD45 {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [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) : 𝓢 ⊢ Axioms.NegEquiv φ
verum : 𝓢 ⊢ Axioms.Verum
imply₁ (φ ψ : F) : 𝓢 ⊢ Axioms.Imply₁ φ ψ
imply₂ (φ ψ χ : F) : 𝓢 ⊢ Axioms.Imply₂ φ ψ χ
and₁ (φ ψ : F) : 𝓢 ⊢ Axioms.AndElim₁ φ ψ
and₂ (φ ψ : F) : 𝓢 ⊢ Axioms.AndElim₂ φ ψ
and₃ (φ ψ : F) : 𝓢 ⊢ Axioms.AndInst φ ψ
or₁ (φ ψ : F) : 𝓢 ⊢ Axioms.OrInst₁ φ ψ
or₂ (φ ψ : F) : 𝓢 ⊢ Axioms.OrInst₂ φ ψ
or₃ (φ ψ χ : F) : 𝓢 ⊢ Axioms.OrElim φ ψ χ
dne (φ : F) : 𝓢 ⊢ Axioms.DNE φ
nec {φ : F} : 𝓢 ⊢ φ → 𝓢 ⊢ □φ
K (φ ψ : F) : 𝓢 ⊢ Axioms.K φ ψ
dia_dual (φ : F) : 𝓢 ⊢ Axioms.DiaDuality φ
D (φ : F) : 𝓢 ⊢ Axioms.D φ
Four (φ : F) : 𝓢 ⊢ Axioms.Four φ
Five (φ : F) : 𝓢 ⊢ Axioms.Five φ

Instances

source

class LO.System.KB4 {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [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) : 𝓢 ⊢ Axioms.NegEquiv φ
verum : 𝓢 ⊢ Axioms.Verum
imply₁ (φ ψ : F) : 𝓢 ⊢ Axioms.Imply₁ φ ψ
imply₂ (φ ψ χ : F) : 𝓢 ⊢ Axioms.Imply₂ φ ψ χ
and₁ (φ ψ : F) : 𝓢 ⊢ Axioms.AndElim₁ φ ψ
and₂ (φ ψ : F) : 𝓢 ⊢ Axioms.AndElim₂ φ ψ
and₃ (φ ψ : F) : 𝓢 ⊢ Axioms.AndInst φ ψ
or₁ (φ ψ : F) : 𝓢 ⊢ Axioms.OrInst₁ φ ψ
or₂ (φ ψ : F) : 𝓢 ⊢ Axioms.OrInst₂ φ ψ
or₃ (φ ψ χ : F) : 𝓢 ⊢ Axioms.OrElim φ ψ χ
dne (φ : F) : 𝓢 ⊢ Axioms.DNE φ
nec {φ : F} : 𝓢 ⊢ φ → 𝓢 ⊢ □φ
K (φ ψ : F) : 𝓢 ⊢ Axioms.K φ ψ
dia_dual (φ : F) : 𝓢 ⊢ Axioms.DiaDuality φ
B (φ : F) : 𝓢 ⊢ Axioms.B φ
Four (φ : F) : 𝓢 ⊢ Axioms.Four φ

Instances

source

class LO.System.KDB {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [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) : 𝓢 ⊢ Axioms.NegEquiv φ
verum : 𝓢 ⊢ Axioms.Verum
imply₁ (φ ψ : F) : 𝓢 ⊢ Axioms.Imply₁ φ ψ
imply₂ (φ ψ χ : F) : 𝓢 ⊢ Axioms.Imply₂ φ ψ χ
and₁ (φ ψ : F) : 𝓢 ⊢ Axioms.AndElim₁ φ ψ
and₂ (φ ψ : F) : 𝓢 ⊢ Axioms.AndElim₂ φ ψ
and₃ (φ ψ : F) : 𝓢 ⊢ Axioms.AndInst φ ψ
or₁ (φ ψ : F) : 𝓢 ⊢ Axioms.OrInst₁ φ ψ
or₂ (φ ψ : F) : 𝓢 ⊢ Axioms.OrInst₂ φ ψ
or₃ (φ ψ χ : F) : 𝓢 ⊢ Axioms.OrElim φ ψ χ
dne (φ : F) : 𝓢 ⊢ Axioms.DNE φ
nec {φ : F} : 𝓢 ⊢ φ → 𝓢 ⊢ □φ
K (φ ψ : F) : 𝓢 ⊢ Axioms.K φ ψ
dia_dual (φ : F) : 𝓢 ⊢ Axioms.DiaDuality φ
D (φ : F) : 𝓢 ⊢ Axioms.D φ
B (φ : F) : 𝓢 ⊢ Axioms.B φ

Instances

source

class LO.System.KD4 {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [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) : 𝓢 ⊢ Axioms.NegEquiv φ
verum : 𝓢 ⊢ Axioms.Verum
imply₁ (φ ψ : F) : 𝓢 ⊢ Axioms.Imply₁ φ ψ
imply₂ (φ ψ χ : F) : 𝓢 ⊢ Axioms.Imply₂ φ ψ χ
and₁ (φ ψ : F) : 𝓢 ⊢ Axioms.AndElim₁ φ ψ
and₂ (φ ψ : F) : 𝓢 ⊢ Axioms.AndElim₂ φ ψ
and₃ (φ ψ : F) : 𝓢 ⊢ Axioms.AndInst φ ψ
or₁ (φ ψ : F) : 𝓢 ⊢ Axioms.OrInst₁ φ ψ
or₂ (φ ψ : F) : 𝓢 ⊢ Axioms.OrInst₂ φ ψ
or₃ (φ ψ χ : F) : 𝓢 ⊢ Axioms.OrElim φ ψ χ
dne (φ : F) : 𝓢 ⊢ Axioms.DNE φ
nec {φ : F} : 𝓢 ⊢ φ → 𝓢 ⊢ □φ
K (φ ψ : F) : 𝓢 ⊢ Axioms.K φ ψ
dia_dual (φ : F) : 𝓢 ⊢ Axioms.DiaDuality φ
D (φ : F) : 𝓢 ⊢ Axioms.D φ
Four (φ : F) : 𝓢 ⊢ Axioms.Four φ

Instances

source

class LO.System.KD5 {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [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) : 𝓢 ⊢ Axioms.NegEquiv φ
verum : 𝓢 ⊢ Axioms.Verum
imply₁ (φ ψ : F) : 𝓢 ⊢ Axioms.Imply₁ φ ψ
imply₂ (φ ψ χ : F) : 𝓢 ⊢ Axioms.Imply₂ φ ψ χ
and₁ (φ ψ : F) : 𝓢 ⊢ Axioms.AndElim₁ φ ψ
and₂ (φ ψ : F) : 𝓢 ⊢ Axioms.AndElim₂ φ ψ
and₃ (φ ψ : F) : 𝓢 ⊢ Axioms.AndInst φ ψ
or₁ (φ ψ : F) : 𝓢 ⊢ Axioms.OrInst₁ φ ψ
or₂ (φ ψ : F) : 𝓢 ⊢ Axioms.OrInst₂ φ ψ
or₃ (φ ψ χ : F) : 𝓢 ⊢ Axioms.OrElim φ ψ χ
dne (φ : F) : 𝓢 ⊢ Axioms.DNE φ
nec {φ : F} : 𝓢 ⊢ φ → 𝓢 ⊢ □φ
K (φ ψ : F) : 𝓢 ⊢ Axioms.K φ ψ
dia_dual (φ : F) : 𝓢 ⊢ Axioms.DiaDuality φ
D (φ : F) : 𝓢 ⊢ Axioms.D φ
Five (φ : F) : 𝓢 ⊢ Axioms.Five φ

Instances

source

class LO.System.K45 {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [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) : 𝓢 ⊢ Axioms.NegEquiv φ
verum : 𝓢 ⊢ Axioms.Verum
imply₁ (φ ψ : F) : 𝓢 ⊢ Axioms.Imply₁ φ ψ
imply₂ (φ ψ χ : F) : 𝓢 ⊢ Axioms.Imply₂ φ ψ χ
and₁ (φ ψ : F) : 𝓢 ⊢ Axioms.AndElim₁ φ ψ
and₂ (φ ψ : F) : 𝓢 ⊢ Axioms.AndElim₂ φ ψ
and₃ (φ ψ : F) : 𝓢 ⊢ Axioms.AndInst φ ψ
or₁ (φ ψ : F) : 𝓢 ⊢ Axioms.OrInst₁ φ ψ
or₂ (φ ψ : F) : 𝓢 ⊢ Axioms.OrInst₂ φ ψ
or₃ (φ ψ χ : F) : 𝓢 ⊢ Axioms.OrElim φ ψ χ
dne (φ : F) : 𝓢 ⊢ Axioms.DNE φ
nec {φ : F} : 𝓢 ⊢ φ → 𝓢 ⊢ □φ
K (φ ψ : F) : 𝓢 ⊢ Axioms.K φ ψ
dia_dual (φ : F) : 𝓢 ⊢ Axioms.DiaDuality φ
Four (φ : F) : 𝓢 ⊢ Axioms.Four φ
Five (φ : F) : 𝓢 ⊢ Axioms.Five φ

Instances

source

class LO.System.Triv {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [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) : 𝓢 ⊢ Axioms.NegEquiv φ
verum : 𝓢 ⊢ Axioms.Verum
imply₁ (φ ψ : F) : 𝓢 ⊢ Axioms.Imply₁ φ ψ
imply₂ (φ ψ χ : F) : 𝓢 ⊢ Axioms.Imply₂ φ ψ χ
and₁ (φ ψ : F) : 𝓢 ⊢ Axioms.AndElim₁ φ ψ
and₂ (φ ψ : F) : 𝓢 ⊢ Axioms.AndElim₂ φ ψ
and₃ (φ ψ : F) : 𝓢 ⊢ Axioms.AndInst φ ψ
or₁ (φ ψ : F) : 𝓢 ⊢ Axioms.OrInst₁ φ ψ
or₂ (φ ψ : F) : 𝓢 ⊢ Axioms.OrInst₂ φ ψ
or₃ (φ ψ χ : F) : 𝓢 ⊢ Axioms.OrElim φ ψ χ
dne (φ : F) : 𝓢 ⊢ Axioms.DNE φ
nec {φ : F} : 𝓢 ⊢ φ → 𝓢 ⊢ □φ
K (φ ψ : F) : 𝓢 ⊢ Axioms.K φ ψ
dia_dual (φ : F) : 𝓢 ⊢ Axioms.DiaDuality φ
T (φ : F) : 𝓢 ⊢ Axioms.T φ
Tc (φ : F) : 𝓢 ⊢ Axioms.Tc φ

Instances

LO.Modal.Hilbert.instTrivFormulaTriv

source

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

System.KT 𝓢

Equations

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

source

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

System.KTc 𝓢

Equations

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

source

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

Type (max u_2 u_3)

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

Instances

LO.Modal.Hilbert.instVerFormulaVer

source

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

Type (max u_2 u_3)

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

Instances

source

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

Type (max u_2 u_3)

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

Instances

source

class LO.System.S4 {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [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) : 𝓢 ⊢ Axioms.NegEquiv φ
verum : 𝓢 ⊢ Axioms.Verum
imply₁ (φ ψ : F) : 𝓢 ⊢ Axioms.Imply₁ φ ψ
imply₂ (φ ψ χ : F) : 𝓢 ⊢ Axioms.Imply₂ φ ψ χ
and₁ (φ ψ : F) : 𝓢 ⊢ Axioms.AndElim₁ φ ψ
and₂ (φ ψ : F) : 𝓢 ⊢ Axioms.AndElim₂ φ ψ
and₃ (φ ψ : F) : 𝓢 ⊢ Axioms.AndInst φ ψ
or₁ (φ ψ : F) : 𝓢 ⊢ Axioms.OrInst₁ φ ψ
or₂ (φ ψ : F) : 𝓢 ⊢ Axioms.OrInst₂ φ ψ
or₃ (φ ψ χ : F) : 𝓢 ⊢ Axioms.OrElim φ ψ χ
dne (φ : F) : 𝓢 ⊢ Axioms.DNE φ
nec {φ : F} : 𝓢 ⊢ φ → 𝓢 ⊢ □φ
K (φ ψ : F) : 𝓢 ⊢ Axioms.K φ ψ
dia_dual (φ : F) : 𝓢 ⊢ Axioms.DiaDuality φ
T (φ : F) : 𝓢 ⊢ Axioms.T φ
Four (φ : F) : 𝓢 ⊢ Axioms.Four φ

Instances

LO.Modal.Hilbert.ExtS4.instS4Formula

source

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

System.K4 𝓢

Equations

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

source

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

System.KT 𝓢

Equations

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

source

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

Type (max u_2 u_3)

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

Instances

LO.Modal.Hilbert.instS4Dot2FormulaS4Dot2

source

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

Type (max u_2 u_3)

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

Instances

LO.Modal.Hilbert.instS4Dot3FormulaS4Dot3

source

class LO.System.S5 {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [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) : 𝓢 ⊢ Axioms.NegEquiv φ
verum : 𝓢 ⊢ Axioms.Verum
imply₁ (φ ψ : F) : 𝓢 ⊢ Axioms.Imply₁ φ ψ
imply₂ (φ ψ χ : F) : 𝓢 ⊢ Axioms.Imply₂ φ ψ χ
and₁ (φ ψ : F) : 𝓢 ⊢ Axioms.AndElim₁ φ ψ
and₂ (φ ψ : F) : 𝓢 ⊢ Axioms.AndElim₂ φ ψ
and₃ (φ ψ : F) : 𝓢 ⊢ Axioms.AndInst φ ψ
or₁ (φ ψ : F) : 𝓢 ⊢ Axioms.OrInst₁ φ ψ
or₂ (φ ψ : F) : 𝓢 ⊢ Axioms.OrInst₂ φ ψ
or₃ (φ ψ χ : F) : 𝓢 ⊢ Axioms.OrElim φ ψ χ
dne (φ : F) : 𝓢 ⊢ Axioms.DNE φ
nec {φ : F} : 𝓢 ⊢ φ → 𝓢 ⊢ □φ
K (φ ψ : F) : 𝓢 ⊢ Axioms.K φ ψ
dia_dual (φ : F) : 𝓢 ⊢ Axioms.DiaDuality φ
T (φ : F) : 𝓢 ⊢ Axioms.T φ
Five (φ : F) : 𝓢 ⊢ Axioms.Five φ

Instances

LO.Modal.Hilbert.instS5FormulaS5

source

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

System.KT 𝓢

Equations

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

source

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

System.K5 𝓢

Equations

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

source

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

Type (max u_2 u_3)

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

Instances

LO.Modal.Hilbert.instGLFormulaGL

source

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

Type (max u_2 u_3)

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

Instances

LO.Modal.Hilbert.instGrzFormulaGrz

source

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

Prop

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

Instances

source

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

𝓢 ⊢! □φ ⋎ □ψ → 𝓢 ⊢! φ ∨ 𝓢 ⊢! ψ

Alias of LO.System.ModalDisjunctive.modal_disjunctive.

source

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

ModalDisjunctive 𝓢

source

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

Unnecessitation 𝓢

Equations

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