Gödel Translation
Equations
Instances For
Equations
- LO.Modal.«term_ᵍ» = Lean.ParserDescr.trailingNode `LO.Modal.term_ᵍ 90 90 (Lean.ParserDescr.symbol "ᵍ")
Instances For
class
LO.Modal.ModalCompanion
{α : Type u_1}
(iΛ : LO.IntProp.Hilbert α)
(mΛ : LO.Modal.Hilbert α)
:
- companion : ∀ {p : LO.IntProp.Formula α}, iΛ ⊢! p ↔ mΛ ⊢! pᵍ
Instances
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 α}
:
theorem
LO.Modal.axiomTc_GTranslate!
{α : Type u}
[DecidableEq α]
{mΛ : LO.Modal.Hilbert α}
{p : LO.IntProp.Formula α}
[LO.System.K4 mΛ]
:
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)
:
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Λ]
:
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Λ]
: