theorem
LO.Modal.Standard.axiomTc_GTranslate!
{α : Type u}
[DecidableEq α]
{mΛ : LO.Modal.Standard.DeductionParameter α}
{p : LO.Propositional.Superintuitionistic.Formula α}
[LO.System.K4 mΛ]
:
instance
LO.Modal.Standard.instK4DeductionParameterFormulaOfS4
{α : Type u}
{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}
[DecidableEq α]
{p : LO.Propositional.Superintuitionistic.Formula α}
(h : 𝐈𝐧𝐭 ⊢! p)
:
theorem
LO.Modal.Standard.provable_S4_of_provable_efq
{α : Type u}
[DecidableEq α]
[Inhabited α]
[Encodable α]
{p : LO.Propositional.Superintuitionistic.Formula α}
:
theorem
LO.Modal.Standard.provable_efq_iff_provable_S4
{α : Type u}
[DecidableEq α]
[Inhabited α]
[Encodable α]
{p : LO.Propositional.Superintuitionistic.Formula α}
:
a.k.a. Gödel-McKinsey-Tarski Theorem
instance
LO.Modal.Standard.instModalCompanionIntuitionisticS4
{α : Type u}
[DecidableEq α]
[Inhabited α]
[Encodable α]
:
Equations
- LO.Modal.Standard.instModalCompanionIntuitionisticS4 = { companion := ⋯ }
theorem
LO.Modal.Standard.dp_of_mdp
{α : Type u}
[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Λ]
:
theorem
LO.Modal.Standard.disjunctive_of_modalDisjunctive
{α : Type u}
[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Λ]
: