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

Gödel Translation

Equations

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

def LO.Modal.«term_ᵍ» : Lean.TrailingParserDescr

Equations

• LO.Modal.«term_ᵍ» = Lean.ParserDescr.trailingNode `LO.Modal.term_ᵍ 90 90 (Lean.ParserDescr.symbol "ᵍ")

class LO.Modal.ModalCompanion {α : Type u_1} (iΛ : LO.IntProp.Hilbert α) (mΛ : LO.Modal.Hilbert α) : Type

• companion : ∀ {p : LO.IntProp.Formula α}, iΛ ⊢! p ↔ mΛ ⊢! pᵍ

Instances

• LO.Modal.instModalCompanionIntuitionisticS4

theorem LO.Modal.ModalCompanion.companion {α : Type u_1} {iΛ : LO.IntProp.Hilbert α} {mΛ : LO.Modal.Hilbert α} [self : LO.Modal.ModalCompanion iΛ mΛ] {p : LO.IntProp.Formula α} : iΛ ⊢! p ↔ mΛ ⊢! pᵍ

theorem LO.Modal.axiomTc_GTranslate! {α : Type u} [DecidableEq α] {mΛ : LO.Modal.Hilbert α} {p : LO.IntProp.Formula α} [LO.System.K4 mΛ] : mΛ ⊢! pᵍ ➝ □pᵍ

instance LO.Modal.instK4HilbertFormulaOfS4 {α : Type u} {mΛ : LO.Modal.Hilbert α} [LO.System.S4 mΛ] : LO.System.K4 mΛ

Equations

• LO.Modal.instK4HilbertFormulaOfS4 = LO.System.K4.mk

theorem LO.Modal.provable_efq_of_provable_S4 {α : Type u} [DecidableEq α] {p : LO.IntProp.Formula α} (h : 𝐈𝐧𝐭 ⊢! p) : 𝐒𝟒 ⊢! pᵍ

theorem LO.Modal.dp_of_mdp {α : Type u} [DecidableEq α] {iΛ : LO.IntProp.Hilbert α} {mΛ : LO.Modal.Hilbert α} {p : LO.IntProp.Formula α} {q : LO.IntProp.Formula α} [LO.System.ModalDisjunctive mΛ] [LO.Modal.ModalCompanion iΛ mΛ] [LO.System.S4 mΛ] : iΛ ⊢! p ⋎ q → iΛ ⊢! p ∨ iΛ ⊢! q

theorem LO.Modal.disjunctive_of_modalDisjunctive {α : Type u} [DecidableEq α] {iΛ : LO.IntProp.Hilbert α} {mΛ : LO.Modal.Hilbert α} [LO.System.ModalDisjunctive mΛ] [LO.Modal.ModalCompanion iΛ mΛ] [LO.System.S4 mΛ] : LO.System.Disjunctive iΛ