@[reducible, inline]
abbrev
LO.Modal.Standard.PLoN.CanonicalFrame
{α : Type u}
(Λ : LO.Modal.Standard.DeductionParameter α)
[Nonempty (Λ)-MCT]
:
Equations
- LO.Modal.Standard.PLoN.CanonicalFrame Λ = LO.Modal.Standard.PLoN.Frame.mk (Λ)-MCT fun (p : LO.Modal.Standard.Formula α) (Ω₁ Ω₂ : (Λ)-MCT) => ~□p ∈ Ω₁.theory ∧ ~p ∈ Ω₂.theory
Instances For
@[reducible, inline]
abbrev
LO.Modal.Standard.PLoN.CanonicalModel
{α : Type u}
(Λ : LO.Modal.Standard.DeductionParameter α)
[Nonempty (Λ)-MCT]
:
Equations
- One or more equations did not get rendered due to their size.
Instances For
instance
LO.Modal.Standard.PLoN.CanonicalModel.instSatisfies
{α : Type u}
{Λ : LO.Modal.Standard.DeductionParameter α}
[Nonempty (Λ)-MCT]
:
Equations
- LO.Modal.Standard.PLoN.CanonicalModel.instSatisfies = LO.Modal.Standard.Formula.PLoN.Satisfies.semantics (LO.Modal.Standard.PLoN.CanonicalModel Λ)
theorem
LO.Modal.Standard.PLoN.truthlemma
{α : Type u}
[DecidableEq α]
{Λ : LO.Modal.Standard.DeductionParameter α}
[Nonempty (Λ)-MCT]
[Λ.HasNecessitation]
{p : LO.Modal.Standard.Formula α}
{Ω : (LO.Modal.Standard.PLoN.CanonicalModel Λ).World}
:
theorem
LO.Modal.Standard.PLoN.complete_of_mem_canonicalFrame
{α : Type u}
[DecidableEq α]
{Λ : LO.Modal.Standard.DeductionParameter α}
[Nonempty (Λ)-MCT]
[Λ.HasNecessitation]
{p : LO.Modal.Standard.Formula α}
{𝔽 : LO.Modal.Standard.PLoN.FrameClass α}
(hFC : LO.Modal.Standard.PLoN.CanonicalFrame Λ ∈ 𝔽)
:
theorem
LO.Modal.Standard.PLoN.instComplete_of_mem_canonicalFrame
{α : Type u}
[DecidableEq α]
{Λ : LO.Modal.Standard.DeductionParameter α}
[Nonempty (Λ)-MCT]
[Λ.HasNecessitation]
{𝔽 : LO.Modal.Standard.PLoN.FrameClass α}
(hFC : LO.Modal.Standard.PLoN.CanonicalFrame Λ ∈ 𝔽)
:
LO.Complete Λ 𝔽
instance
LO.Modal.Standard.PLoN.instCompleteDeductionParameterFormulaFrameClassNAllFrameClass
{α : Type u}
[DecidableEq α]
:
Equations
- ⋯ = ⋯