class LO.System.K4Loeb {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [System F S] (𝓢 : S) extends LO.System.K4 𝓢, LO.System.LoebRule 𝓢 : 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 φ
• loeb {φ : F} : 𝓢 ⊢ □φ ➝ φ → 𝓢 ⊢ φ

def LO.System.K4Loeb.axiomL {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [DecidableEq F] [System F S] {𝓢 : S} [System.K4Loeb 𝓢] {φ : F} : 𝓢 ⊢ 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} [BasicModalLogicalConnective F] [DecidableEq F] [System F S] {𝓢 : S} [System.K4Loeb 𝓢] : 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} [BasicModalLogicalConnective F] [System F S] (𝓢 : S) extends LO.System.K4 𝓢, LO.System.HenkinRule 𝓢 : 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 φ
• henkin {φ : F} : 𝓢 ⊢ □φ ⭤ φ → 𝓢 ⊢ φ

instance LO.System.K4Henkin.instLoebRule {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [System F S] {𝓢 : S} [System.K4Henkin 𝓢] : 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} [BasicModalLogicalConnective F] [System F S] (𝓢 : S) extends LO.System.K4 𝓢, LO.System.HasAxiomH 𝓢 : 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 φ
• H (φ : F) : 𝓢 ⊢ Axioms.H φ

instance LO.System.K4H.instHenkinRule {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [System F S] {𝓢 : S} [System.K4H 𝓢] : 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) : Hilbert α

Equations

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

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

Equations

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

@[reducible, inline]

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

Equations

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

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

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

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

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

Equations

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

@[reducible, inline]

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

Equations

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

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

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

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

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

Equations

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

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

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

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

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

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