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

Gödel Translation

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.and qᵍ = pᵍ ⋏ qᵍ
• p.or qᵍ = pᵍ ⋎ qᵍ
• p.imp qᵍ = □(pᵍ ⟶ qᵍ)

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

Equations

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

class LO.Modal.Standard.ModalCompanion {α : Type u_1} (iΛ : LO.Propositional.Superintuitionistic.DeductionParameter α) (mΛ : LO.Modal.Standard.DeductionParameter α) : Type

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

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