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

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

def LO.System.K4Loeb.axiomL {S : Type u_1} {F : Type u_2} [LO.BasicModalLogicalConnective F] [DecidableEq F] [LO.System F S] {𝓢 : S} [LO.System.K4Loeb 𝓢] {φ : F} : 𝓢 ⊢ LO.Axioms.L φ

Equations

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

instance LO.System.K4Loeb.instHasAxiomL {S : Type u_1} {F : Type u_2} [LO.BasicModalLogicalConnective F] [DecidableEq F] [LO.System F S] {𝓢 : S} [LO.System.K4Loeb 𝓢] : LO.System.HasAxiomL 𝓢

Equations

• LO.System.K4Loeb.instHasAxiomL = { L := fun (x : F) => LO.System.K4Loeb.axiomL }

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

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

instance LO.System.K4Henkin.instLoebRule {S : Type u_1} {F : Type u_2} [LO.BasicModalLogicalConnective F] [LO.System F S] {𝓢 : S} [LO.System.K4Henkin 𝓢] : LO.System.LoebRule 𝓢

Equations

• LO.System.K4Henkin.instLoebRule = { loeb := fun {φ : F} (h : 𝓢 ⊢ □φ ➝ φ) => h⨀LO.System.henkin (LO.System.iffIntro (LO.System.axiomK' (LO.System.nec h)) LO.System.axiomFour) }

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

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

instance LO.System.K4H.instHenkinRule {S : Type u_1} {F : Type u_2} [LO.BasicModalLogicalConnective F] [LO.System F S] {𝓢 : S} [LO.System.K4H 𝓢] : LO.System.HenkinRule 𝓢

Equations

• LO.System.K4H.instHenkinRule = { henkin := fun {φ : F} (h : 𝓢 ⊢ □φ ⭤ φ) => LO.System.and₁' h⨀(LO.System.axiomH⨀LO.System.nec h) }

@[reducible, inline]

abbrev LO.Modal.Hilbert.K4H (α : Type u_1) : LO.Modal.Hilbert α

Equations

• LO.Modal.Hilbert.K4H α = LO.Modal.Hilbert.ExtK (𝟰 ∪ 𝗛)

instance LO.Modal.Hilbert.instK4HFormulaK4H {α : Type u_1} : LO.System.K4H (LO.Modal.Hilbert.K4H α)

Equations

• LO.Modal.Hilbert.instK4HFormulaK4H = LO.System.K4H.mk

@[reducible, inline]

abbrev LO.Modal.Hilbert.K4Loeb (α : Type u_1) : LO.Modal.Hilbert α

Equations

• LO.Modal.Hilbert.K4Loeb α = { axioms := 𝗞 ∪ 𝟰, rules := ⟮Nec⟯ ∪ ⟮Loeb⟯ }

instance LO.Modal.Hilbert.instHasAxiomKK4Loeb {α : Type u_1} : (LO.Modal.Hilbert.K4Loeb α).HasAxiomK

Equations

• ⋯ = ⋯

instance LO.Modal.Hilbert.instHasNecessitationK4Loeb {α : Type u_1} : (LO.Modal.Hilbert.K4Loeb α).HasNecessitation

Equations

• ⋯ = ⋯

instance LO.Modal.Hilbert.instHasLoebRuleK4Loeb {α : Type u_1} : (LO.Modal.Hilbert.K4Loeb α).HasLoebRule

Equations

• ⋯ = ⋯

instance LO.Modal.Hilbert.instK4LoebFormulaK4Loeb {α : Type u_1} : LO.System.K4Loeb (LO.Modal.Hilbert.K4Loeb α)

Equations

• LO.Modal.Hilbert.instK4LoebFormulaK4Loeb = LO.System.K4Loeb.mk

@[reducible, inline]

abbrev LO.Modal.Hilbert.K4Henkin (α : Type u_1) : LO.Modal.Hilbert α

Equations

• LO.Modal.Hilbert.K4Henkin α = { axioms := 𝗞 ∪ 𝟰, rules := ⟮Nec⟯ ∪ ⟮Henkin⟯ }

instance LO.Modal.Hilbert.instHasAxiomKK4Henkin {α : Type u_1} : (LO.Modal.Hilbert.K4Henkin α).HasAxiomK

Equations

• ⋯ = ⋯

instance LO.Modal.Hilbert.instHasNecessitationK4Henkin {α : Type u_1} : (LO.Modal.Hilbert.K4Henkin α).HasNecessitation

Equations

• ⋯ = ⋯

instance LO.Modal.Hilbert.instHasHenkinRuleK4Henkin {α : Type u_1} : (LO.Modal.Hilbert.K4Henkin α).HasHenkinRule

Equations

• ⋯ = ⋯

instance LO.Modal.Hilbert.instK4HenkinFormulaK4Henkin {α : Type u_1} : LO.System.K4Henkin (LO.Modal.Hilbert.K4Henkin α)

Equations

• LO.Modal.Hilbert.instK4HenkinFormulaK4Henkin = LO.System.K4Henkin.mk

theorem LO.Modal.Hilbert.GL_weakerThan_K4Loeb {α : Type u_1} [DecidableEq α] : LO.Modal.Hilbert.GL α ≤ₛ LO.Modal.Hilbert.K4Loeb α

theorem LO.Modal.Hilbert.K4Loeb_weakerThan_K4Henkin {α : Type u_1} [DecidableEq α] : LO.Modal.Hilbert.K4Loeb α ≤ₛ LO.Modal.Hilbert.K4Henkin α

theorem LO.Modal.Hilbert.K4Henkin_weakerThan_K4H {α : Type u_1} [DecidableEq α] : LO.Modal.Hilbert.K4Henkin α ≤ₛ LO.Modal.Hilbert.K4H α

theorem LO.Modal.Hilbert.K4Henkin_weakerThan_GL {α : Type u_1} [DecidableEq α] : LO.Modal.Hilbert.K4H α ≤ₛ LO.Modal.Hilbert.GL α

theorem LO.Modal.Hilbert.GL_equiv_K4Loeb {α : Type u_1} [DecidableEq α] : LO.Modal.Hilbert.GL α =ₛ LO.Modal.Hilbert.K4Loeb α