Documentation

Logic.Modal.Maximal

Maximality of 𝐓𝐫𝐢𝐯 and 𝐕𝐞𝐫 #

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

Equations
Equations
@[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
@[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.of_classical {α : Type u_1} [DecidableEq α] {mΛ : LO.Modal.Hilbert α} {p : LO.IntProp.Formula α} :
𝐂𝐥 ⊢! p ⊢! p