Maximality of 𝐓𝐫𝐢𝐯 and 𝐕𝐞𝐫

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

def LO.IntProp.Formula.toModalFormula {α : Type u_1} : LO.IntProp.Formula α → LO.Modal.Formula α

Equations

• LO.IntProp.Formula.atom aᴹ = LO.Modal.Formula.atom a
• LO.IntProp.Formula.verumᴹ = ⊤
• LO.IntProp.Formula.falsumᴹ = ⊥
• p.negᴹ = ∼pᴹ
• p.imp qᴹ = pᴹ ➝ qᴹ
• p.and qᴹ = pᴹ ⋏ qᴹ
• p.or qᴹ = pᴹ ⋎ qᴹ

def LO.IntProp.«term_ᴹ» : Lean.TrailingParserDescr

Equations

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

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

Equations

• (LO.Modal.Formula.atom aᴾ) x_1 = LO.IntProp.Formula.atom a
• (LO.Modal.Formula.falsumᴾ) x_1 = ⊥
• (p_2.imp qᴾ) x_1 = (p_2ᴾ) ⋯ ➝ (qᴾ) ⋯

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

Equations

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

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

Equations

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

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

Equations

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

@[simp]

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

@[simp]

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

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

Equations

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

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

Equations

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

@[simp]

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

@[simp]

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

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

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

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

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

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

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

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

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

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

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

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

Equations

• ⋯ = ⋯

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