Basic

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

Imported declaration from the Incompleteness formalization.

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

  Imported declaration from the Incompleteness formalization.

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

Alias of LO.Entailment.Necessitation.nec.

---

Imported declaration from the Incompleteness formalization.

Equations

• @LO.Entailment.nec = @LO.Entailment.Necessitation.nec

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

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

Imported declaration from the Incompleteness formalization.

Equations

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

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

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

Imported declaration from the Incompleteness formalization.

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

  Imported declaration from the Incompleteness formalization.

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

Alias of LO.Entailment.Unnecessitation.unnec.

---

Imported declaration from the Incompleteness formalization.

Equations

• @LO.Entailment.unnec = @LO.Entailment.Unnecessitation.unnec

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

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

Imported declaration from the Incompleteness formalization.

Equations

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

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

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

Imported declaration from the Incompleteness formalization.

• loeb {φ : F} : 𝓢 ⊢ □φ ==> φ → 𝓢 ⊢ φ

  Imported declaration from the Incompleteness formalization.

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

Alias of LO.Entailment.LoebRule.loeb.

---

Imported declaration from the Incompleteness formalization.

Equations

• @LO.Entailment.loeb = @LO.Entailment.LoebRule.loeb

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

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

Imported declaration from the Incompleteness formalization.

• henkin {φ : F} : 𝓢 ⊢ □φ <=> φ → 𝓢 ⊢ φ

  Imported declaration from the Incompleteness formalization.

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

Alias of LO.Entailment.HenkinRule.henkin.

---

Imported declaration from the Incompleteness formalization.

Equations

• @LO.Entailment.henkin = @LO.Entailment.HenkinRule.henkin

theorem LO.Entailment.henkin! {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [Entailment F S] {𝓢 : S} [HenkinRule 𝓢] {φ : F} : 𝓢 ⊢! □φ <=> φ → 𝓢 ⊢! φ

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

Imported declaration from the Incompleteness formalization.

• diaDual (φ : F) : 𝓢 ⊢ Axioms.DiaDuality φ

  Imported declaration from the Incompleteness formalization.

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

Imported declaration from the Incompleteness formalization.

Equations

• LO.Entailment.diaDuality = LO.Entailment.HasDiaDuality.diaDual φ

@[simp]

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

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

Imported declaration from the Incompleteness formalization.

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

  Imported declaration from the Incompleteness formalization.

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

Imported declaration from the Incompleteness formalization.

Equations

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

@[simp]

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

@[implicit_reducible]

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

Equations

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

@[implicit_reducible]

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

Equations

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

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

Imported declaration from the Incompleteness formalization.

Equations

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

@[simp]

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

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

Imported declaration from the Incompleteness formalization.

Equations

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

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

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

Imported declaration from the Incompleteness formalization.

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

  Imported declaration from the Incompleteness formalization.

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

Imported declaration from the Incompleteness formalization.

Equations

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

@[simp]

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

@[implicit_reducible]

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

Equations

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

@[implicit_reducible]

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

Equations

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

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

Imported declaration from the Incompleteness formalization.

Equations

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

@[simp]

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

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

Imported declaration from the Incompleteness formalization.

• diaTc (φ : F) : 𝓢 ⊢ Axioms.DiaTc φ

  Imported declaration from the Incompleteness formalization.

def LO.Entailment.diaTc {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [Entailment F S] {𝓢 : S} [HasAxiomDiaTc 𝓢] {φ : F} : 𝓢 ⊢ φ ==> ◇φ

Imported declaration from the Incompleteness formalization.

Equations

• LO.Entailment.diaTc = LO.Entailment.HasAxiomDiaTc.diaTc φ

@[simp]

theorem LO.Entailment.diaTc! {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [Entailment F S] {𝓢 : S} [HasAxiomDiaTc 𝓢] {φ : F} : 𝓢 ⊢! φ ==> ◇φ

@[implicit_reducible]

instance LO.Entailment.instHasAxiomDiaTcFiniteContext {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [Entailment F S] {𝓢 : S} [HasAxiomDiaTc 𝓢] [Entailment.Minimal 𝓢] (Γ : FiniteContext F 𝓢) : HasAxiomDiaTc Γ

Equations

• LO.Entailment.instHasAxiomDiaTcFiniteContext Γ = { diaTc := fun (x : F) => LO.Entailment.FiniteContext.of LO.Entailment.diaTc }

@[implicit_reducible]

instance LO.Entailment.instHasAxiomDiaTcContext {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [Entailment F S] {𝓢 : S} [HasAxiomDiaTc 𝓢] [Entailment.Minimal 𝓢] (Γ : Context F 𝓢) : HasAxiomDiaTc Γ

Equations

• LO.Entailment.instHasAxiomDiaTcContext Γ = { diaTc := fun (x : F) => LO.Entailment.Context.of LO.Entailment.diaTc }

def LO.Entailment.diaTc' {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [Entailment F S] {𝓢 : S} [HasAxiomDiaTc 𝓢] [Entailment.Minimal 𝓢] {φ : F} (h : 𝓢 ⊢ φ) : 𝓢 ⊢ ◇φ

Imported declaration from the Incompleteness formalization.

Equations

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

theorem LO.Entailment.diaTc'! {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [Entailment F S] {𝓢 : S} [HasAxiomDiaTc 𝓢] [Entailment.Minimal 𝓢] {φ : F} (h : 𝓢 ⊢! φ) : 𝓢 ⊢! ◇φ

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

Imported declaration from the Incompleteness formalization.

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

  Imported declaration from the Incompleteness formalization.

def LO.Entailment.axiomD {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [Entailment F S] {𝓢 : S} [HasAxiomD 𝓢] {φ : F} : 𝓢 ⊢ □φ ==> ◇φ

Imported declaration from the Incompleteness formalization.

Equations

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

@[simp]

theorem LO.Entailment.axiomD! {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [Entailment F S] {𝓢 : S} [HasAxiomD 𝓢] {φ : F} : 𝓢 ⊢! □φ ==> ◇φ

@[implicit_reducible]

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

Equations

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

@[implicit_reducible]

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

Equations

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

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

Imported declaration from the Incompleteness formalization.

Equations

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

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

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

Imported declaration from the Incompleteness formalization.

• P : 𝓢 ⊢ Axioms.P

  Imported declaration from the Incompleteness formalization.

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

Imported declaration from the Incompleteness formalization.

Equations

• LO.Entailment.axiomP = LO.Entailment.HasAxiomP.P

@[simp]

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

@[implicit_reducible]

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

Equations

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

@[implicit_reducible]

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

Equations

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

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

Imported declaration from the Incompleteness formalization.

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

  Imported declaration from the Incompleteness formalization.

def LO.Entailment.axiomB {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [Entailment F S] {𝓢 : S} [HasAxiomB 𝓢] {φ : F} : 𝓢 ⊢ φ ==> □◇φ

Imported declaration from the Incompleteness formalization.

Equations

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

@[simp]

theorem LO.Entailment.axiomB! {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [Entailment F S] {𝓢 : S} [HasAxiomB 𝓢] {φ : F} : 𝓢 ⊢! φ ==> □◇φ

@[implicit_reducible]

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

Equations

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

@[implicit_reducible]

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

Equations

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

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

Imported declaration from the Incompleteness formalization.

Equations

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

@[simp]

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

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

Imported declaration from the Incompleteness formalization.

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

  Imported declaration from the Incompleteness formalization.

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

Imported declaration from the Incompleteness formalization.

Equations

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

@[simp]

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

@[implicit_reducible]

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

Equations

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

@[implicit_reducible]

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

Equations

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

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

Imported declaration from the Incompleteness formalization.

Equations

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

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

Imported declaration from the Incompleteness formalization.

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

Imported declaration from the Incompleteness formalization.

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

  Imported declaration from the Incompleteness formalization.

def LO.Entailment.axiomFive {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [Entailment F S] {𝓢 : S} [HasAxiomFive 𝓢] {φ : F} : 𝓢 ⊢ ◇φ ==> □◇φ

Imported declaration from the Incompleteness formalization.

Equations

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

@[simp]

theorem LO.Entailment.axiomFive! {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [Entailment F S] {𝓢 : S} [HasAxiomFive 𝓢] {φ : F} : 𝓢 ⊢! ◇φ ==> □◇φ

@[implicit_reducible]

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

Equations

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

@[implicit_reducible]

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

Equations

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

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

Imported declaration from the Incompleteness formalization.

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

  Imported declaration from the Incompleteness formalization.

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

Imported declaration from the Incompleteness formalization.

Equations

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

@[simp]

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

@[implicit_reducible]

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

Equations

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

@[implicit_reducible]

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

Equations

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

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

Imported declaration from the Incompleteness formalization.

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

  Imported declaration from the Incompleteness formalization.

def LO.Entailment.axiomDot2 {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [Entailment F S] {𝓢 : S} [HasAxiomDot2 𝓢] {φ : F} : 𝓢 ⊢ ◇□φ ==> □◇φ

Imported declaration from the Incompleteness formalization.

Equations

• LO.Entailment.axiomDot2 = LO.Entailment.HasAxiomDot2.Dot2 φ

@[simp]

theorem LO.Entailment.axiomDot2! {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [Entailment F S] {𝓢 : S} [HasAxiomDot2 𝓢] {φ : F} : 𝓢 ⊢! ◇□φ ==> □◇φ

@[implicit_reducible]

instance LO.Entailment.instHasAxiomDot2FiniteContext {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [Entailment F S] {𝓢 : S} [HasAxiomDot2 𝓢] [Entailment.Minimal 𝓢] (Γ : FiniteContext F 𝓢) : HasAxiomDot2 Γ

Equations

• LO.Entailment.instHasAxiomDot2FiniteContext Γ = { Dot2 := fun (x : F) => LO.Entailment.FiniteContext.of LO.Entailment.axiomDot2 }

@[implicit_reducible]

instance LO.Entailment.instHasAxiomDot2Context {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [Entailment F S] {𝓢 : S} [HasAxiomDot2 𝓢] [Entailment.Minimal 𝓢] (Γ : Context F 𝓢) : HasAxiomDot2 Γ

Equations

• LO.Entailment.instHasAxiomDot2Context Γ = { Dot2 := fun (x : F) => LO.Entailment.Context.of LO.Entailment.axiomDot2 }

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

Imported declaration from the Incompleteness formalization.

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

  Imported declaration from the Incompleteness formalization.

def LO.Entailment.axiomDot3 {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [Entailment F S] {𝓢 : S} [HasAxiomDot3 𝓢] {φ ψ : F} : 𝓢 ⊢ □(□φ ==> ψ) ⋎ □(□ψ ==> φ)

Imported declaration from the Incompleteness formalization.

Equations

• LO.Entailment.axiomDot3 = LO.Entailment.HasAxiomDot3.Dot3 φ ψ

@[simp]

theorem LO.Entailment.axiomDot3! {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [Entailment F S] {𝓢 : S} [HasAxiomDot3 𝓢] {φ ψ : F} : 𝓢 ⊢! □(□φ ==> ψ) ⋎ □(□ψ ==> φ)

@[implicit_reducible]

instance LO.Entailment.instHasAxiomDot3FiniteContext {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [Entailment F S] {𝓢 : S} [HasAxiomDot3 𝓢] [Entailment.Minimal 𝓢] (Γ : FiniteContext F 𝓢) : HasAxiomDot3 Γ

Equations

• LO.Entailment.instHasAxiomDot3FiniteContext Γ = { Dot3 := fun (x x_1 : F) => LO.Entailment.FiniteContext.of LO.Entailment.axiomDot3 }

@[implicit_reducible]

instance LO.Entailment.instHasAxiomDot3Context {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [Entailment F S] {𝓢 : S} [HasAxiomDot3 𝓢] [Entailment.Minimal 𝓢] (Γ : Context F 𝓢) : HasAxiomDot3 Γ

Equations

• LO.Entailment.instHasAxiomDot3Context Γ = { Dot3 := fun (x x_1 : F) => LO.Entailment.Context.of LO.Entailment.axiomDot3 }

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

Imported declaration from the Incompleteness formalization.

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

  Imported declaration from the Incompleteness formalization.

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

Imported declaration from the Incompleteness formalization.

Equations

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

@[simp]

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

@[implicit_reducible]

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

Equations

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

@[implicit_reducible]

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

Equations

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

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

Imported declaration from the Incompleteness formalization.

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

  Imported declaration from the Incompleteness formalization.

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

Imported declaration from the Incompleteness formalization.

Equations

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

@[simp]

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

@[implicit_reducible]

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

Equations

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

@[implicit_reducible]

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

Equations

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

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

Imported declaration from the Incompleteness formalization.

• diaT (φ : F) : 𝓢 ⊢ Axioms.DiaT φ

  Imported declaration from the Incompleteness formalization.

def LO.Entailment.diaT {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [Entailment F S] {𝓢 : S} [HasAxiomDiaT 𝓢] {φ : F} : 𝓢 ⊢ ◇φ ==> φ

Imported declaration from the Incompleteness formalization.

Equations

• LO.Entailment.diaT = LO.Entailment.HasAxiomDiaT.diaT φ

@[simp]

theorem LO.Entailment.diaT! {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [Entailment F S] {𝓢 : S} [HasAxiomDiaT 𝓢] {φ : F} : 𝓢 ⊢! ◇φ ==> φ

@[implicit_reducible]

instance LO.Entailment.instHasAxiomDiaTFiniteContext {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [Entailment F S] {𝓢 : S} [HasAxiomDiaT 𝓢] [Entailment.Minimal 𝓢] (Γ : FiniteContext F 𝓢) : HasAxiomDiaT Γ

Equations

• LO.Entailment.instHasAxiomDiaTFiniteContext Γ = { diaT := fun (x : F) => LO.Entailment.FiniteContext.of LO.Entailment.diaT }

@[implicit_reducible]

instance LO.Entailment.instHasAxiomDiaTContext {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [Entailment F S] {𝓢 : S} [HasAxiomDiaT 𝓢] [Entailment.Minimal 𝓢] (Γ : Context F 𝓢) : HasAxiomDiaT Γ

Equations

• LO.Entailment.instHasAxiomDiaTContext Γ = { diaT := fun (x : F) => LO.Entailment.Context.of LO.Entailment.diaT }

def LO.Entailment.diaT' {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [Entailment F S] {𝓢 : S} [HasAxiomDiaT 𝓢] [Entailment.Minimal 𝓢] {φ : F} (h : 𝓢 ⊢ ◇φ) : 𝓢 ⊢ φ

Imported declaration from the Incompleteness formalization.

Equations

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

theorem LO.Entailment.diaT'! {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [Entailment F S] {𝓢 : S} [HasAxiomDiaT 𝓢] [Entailment.Minimal 𝓢] {φ : F} (h : 𝓢 ⊢! ◇φ) : 𝓢 ⊢! φ

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

Imported declaration from the Incompleteness formalization.

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

  Imported declaration from the Incompleteness formalization.

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

Imported declaration from the Incompleteness formalization.

Equations

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

@[simp]

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

@[implicit_reducible]

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

Equations

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

@[implicit_reducible]

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

Equations

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

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

Imported declaration from the Incompleteness formalization.

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

  Imported declaration from the Incompleteness formalization.

def LO.Entailment.axiomH {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [Entailment F S] {𝓢 : S} [HasAxiomH 𝓢] {φ : F} : 𝓢 ⊢ □(□φ <=> φ) ==> □φ

Imported declaration from the Incompleteness formalization.

Equations

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

@[simp]

theorem LO.Entailment.axiomH! {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [Entailment F S] {𝓢 : S} [HasAxiomH 𝓢] {φ : F} : 𝓢 ⊢! □(□φ <=> φ) ==> □φ

@[implicit_reducible]

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

Equations

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

@[implicit_reducible]

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

Equations

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

@[implicit_reducible]

instance LO.Entailment.instHasDiaDualityOfMinimalOfModalDeMorgan {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [Entailment F S] {𝓢 : S} [Entailment.Minimal 𝓢] [ModalDeMorgan F] : HasDiaDuality 𝓢

Equations

• LO.Entailment.instHasDiaDualityOfMinimalOfModalDeMorgan = { diaDual := fun (φ : F) => ⋯.mpr (LO.Entailment.iffId (◇φ)) }

@[implicit_reducible]

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

Equations

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

@[implicit_reducible]

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

Equations

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

class LO.Entailment.K {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [Entailment F S] (𝓢 : S) extends LO.Entailment.Classical 𝓢, LO.Entailment.Necessitation 𝓢, LO.Entailment.HasAxiomK 𝓢, LO.Entailment.HasDiaDuality 𝓢 : Type (max u_2 u_3)

Imported declaration from the Incompleteness formalization.

• mdp {φ ψ : F} : 𝓢 ⊢ φ ==> ψ → 𝓢 ⊢ φ → 𝓢 ⊢ ψ
• negEquiv (φ : 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 φ ψ
• diaDual (φ : F) : 𝓢 ⊢ Axioms.DiaDuality φ

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

Imported declaration from the Incompleteness formalization.

• mdp {φ ψ : F} : 𝓢 ⊢ φ ==> ψ → 𝓢 ⊢ φ → 𝓢 ⊢ ψ
• negEquiv (φ : 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 φ ψ
• diaDual (φ : F) : 𝓢 ⊢ Axioms.DiaDuality φ
• D (φ : F) : 𝓢 ⊢ Axioms.D φ

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

Imported declaration from the Incompleteness formalization.

• mdp {φ ψ : F} : 𝓢 ⊢ φ ==> ψ → 𝓢 ⊢ φ → 𝓢 ⊢ ψ
• negEquiv (φ : 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 φ ψ
• diaDual (φ : F) : 𝓢 ⊢ Axioms.DiaDuality φ
• P : 𝓢 ⊢ Axioms.P

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

Imported declaration from the Incompleteness formalization.

• mdp {φ ψ : F} : 𝓢 ⊢ φ ==> ψ → 𝓢 ⊢ φ → 𝓢 ⊢ ψ
• negEquiv (φ : 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 φ ψ
• diaDual (φ : F) : 𝓢 ⊢ Axioms.DiaDuality φ
• B (φ : F) : 𝓢 ⊢ Axioms.B φ

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

Imported declaration from the Incompleteness formalization.

• mdp {φ ψ : F} : 𝓢 ⊢ φ ==> ψ → 𝓢 ⊢ φ → 𝓢 ⊢ ψ
• negEquiv (φ : 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 φ ψ
• diaDual (φ : F) : 𝓢 ⊢ Axioms.DiaDuality φ
• T (φ : F) : 𝓢 ⊢ Axioms.T φ

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

Imported declaration from the Incompleteness formalization.

• mdp {φ ψ : F} : 𝓢 ⊢ φ ==> ψ → 𝓢 ⊢ φ → 𝓢 ⊢ ψ
• negEquiv (φ : 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 φ ψ
• diaDual (φ : F) : 𝓢 ⊢ Axioms.DiaDuality φ
• diaTc (φ : F) : 𝓢 ⊢ Axioms.DiaTc φ

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

Imported declaration from the Incompleteness formalization.

• mdp {φ ψ : F} : 𝓢 ⊢ φ ==> ψ → 𝓢 ⊢ φ → 𝓢 ⊢ ψ
• negEquiv (φ : 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 φ ψ
• diaDual (φ : F) : 𝓢 ⊢ Axioms.DiaDuality φ
• Tc (φ : F) : 𝓢 ⊢ Axioms.Tc φ

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

Imported declaration from the Incompleteness formalization.

• mdp {φ ψ : F} : 𝓢 ⊢ φ ==> ψ → 𝓢 ⊢ φ → 𝓢 ⊢ ψ
• negEquiv (φ : 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 φ ψ
• diaDual (φ : F) : 𝓢 ⊢ Axioms.DiaDuality φ
• diaT (φ : F) : 𝓢 ⊢ Axioms.DiaT φ

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

Imported declaration from the Incompleteness formalization.

• mdp {φ ψ : F} : 𝓢 ⊢ φ ==> ψ → 𝓢 ⊢ φ → 𝓢 ⊢ ψ
• negEquiv (φ : 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 φ ψ
• diaDual (φ : F) : 𝓢 ⊢ Axioms.DiaDuality φ
• T (φ : F) : 𝓢 ⊢ Axioms.T φ
• B (φ : F) : 𝓢 ⊢ Axioms.B φ

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

Imported declaration from the Incompleteness formalization.

• mdp {φ ψ : F} : 𝓢 ⊢ φ ==> ψ → 𝓢 ⊢ φ → 𝓢 ⊢ ψ
• negEquiv (φ : 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 φ ψ
• diaDual (φ : F) : 𝓢 ⊢ Axioms.DiaDuality φ
• D (φ : F) : 𝓢 ⊢ Axioms.D φ
• Four (φ : F) : 𝓢 ⊢ Axioms.Four φ
• Five (φ : F) : 𝓢 ⊢ Axioms.Five φ

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

Imported declaration from the Incompleteness formalization.

• mdp {φ ψ : F} : 𝓢 ⊢ φ ==> ψ → 𝓢 ⊢ φ → 𝓢 ⊢ ψ
• negEquiv (φ : 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 φ ψ
• diaDual (φ : F) : 𝓢 ⊢ Axioms.DiaDuality φ
• B (φ : F) : 𝓢 ⊢ Axioms.B φ
• Four (φ : F) : 𝓢 ⊢ Axioms.Four φ

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

Imported declaration from the Incompleteness formalization.

• mdp {φ ψ : F} : 𝓢 ⊢ φ ==> ψ → 𝓢 ⊢ φ → 𝓢 ⊢ ψ
• negEquiv (φ : 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 φ ψ
• diaDual (φ : F) : 𝓢 ⊢ Axioms.DiaDuality φ
• B (φ : F) : 𝓢 ⊢ Axioms.B φ
• Five (φ : F) : 𝓢 ⊢ Axioms.Five φ

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

Imported declaration from the Incompleteness formalization.

• mdp {φ ψ : F} : 𝓢 ⊢ φ ==> ψ → 𝓢 ⊢ φ → 𝓢 ⊢ ψ
• negEquiv (φ : 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 φ ψ
• diaDual (φ : F) : 𝓢 ⊢ Axioms.DiaDuality φ
• D (φ : F) : 𝓢 ⊢ Axioms.D φ
• B (φ : F) : 𝓢 ⊢ Axioms.B φ

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

Imported declaration from the Incompleteness formalization.

• mdp {φ ψ : F} : 𝓢 ⊢ φ ==> ψ → 𝓢 ⊢ φ → 𝓢 ⊢ ψ
• negEquiv (φ : 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 φ ψ
• diaDual (φ : F) : 𝓢 ⊢ Axioms.DiaDuality φ
• D (φ : F) : 𝓢 ⊢ Axioms.D φ
• Four (φ : F) : 𝓢 ⊢ Axioms.Four φ

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

Imported declaration from the Incompleteness formalization.

• mdp {φ ψ : F} : 𝓢 ⊢ φ ==> ψ → 𝓢 ⊢ φ → 𝓢 ⊢ ψ
• negEquiv (φ : 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 φ ψ
• diaDual (φ : F) : 𝓢 ⊢ Axioms.DiaDuality φ
• D (φ : F) : 𝓢 ⊢ Axioms.D φ
• Five (φ : F) : 𝓢 ⊢ Axioms.Five φ

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

Imported declaration from the Incompleteness formalization.

• mdp {φ ψ : F} : 𝓢 ⊢ φ ==> ψ → 𝓢 ⊢ φ → 𝓢 ⊢ ψ
• negEquiv (φ : 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 φ ψ
• diaDual (φ : F) : 𝓢 ⊢ Axioms.DiaDuality φ
• Four (φ : F) : 𝓢 ⊢ Axioms.Four φ
• Five (φ : F) : 𝓢 ⊢ Axioms.Five φ

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

Imported declaration from the Incompleteness formalization.

• mdp {φ ψ : F} : 𝓢 ⊢ φ ==> ψ → 𝓢 ⊢ φ → 𝓢 ⊢ ψ
• negEquiv (φ : 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 φ ψ
• diaDual (φ : F) : 𝓢 ⊢ Axioms.DiaDuality φ
• T (φ : F) : 𝓢 ⊢ Axioms.T φ
• Tc (φ : F) : 𝓢 ⊢ Axioms.Tc φ

@[implicit_reducible]

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

Equations

• LO.Entailment.instKTOfTriv 𝓢 = { toK := inst✝.toK, toHasAxiomT := inst✝.toHasAxiomT }

@[implicit_reducible]

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

Equations

• LO.Entailment.instKTcOfTriv 𝓢 = { toK := inst✝.toK, toHasAxiomTc := inst✝.toHasAxiomTc }

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

Imported declaration from the Incompleteness formalization.

• mdp {φ ψ : F} : 𝓢 ⊢ φ ==> ψ → 𝓢 ⊢ φ → 𝓢 ⊢ ψ
• negEquiv (φ : 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 φ ψ
• diaDual (φ : F) : 𝓢 ⊢ Axioms.DiaDuality φ
• Ver (φ : F) : 𝓢 ⊢ Axioms.Ver φ

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

Imported declaration from the Incompleteness formalization.

• mdp {φ ψ : F} : 𝓢 ⊢ φ ==> ψ → 𝓢 ⊢ φ → 𝓢 ⊢ ψ
• negEquiv (φ : 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 φ ψ
• diaDual (φ : F) : 𝓢 ⊢ Axioms.DiaDuality φ
• Four (φ : F) : 𝓢 ⊢ Axioms.Four φ

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

Imported declaration from the Incompleteness formalization.

• mdp {φ ψ : F} : 𝓢 ⊢ φ ==> ψ → 𝓢 ⊢ φ → 𝓢 ⊢ ψ
• negEquiv (φ : 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 φ ψ
• diaDual (φ : F) : 𝓢 ⊢ Axioms.DiaDuality φ
• Five (φ : F) : 𝓢 ⊢ Axioms.Five φ

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

Imported declaration from the Incompleteness formalization.

• mdp {φ ψ : F} : 𝓢 ⊢ φ ==> ψ → 𝓢 ⊢ φ → 𝓢 ⊢ ψ
• negEquiv (φ : 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 φ ψ
• diaDual (φ : F) : 𝓢 ⊢ Axioms.DiaDuality φ
• T (φ : F) : 𝓢 ⊢ Axioms.T φ
• Four (φ : F) : 𝓢 ⊢ Axioms.Four φ

@[implicit_reducible]

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

Equations

• LO.Entailment.instK4OfS4 𝓢 = { toK := inst✝.toK, toHasAxiomFour := inst✝.toHasAxiomFour }

@[implicit_reducible]

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

Equations

• LO.Entailment.instKTOfS4 𝓢 = { toK := inst✝.toK, toHasAxiomT := inst✝.toHasAxiomT }

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

Imported declaration from the Incompleteness formalization.

• mdp {φ ψ : F} : 𝓢 ⊢ φ ==> ψ → 𝓢 ⊢ φ → 𝓢 ⊢ ψ
• negEquiv (φ : 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 φ ψ
• diaDual (φ : F) : 𝓢 ⊢ Axioms.DiaDuality φ
• T (φ : F) : 𝓢 ⊢ Axioms.T φ
• Four (φ : F) : 𝓢 ⊢ Axioms.Four φ
• Dot2 (φ : F) : 𝓢 ⊢ Axioms.Dot2 φ

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

Imported declaration from the Incompleteness formalization.

• mdp {φ ψ : F} : 𝓢 ⊢ φ ==> ψ → 𝓢 ⊢ φ → 𝓢 ⊢ ψ
• negEquiv (φ : 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 φ ψ
• diaDual (φ : F) : 𝓢 ⊢ Axioms.DiaDuality φ
• T (φ : F) : 𝓢 ⊢ Axioms.T φ
• Four (φ : F) : 𝓢 ⊢ Axioms.Four φ
• Dot3 (φ ψ : F) : 𝓢 ⊢ Axioms.Dot3 φ ψ

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

Imported declaration from the Incompleteness formalization.

• mdp {φ ψ : F} : 𝓢 ⊢ φ ==> ψ → 𝓢 ⊢ φ → 𝓢 ⊢ ψ
• negEquiv (φ : 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 φ ψ
• diaDual (φ : F) : 𝓢 ⊢ Axioms.DiaDuality φ
• T (φ : F) : 𝓢 ⊢ Axioms.T φ
• Five (φ : F) : 𝓢 ⊢ Axioms.Five φ

@[implicit_reducible]

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

Equations

• LO.Entailment.instKTOfS5 𝓢 = { toK := inst✝.toK, toHasAxiomT := inst✝.toHasAxiomT }

@[implicit_reducible]

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

Equations

• LO.Entailment.instK5OfS5 𝓢 = { toK := inst✝.toK, toHasAxiomFive := inst✝.toHasAxiomFive }

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

Imported declaration from the Incompleteness formalization.

• mdp {φ ψ : F} : 𝓢 ⊢ φ ==> ψ → 𝓢 ⊢ φ → 𝓢 ⊢ ψ
• negEquiv (φ : 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 φ ψ
• diaDual (φ : F) : 𝓢 ⊢ Axioms.DiaDuality φ
• L (φ : F) : 𝓢 ⊢ Axioms.L φ

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

Imported declaration from the Incompleteness formalization.

• mdp {φ ψ : F} : 𝓢 ⊢ φ ==> ψ → 𝓢 ⊢ φ → 𝓢 ⊢ ψ
• negEquiv (φ : 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 φ ψ
• diaDual (φ : F) : 𝓢 ⊢ Axioms.DiaDuality φ
• Grz (φ : F) : 𝓢 ⊢ Axioms.Grz φ

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

Imported declaration from the Incompleteness formalization.

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

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

Alias of LO.Entailment.ModalDisjunctive.modal_disjunctive.

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

@[implicit_reducible]

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

Equations

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