Maximality of 𝐓𝐫𝐢𝐯 and 𝐕𝐞𝐫

𝐓𝐫𝐢𝐯 and 𝐕𝐞𝐫 are maximal in normal modal logic.

def LO.Propositional.Superintuitionistic.Formula.toModalFormula {α : Type u_1} : LO.Propositional.Superintuitionistic.Formula α → LO.Modal.Standard.Formula α

Equations

• LO.Propositional.Superintuitionistic.Formula.atom aᴹ = LO.Modal.Standard.Formula.atom a
• LO.Propositional.Superintuitionistic.Formula.verumᴹ = ⊤
• LO.Propositional.Superintuitionistic.Formula.falsumᴹ = ⊥
• p.negᴹ = ~pᴹ
• p.imp qᴹ = pᴹ ⟶ qᴹ
• p.and qᴹ = pᴹ ⋏ qᴹ
• p.or qᴹ = pᴹ ⋎ qᴹ

def LO.Propositional.Superintuitionistic.«term_ᴹ» : Lean.TrailingParserDescr

Equations

• LO.Propositional.Superintuitionistic.«term_ᴹ» = Lean.ParserDescr.trailingNode `LO.Propositional.Superintuitionistic.term_ᴹ 75 75 (Lean.ParserDescr.symbol "ᴹ")

def LO.Modal.Standard.Formula.toPropFormula {α : Type u_1} (p : LO.Modal.Standard.Formula α) : autoParam (p.degree = 0) _auto✝ → LO.Propositional.Superintuitionistic.Formula α

Equations

• (LO.Modal.Standard.Formula.atom aᴾ) x_1 = LO.Propositional.Superintuitionistic.Formula.atom a
• (LO.Modal.Standard.Formula.falsumᴾ) x_1 = ⊥
• (p_2.imp qᴾ) x_1 = (p_2ᴾ) ⋯ ⟶ (qᴾ) ⋯

def LO.Modal.Standard.Formula.«term_ᴾ» : Lean.TrailingParserDescr

Equations

• LO.Modal.Standard.Formula.«term_ᴾ» = Lean.ParserDescr.trailingNode `LO.Modal.Standard.Formula.term_ᴾ 75 75 (Lean.ParserDescr.symbol "ᴾ")

def LO.Modal.Standard.Formula.TrivTranslation {α : Type u_1} : LO.Modal.Standard.Formula α → LO.Modal.Standard.Formula α

Equations

• LO.Modal.Standard.Formula.atom aᵀ = LO.Modal.Standard.Formula.atom a
• p.boxᵀ = pᵀ
• LO.Modal.Standard.Formula.falsumᵀ = ⊥
• p.imp qᵀ = pᵀ ⟶ qᵀ

def LO.Modal.Standard.Formula.«term_ᵀ» : Lean.TrailingParserDescr

Equations

• LO.Modal.Standard.Formula.«term_ᵀ» = Lean.ParserDescr.trailingNode `LO.Modal.Standard.Formula.term_ᵀ 75 75 (Lean.ParserDescr.symbol "ᵀ")

@[simp]

theorem LO.Modal.Standard.Formula.TrivTranslation.degree_zero : ∀ {α : Type u_1} {p : LO.Modal.Standard.Formula α}, pᵀ.degree = 0

@[simp]

theorem LO.Modal.Standard.Formula.TrivTranslation.back : ∀ {α : Type u_1} {p : LO.Modal.Standard.Formula α}, (pᵀᴾ) ⋯ᴹ = pᵀ

def LO.Modal.Standard.Formula.VerTranslation {α : Type u_1} : LO.Modal.Standard.Formula α → LO.Modal.Standard.Formula α

Equations

• LO.Modal.Standard.Formula.atom aⱽ = LO.Modal.Standard.Formula.atom a
• p.boxⱽ = ⊤
• LO.Modal.Standard.Formula.falsumⱽ = ⊥
• p.imp qⱽ = pⱽ ⟶ qⱽ

def LO.Modal.Standard.Formula.«term_ⱽ» : Lean.TrailingParserDescr

Equations

• LO.Modal.Standard.Formula.«term_ⱽ» = Lean.ParserDescr.trailingNode `LO.Modal.Standard.Formula.term_ⱽ 75 75 (Lean.ParserDescr.symbol "ⱽ")

@[simp]

theorem LO.Modal.Standard.Formula.VerTranslation.degree_zero : ∀ {α : Type u_1} {p : LO.Modal.Standard.Formula α}, pⱽ.degree = 0

@[simp]

theorem LO.Modal.Standard.Formula.VerTranslation.back : ∀ {α : Type u_1} {p : LO.Modal.Standard.Formula α}, (pⱽᴾ) ⋯ᴹ = pⱽ

theorem LO.Modal.Standard.deducible_iff_trivTranslation {α : Type u_1} [DecidableEq α] {p : LO.Modal.Standard.Formula α} : 𝐓𝐫𝐢𝐯 ⊢! p ⟷ pᵀ

theorem LO.Modal.Standard.deducible_iff_verTranslation {α : Type u_1} [DecidableEq α] {p : LO.Modal.Standard.Formula α} : 𝐕𝐞𝐫 ⊢! p ⟷ pⱽ

theorem LO.Modal.Standard.of_classical {α : Type u_1} [DecidableEq α] {mΛ : LO.Modal.Standard.DeductionParameter α} {p : LO.Propositional.Superintuitionistic.Formula α} : 𝐂𝐥 ⊢! p → mΛ ⊢! pᴹ

theorem LO.Modal.Standard.iff_Triv_classical {α : Type u_1} [DecidableEq α] {p : LO.Modal.Standard.Formula α} : 𝐓𝐫𝐢𝐯 ⊢! p ↔ 𝐂𝐥 ⊢! (pᵀᴾ) ⋯

theorem LO.Modal.Standard.iff_Ver_classical {α : Type u_1} [DecidableEq α] {p : LO.Modal.Standard.Formula α} : 𝐕𝐞𝐫 ⊢! p ↔ 𝐂𝐥 ⊢! (pⱽᴾ) ⋯

theorem LO.Modal.Standard.trivTranslated_of_K4 {α : Type u_1} [DecidableEq α] {p : LO.Modal.Standard.Formula α} : 𝐊𝟒 ⊢! p → 𝐂𝐥 ⊢! (pᵀᴾ) ⋯

theorem LO.Modal.Standard.verTranslated_of_GL {α : Type u_1} [DecidableEq α] {p : LO.Modal.Standard.Formula α} : 𝐆𝐋 ⊢! p → 𝐂𝐥 ⊢! (pⱽᴾ) ⋯

theorem LO.Modal.Standard.unprovable_AxiomL_K4 {α : Type u_1} [DecidableEq α] [Inhabited α] : 𝐊𝟒 ⊬! LO.Axioms.L (LO.Modal.Standard.Formula.atom default)

theorem LO.Modal.Standard.strictReducible_K4_GL {α : Type u_1} [DecidableEq α] [Inhabited α] : 𝐊𝟒 <ₛ 𝐆𝐋

theorem LO.Modal.Standard.unprovable_AxiomT_GL {α : Type u_1} [DecidableEq α] [Inhabited α] : 𝐆𝐋 ⊬! LO.Axioms.T (LO.Modal.Standard.Formula.atom default)

instance LO.Modal.Standard.instGLConsistencyViaUnprovableAxiomT {α : Type u_1} [DecidableEq α] [Inhabited α] : LO.System.Consistent 𝐆𝐋

Equations

• ⋯ = ⋯

theorem LO.Modal.Standard.notReducible_S4_GL {α : Type u_1} [DecidableEq α] [Inhabited α] : ¬𝐒𝟒 ≤ₛ 𝐆𝐋