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ᵍ = ⊥
• φ.negᵍ = □(∼φᵍ)
• φ.and ψᵍ = φᵍ ⋏ ψᵍ
• φ.or ψᵍ = φᵍ ⋎ ψᵍ
• φ.imp ψᵍ = □(φᵍ ➝ ψᵍ)

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} (iH : LO.IntProp.Hilbert α) (mH : LO.Modal.Hilbert α) : Prop

• companion : ∀ {φ : LO.IntProp.Formula α}, iH ⊢! φ ↔ mH ⊢! φᵍ

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

theorem LO.Modal.provable_efq_of_provable_S4 {α : Type u} {φ : LO.IntProp.Formula α} [DecidableEq α] (h : LO.IntProp.Hilbert.Int α ⊢! φ) : LO.Modal.Hilbert.S4 α ⊢! φᵍ

theorem LO.Modal.dp_of_mdp {α : Type u} {iH : LO.IntProp.Hilbert α} {mH : LO.Modal.Hilbert α} {φ ψ : LO.IntProp.Formula α} [DecidableEq α] [LO.System.ModalDisjunctive mH] [LO.Modal.ModalCompanion iH mH] [LO.System.S4 mH] : iH ⊢! φ ⋎ ψ → iH ⊢! φ ∨ iH ⊢! ψ

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