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

theorem LO.Modal.Standard.axiomTc_GTranslate! {α : Type u_1} [DecidableEq α] {m𝓓 : LO.Modal.Standard.DeductionParameter α} {p : LO.Propositional.Superintuitionistic.Formula α} [LO.System.K4 m𝓓] : m𝓓 ⊢! pᵍ ⟶ □pᵍ

instance LO.Modal.Standard.instK4DeductionParameterFormulaOfS4 {α : Type u_1} {m𝓓 : LO.Modal.Standard.DeductionParameter α} [LO.System.S4 m𝓓] : LO.System.K4 m𝓓

Equations

• LO.Modal.Standard.instK4DeductionParameterFormulaOfS4 = LO.System.K4.mk

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

theorem LO.Modal.Standard.provable_S4_of_provable_efq {α : Type u_1} [DecidableEq α] [Inhabited α] [Encodable α] {p : LO.Propositional.Superintuitionistic.Formula α} : 𝐒𝟒 ⊢! pᵍ → 𝐈𝐧𝐭 ⊢! p

theorem LO.Modal.Standard.provable_efq_iff_provable_S4 {α : Type u_1} [DecidableEq α] [Inhabited α] [Encodable α] {p : LO.Propositional.Superintuitionistic.Formula α} : 𝐈𝐧𝐭 ⊢! p ↔ 𝐒𝟒 ⊢! pᵍ

a.k.a. Gödel-McKinsey-Tarski Theorem

instance LO.Modal.Standard.instModalCompanionIntuitionisticS4 {α : Type u_1} [DecidableEq α] [Inhabited α] [Encodable α] : LO.Modal.Standard.ModalCompanion 𝐈𝐧𝐭 𝐒𝟒

Equations

• LO.Modal.Standard.instModalCompanionIntuitionisticS4 = { companion := ⋯ }

theorem LO.Modal.Standard.dp_of_mdp {α : Type u_1} [DecidableEq α] {i𝓓 : LO.Propositional.Superintuitionistic.DeductionParameter α} {m𝓓 : LO.Modal.Standard.DeductionParameter α} {p : LO.Propositional.Superintuitionistic.Formula α} {q : LO.Propositional.Superintuitionistic.Formula α} [LO.System.ModalDisjunctive m𝓓] [LO.Modal.Standard.ModalCompanion i𝓓 m𝓓] [LO.System.S4 m𝓓] : i𝓓 ⊢! p ⋎ q → i𝓓 ⊢! p ∨ i𝓓 ⊢! q

theorem LO.Modal.Standard.disjunctive_of_modalDisjunctive {α : Type u_1} [DecidableEq α] {i𝓓 : LO.Propositional.Superintuitionistic.DeductionParameter α} {m𝓓 : LO.Modal.Standard.DeductionParameter α} [LO.System.ModalDisjunctive m𝓓] [LO.Modal.Standard.ModalCompanion i𝓓 m𝓓] [LO.System.S4 m𝓓] : LO.System.Disjunctive i𝓓