@[reducible, inline]
abbrev
LO.Modal.Standard.Kripke.CanonicalFrame
{α : Type u}
(Λ : LO.Modal.Standard.DeductionParameter α)
[Nonempty (Λ)-MCT]
:
Equations
- LO.Modal.Standard.Kripke.CanonicalFrame Λ = LO.Kripke.Frame.mk (Λ)-MCT fun (Ω₁ Ω₂ : (Λ)-MCT) => □''⁻¹Ω₁.theory ⊆ Ω₂.theory
Instances For
@[simp]
theorem
LO.Modal.Standard.Kripke.CanonicalFrame.rel_def_box
{α : Type u}
{Λ : LO.Modal.Standard.DeductionParameter α}
[Nonempty (Λ)-MCT]
{Ω₁ : (LO.Modal.Standard.Kripke.CanonicalFrame Λ).World}
{Ω₂ : (LO.Modal.Standard.Kripke.CanonicalFrame Λ).World}
:
theorem
LO.Modal.Standard.Kripke.CanonicalFrame.multirel_def_multibox
{α : Type u}
[DecidableEq α]
{Λ : LO.Modal.Standard.DeductionParameter α}
[Λ.IsNormal]
[Nonempty (Λ)-MCT]
{Ω₁ : (LO.Modal.Standard.Kripke.CanonicalFrame Λ).World}
{Ω₂ : (LO.Modal.Standard.Kripke.CanonicalFrame Λ).World}
{n : ℕ}
:
theorem
LO.Modal.Standard.Kripke.CanonicalFrame.multirel_def_multibox'
{α : Type u}
[DecidableEq α]
{Λ : LO.Modal.Standard.DeductionParameter α}
[Λ.IsNormal]
[Nonempty (Λ)-MCT]
{Ω₁ : (LO.Modal.Standard.Kripke.CanonicalFrame Λ).World}
{Ω₂ : (LO.Modal.Standard.Kripke.CanonicalFrame Λ).World}
{n : ℕ}
:
theorem
LO.Modal.Standard.Kripke.CanonicalFrame.multirel_def_multidia
{α : Type u}
[DecidableEq α]
{Λ : LO.Modal.Standard.DeductionParameter α}
[Λ.IsNormal]
[Nonempty (Λ)-MCT]
{Ω₁ : (LO.Modal.Standard.Kripke.CanonicalFrame Λ).World}
{Ω₂ : (LO.Modal.Standard.Kripke.CanonicalFrame Λ).World}
{n : ℕ}
:
theorem
LO.Modal.Standard.Kripke.CanonicalFrame.rel_def_dia
{α : Type u}
[DecidableEq α]
{Λ : LO.Modal.Standard.DeductionParameter α}
[Λ.IsNormal]
[Nonempty (Λ)-MCT]
{Ω₁ : (LO.Modal.Standard.Kripke.CanonicalFrame Λ).World}
{Ω₂ : (LO.Modal.Standard.Kripke.CanonicalFrame Λ).World}
:
@[reducible, inline]
abbrev
LO.Modal.Standard.Kripke.CanonicalModel
{α : Type u}
(Λ : LO.Modal.Standard.DeductionParameter α)
[Nonempty (Λ)-MCT]
:
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[reducible]
instance
LO.Modal.Standard.Kripke.CanonicalModel.instSemanticsFormulaWorld
{α : Type u}
{Λ : LO.Modal.Standard.DeductionParameter α}
[Nonempty (Λ)-MCT]
:
Equations
- LO.Modal.Standard.Kripke.CanonicalModel.instSemanticsFormulaWorld = LO.Modal.Standard.Formula.Kripke.Satisfies.semantics
theorem
LO.Modal.Standard.Kripke.truthlemma
{α : Type u}
[DecidableEq α]
{Λ : LO.Modal.Standard.DeductionParameter α}
[Λ.IsNormal]
[Nonempty (Λ)-MCT]
{p : LO.Modal.Standard.Formula α}
{Ω : (LO.Modal.Standard.Kripke.CanonicalModel Λ).World}
:
theorem
LO.Modal.Standard.Kripke.iff_valid_on_canonicalModel_deducible
{α : Type u}
[DecidableEq α]
{Λ : LO.Modal.Standard.DeductionParameter α}
[Λ.IsNormal]
[Nonempty (Λ)-MCT]
{p : LO.Modal.Standard.Formula α}
:
LO.Modal.Standard.Kripke.CanonicalModel Λ ⊧ p ↔ Λ ⊢! p
theorem
LO.Modal.Standard.Kripke.realize_axiomset_of_self_canonicalModel
{α : Type u}
[DecidableEq α]
{Λ : LO.Modal.Standard.DeductionParameter α}
[Λ.IsNormal]
[Nonempty (Λ)-MCT]
:
theorem
LO.Modal.Standard.Kripke.realize_theory_of_self_canonicalModel
{α : Type u}
[DecidableEq α]
{Λ : LO.Modal.Standard.DeductionParameter α}
[Λ.IsNormal]
[Nonempty (Λ)-MCT]
:
theorem
LO.Modal.Standard.Kripke.complete_of_mem_canonicalFrame
{α : Type u}
[DecidableEq α]
{Λ : LO.Modal.Standard.DeductionParameter α}
[Λ.IsNormal]
{p : LO.Modal.Standard.Formula α}
[Nonempty (Λ)-MCT]
{𝔽 : LO.Kripke.FrameClass}
(hFC : LO.Modal.Standard.Kripke.CanonicalFrame Λ ∈ 𝔽)
:
instance
LO.Modal.Standard.Kripke.instComplete_of_mem_canonicalFrame
{α : Type u}
[DecidableEq α]
{Λ : LO.Modal.Standard.DeductionParameter α}
[Λ.IsNormal]
[Nonempty (Λ)-MCT]
(𝔽 : LO.Kripke.FrameClass)
(hFC : LO.Modal.Standard.Kripke.CanonicalFrame Λ ∈ 𝔽)
:
LO.Complete Λ 𝔽#α
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯