def
LO.Modal.Formula.Kripke.Satisfies
{α : Type u_1}
(M : LO.Kripke.Model α)
(x : M.World)
:
LO.Modal.Formula α → Prop
Equations
- LO.Modal.Formula.Kripke.Satisfies M x (LO.Modal.Formula.atom a) = M.Valuation x a
- LO.Modal.Formula.Kripke.Satisfies M x LO.Modal.Formula.falsum = False
- LO.Modal.Formula.Kripke.Satisfies M x (p.imp q) = LO.Modal.Formula.Kripke.Satisfies M x p ➝ LO.Modal.Formula.Kripke.Satisfies M x q
- LO.Modal.Formula.Kripke.Satisfies M x p.box = ∀ (y : M.Frame.World), x ≺ y → LO.Modal.Formula.Kripke.Satisfies M y p
Instances For
instance
LO.Modal.Formula.Kripke.Satisfies.semantics
{α : Type u_1}
{M : LO.Kripke.Model α}
:
LO.Semantics (LO.Modal.Formula α) M.World
Equations
- LO.Modal.Formula.Kripke.Satisfies.semantics = { Realize := fun (x : M.World) => LO.Modal.Formula.Kripke.Satisfies M x }
@[simp]
theorem
LO.Modal.Formula.Kripke.Satisfies.iff_models
{α : Type u_1}
{M : LO.Kripke.Model α}
{x : M.World}
{p : LO.Modal.Formula α}
:
x ⊧ p ↔ LO.Modal.Formula.Kripke.Satisfies M x p
theorem
LO.Modal.Formula.Kripke.Satisfies.box_def
{α : Type u_1}
{M : LO.Kripke.Model α}
{x : M.World}
{p : LO.Modal.Formula α}
:
theorem
LO.Modal.Formula.Kripke.Satisfies.dia_def
{α : Type u_1}
{M : LO.Kripke.Model α}
{x : M.World}
{p : LO.Modal.Formula α}
:
theorem
LO.Modal.Formula.Kripke.Satisfies.not_def
{α : Type u_1}
{M : LO.Kripke.Model α}
{x : M.World}
{p : LO.Modal.Formula α}
:
instance
LO.Modal.Formula.Kripke.Satisfies.instNotWorld
{α : Type u_1}
{M : LO.Kripke.Model α}
:
LO.Semantics.Not M.World
Equations
- LO.Modal.Formula.Kripke.Satisfies.instNotWorld = { realize_not := ⋯ }
theorem
LO.Modal.Formula.Kripke.Satisfies.imp_def
{α : Type u_1}
{M : LO.Kripke.Model α}
{x : M.World}
{p : LO.Modal.Formula α}
{q : LO.Modal.Formula α}
:
instance
LO.Modal.Formula.Kripke.Satisfies.instImpWorld
{α : Type u_1}
{M : LO.Kripke.Model α}
:
LO.Semantics.Imp M.World
Equations
- LO.Modal.Formula.Kripke.Satisfies.instImpWorld = { realize_imp := ⋯ }
theorem
LO.Modal.Formula.Kripke.Satisfies.or_def
{α : Type u_1}
{M : LO.Kripke.Model α}
{x : M.World}
{p : LO.Modal.Formula α}
{q : LO.Modal.Formula α}
:
instance
LO.Modal.Formula.Kripke.Satisfies.instOrWorld
{α : Type u_1}
{M : LO.Kripke.Model α}
:
LO.Semantics.Or M.World
Equations
- LO.Modal.Formula.Kripke.Satisfies.instOrWorld = { realize_or := ⋯ }
theorem
LO.Modal.Formula.Kripke.Satisfies.and_def
{α : Type u_1}
{M : LO.Kripke.Model α}
{x : M.World}
{p : LO.Modal.Formula α}
{q : LO.Modal.Formula α}
:
instance
LO.Modal.Formula.Kripke.Satisfies.instAndWorld
{α : Type u_1}
{M : LO.Kripke.Model α}
:
LO.Semantics.And M.World
Equations
- LO.Modal.Formula.Kripke.Satisfies.instAndWorld = { realize_and := ⋯ }
instance
LO.Modal.Formula.Kripke.Satisfies.instTarskiWorld
{α : Type u_1}
{M : LO.Kripke.Model α}
:
LO.Semantics.Tarski M.World
Equations
- LO.Modal.Formula.Kripke.Satisfies.instTarskiWorld = LO.Semantics.Tarski.mk
theorem
LO.Modal.Formula.Kripke.Satisfies.negneg_def
{α : Type u_1}
{M : LO.Kripke.Model α}
{x : M.World}
{p : LO.Modal.Formula α}
:
theorem
LO.Modal.Formula.Kripke.Satisfies.multibox_def
{α : Type u_1}
{M : LO.Kripke.Model α}
{x : M.World}
{p : LO.Modal.Formula α}
{n : ℕ}
:
theorem
LO.Modal.Formula.Kripke.Satisfies.multidia_def
{α : Type u_1}
{M : LO.Kripke.Model α}
{x : M.World}
{p : LO.Modal.Formula α}
{n : ℕ}
:
theorem
LO.Modal.Formula.Kripke.Satisfies.trans
{α : Type u_1}
{M : LO.Kripke.Model α}
{x : M.World}
{p : LO.Modal.Formula α}
{q : LO.Modal.Formula α}
{r : LO.Modal.Formula α}
(hpq : x ⊧ p ➝ q)
(hqr : x ⊧ q ➝ r)
:
theorem
LO.Modal.Formula.Kripke.Satisfies.mdp
{α : Type u_1}
{M : LO.Kripke.Model α}
{x : M.World}
{p : LO.Modal.Formula α}
{q : LO.Modal.Formula α}
(hpq : x ⊧ p ➝ q)
(hp : x ⊧ p)
:
x ⊧ q
theorem
LO.Modal.Formula.Kripke.Satisfies.dia_dual
{α : Type u_1}
{M : LO.Kripke.Model α}
{x : M.World}
{p : LO.Modal.Formula α}
:
theorem
LO.Modal.Formula.Kripke.Satisfies.box_dual
{α : Type u_1}
{M : LO.Kripke.Model α}
{x : M.World}
{p : LO.Modal.Formula α}
:
theorem
LO.Modal.Formula.Kripke.Satisfies.not_imp
{α : Type u_1}
{M : LO.Kripke.Model α}
{x : M.World}
{p : LO.Modal.Formula α}
{q : LO.Modal.Formula α}
:
def
LO.Modal.Formula.Kripke.ValidOnModel
{α : Type u_1}
(M : LO.Kripke.Model α)
(p : LO.Modal.Formula α)
:
Equations
- LO.Modal.Formula.Kripke.ValidOnModel M p = ∀ (x : M.World), x ⊧ p
Instances For
Equations
- LO.Modal.Formula.Kripke.ValidOnModel.semantics = { Realize := fun (M : LO.Kripke.Model α) => LO.Modal.Formula.Kripke.ValidOnModel M }
@[simp]
theorem
LO.Modal.Formula.Kripke.ValidOnModel.iff_models
{α : Type u_1}
{f : LO.Modal.Formula α}
{M : LO.Kripke.Model α}
:
M ⊧ f ↔ LO.Modal.Formula.Kripke.ValidOnModel M f
Equations
- LO.Modal.Formula.Kripke.ValidOnModel.instBotModel = { realize_bot := ⋯ }
theorem
LO.Modal.Formula.Kripke.ValidOnModel.mdp
{α : Type u_1}
{M : LO.Kripke.Model α}
{p : LO.Modal.Formula α}
{q : LO.Modal.Formula α}
(hpq : M ⊧ p ➝ q)
(hp : M ⊧ p)
:
M ⊧ q
theorem
LO.Modal.Formula.Kripke.ValidOnModel.nec
{α : Type u_1}
{M : LO.Kripke.Model α}
{p : LO.Modal.Formula α}
(h : M ⊧ p)
:
theorem
LO.Modal.Formula.Kripke.ValidOnModel.imply₁
{α : Type u_1}
{M : LO.Kripke.Model α}
{p : LO.Modal.Formula α}
{q : LO.Modal.Formula α}
:
M ⊧ LO.Axioms.Imply₁ p q
theorem
LO.Modal.Formula.Kripke.ValidOnModel.imply₂
{α : Type u_1}
{M : LO.Kripke.Model α}
{p : LO.Modal.Formula α}
{q : LO.Modal.Formula α}
{r : LO.Modal.Formula α}
:
M ⊧ LO.Axioms.Imply₂ p q r
theorem
LO.Modal.Formula.Kripke.ValidOnModel.elimContra
{α : Type u_1}
{M : LO.Kripke.Model α}
{p : LO.Modal.Formula α}
{q : LO.Modal.Formula α}
:
M ⊧ LO.Axioms.ElimContra p q
theorem
LO.Modal.Formula.Kripke.ValidOnModel.axiomK
{α : Type u_1}
{M : LO.Kripke.Model α}
{p : LO.Modal.Formula α}
{q : LO.Modal.Formula α}
:
M ⊧ LO.Axioms.K p q
def
LO.Modal.Formula.Kripke.ValidOnFrame
{α : Type u_1}
(F : LO.Kripke.Frame)
(p : LO.Modal.Formula α)
:
Equations
- LO.Modal.Formula.Kripke.ValidOnFrame F p = ∀ (V : LO.Kripke.Valuation F α), { Frame := F, Valuation := V } ⊧ p
Instances For
Equations
- LO.Modal.Formula.Kripke.ValidOnFrame.semantics = { Realize := fun (F : LO.Kripke.Frame.Dep α) => LO.Modal.Formula.Kripke.ValidOnFrame F }
@[simp]
theorem
LO.Modal.Formula.Kripke.ValidOnFrame.models_iff
{α : Type u_1}
{F : LO.Kripke.Frame.Dep α}
{p : LO.Modal.Formula α}
:
F ⊧ p ↔ LO.Modal.Formula.Kripke.ValidOnFrame F p
Equations
- LO.Modal.Formula.Kripke.ValidOnFrame.instBotDep = { realize_bot := ⋯ }
theorem
LO.Modal.Formula.Kripke.ValidOnFrame.nec
{α : Type u_1}
{F : LO.Kripke.Frame.Dep α}
{p : LO.Modal.Formula α}
(h : F ⊧ p)
:
theorem
LO.Modal.Formula.Kripke.ValidOnFrame.mdp
{α : Type u_1}
{F : LO.Kripke.Frame.Dep α}
{p : LO.Modal.Formula α}
{q : LO.Modal.Formula α}
(hpq : F ⊧ p ➝ q)
(hp : F ⊧ p)
:
F ⊧ q
theorem
LO.Modal.Formula.Kripke.ValidOnFrame.imply₁
{α : Type u_1}
{F : LO.Kripke.Frame.Dep α}
{p : LO.Modal.Formula α}
{q : LO.Modal.Formula α}
:
F ⊧ LO.Axioms.Imply₁ p q
theorem
LO.Modal.Formula.Kripke.ValidOnFrame.imply₂
{α : Type u_1}
{F : LO.Kripke.Frame.Dep α}
{p : LO.Modal.Formula α}
{q : LO.Modal.Formula α}
{r : LO.Modal.Formula α}
:
F ⊧ LO.Axioms.Imply₂ p q r
theorem
LO.Modal.Formula.Kripke.ValidOnFrame.elimContra
{α : Type u_1}
{F : LO.Kripke.Frame.Dep α}
{p : LO.Modal.Formula α}
{q : LO.Modal.Formula α}
:
F ⊧ LO.Axioms.ElimContra p q
theorem
LO.Modal.Formula.Kripke.ValidOnFrame.axiomK
{α : Type u_1}
{F : LO.Kripke.Frame.Dep α}
{p : LO.Modal.Formula α}
{q : LO.Modal.Formula α}
:
F ⊧ LO.Axioms.K p q
theorem
LO.Modal.Formula.Kripke.ValidOnFrame.axiomK_set
{α : Type u_2}
{F : LO.Kripke.Frame.Dep α}
:
def
LO.Modal.Formula.Kripke.ValidOnFrameClass
{α : Type u_1}
(𝔽 : LO.Kripke.FrameClass)
(p : LO.Modal.Formula α)
:
Equations
- LO.Modal.Formula.Kripke.ValidOnFrameClass 𝔽 p = ∀ {F : LO.Kripke.Frame}, F ∈ 𝔽 → F#α ⊧ p
Instances For
Equations
- LO.Modal.Formula.Kripke.ValidOnFrameClass.semantics = { Realize := fun (𝔽 : LO.Kripke.FrameClass.Dep α) => LO.Modal.Formula.Kripke.ValidOnFrameClass 𝔽 }
@[simp]
theorem
LO.Modal.Formula.Kripke.ValidOnFrameClass.models_iff
{α : Type u_1}
{𝔽 : LO.Kripke.FrameClass.Dep α}
{p : LO.Modal.Formula α}
:
theorem
LO.Modal.Formula.Kripke.ValidOnFrameClass.nec
{α : Type u_1}
{𝔽 : LO.Kripke.FrameClass.Dep α}
{p : LO.Modal.Formula α}
(h : 𝔽 ⊧ p)
:
theorem
LO.Modal.Formula.Kripke.ValidOnFrameClass.mdp
{α : Type u_1}
{𝔽 : LO.Kripke.FrameClass.Dep α}
{p : LO.Modal.Formula α}
{q : LO.Modal.Formula α}
(hpq : 𝔽 ⊧ p ➝ q)
(hp : 𝔽 ⊧ p)
:
𝔽 ⊧ q
@[reducible, inline]
abbrev
LO.Modal.Formula.Kripke.ValidOnFiniteFrameClass
{α : Type u_1}
(𝔽 : LO.Kripke.FiniteFrameClass)
(p : LO.Modal.Formula α)
:
Equations
- LO.Modal.Formula.Kripke.ValidOnFiniteFrameClass 𝔽 p = (𝔽.toFrameClass#α ⊧ p)
Instances For
Equations
- LO.Modal.Formula.Kripke.ValidOnFiniteFrameClass.semantics = { Realize := fun (𝔽 : LO.Kripke.FiniteFrameClass.Dep α) => LO.Modal.Formula.Kripke.ValidOnFiniteFrameClass 𝔽 }
@[simp]
theorem
LO.Modal.Formula.Kripke.ValidOnFiniteFrameClass.models_iff
{α : Type u_1}
{𝔽 : LO.Kripke.FiniteFrameClass.Dep α}
{p : LO.Modal.Formula α}
:
theorem
LO.Modal.Kripke.nec
{α : Type u_1}
{𝔽 : LO.Kripke.FrameClass}
{p : LO.Modal.Formula α}
(h : 𝔽#α ⊧ p)
:
theorem
LO.Modal.Kripke.mdp
{α : Type u_1}
{𝔽 : LO.Kripke.FrameClass}
{p : LO.Modal.Formula α}
{q : LO.Modal.Formula α}
(hpq : 𝔽#α ⊧ p ➝ q)
(hp : 𝔽#α ⊧ p)
:
theorem
LO.Modal.Kripke.iff_not_validOnFrameClass
{α : Type u_1}
{𝔽 : LO.Kripke.FrameClass}
{p : LO.Modal.Formula α}
:
¬𝔽#α ⊧ p ↔ ∃ F ∈ 𝔽,
∃ (V : LO.Kripke.Valuation F α) (x : { Frame := F, Valuation := V }.World),
¬LO.Modal.Formula.Kripke.Satisfies { Frame := F, Valuation := V } x p
theorem
LO.Modal.Kripke.iff_not_set_validOnFrameClass
{α : Type u_1}
{𝔽 : LO.Kripke.FrameClass}
{T : Set (LO.Modal.Formula α)}
:
¬𝔽#α ⊧* T ↔ ∃ p ∈ T,
∃ F ∈ 𝔽,
∃ (V : LO.Kripke.Valuation F α) (x : { Frame := F, Valuation := V }.World),
¬LO.Modal.Formula.Kripke.Satisfies { Frame := F, Valuation := V } x p
theorem
LO.Modal.Kripke.iff_not_validOnFrame
{α : Type u_1}
{F : LO.Kripke.Frame}
{T : Set (LO.Modal.Formula α)}
:
¬F#α ⊧* T ↔ ∃ p ∈ T,
∃ (V : LO.Kripke.Valuation F α) (x : { Frame := F, Valuation := V }.World),
¬LO.Modal.Formula.Kripke.Satisfies { Frame := F, Valuation := V } x p
@[reducible, inline]
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[reducible, inline]
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
def
LO.Modal.Kripke.definability_union_frameclass_of_theory
{α : Type u_1}
{𝔽₁ : LO.Kripke.FrameClass}
{𝔽₂ : LO.Kripke.FrameClass}
{T₁ : LO.Modal.Theory α}
{T₂ : LO.Modal.Theory α}
(defi₁ : 𝔽(T₁).DefinedBy 𝔽₁)
(defi₂ : 𝔽(T₂).DefinedBy 𝔽₂)
(nonempty : Set.Nonempty (𝔽₁ ∩ 𝔽₂))
:
Equations
- LO.Modal.Kripke.definability_union_frameclass_of_theory defi₁ defi₂ nonempty = { define := ⋯, nonempty := nonempty }
Instances For
def
LO.Modal.Kripke.characterizability_union_frameclass_of_theory
{α : Type u_1}
{𝔽₁ : LO.Kripke.FrameClass}
{𝔽₂ : LO.Kripke.FrameClass}
{T₁ : LO.Modal.Theory α}
{T₂ : LO.Modal.Theory α}
(char₁ : 𝔽(T₁).Characteraizable 𝔽₁)
(char₂ : 𝔽(T₂).Characteraizable 𝔽₂)
(nonempty : Set.Nonempty (𝔽₁ ∩ 𝔽₂))
:
Equations
- LO.Modal.Kripke.characterizability_union_frameclass_of_theory char₁ char₂ nonempty = { characterize := ⋯, nonempty := nonempty }
Instances For
@[reducible, inline]
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
instance
LO.Modal.Kripke.instDefinedByFrameClassOfHilbertExtKOfFrameClassOfTheory
{α : Type u_1}
{Ax : LO.Modal.Theory α}
{𝔽 : LO.Kripke.FrameClass}
[defi : 𝔽(Ax).DefinedBy 𝔽]
:
Equations
- LO.Modal.Kripke.instDefinedByFrameClassOfHilbertExtKOfFrameClassOfTheory = { define := ⋯, nonempty := ⋯ }
instance
LO.Modal.Kripke.instCharacteraizableFrameClassOfHilbertExtKOfFrameClassOfTheory
{α : Type u_1}
{Ax : LO.Modal.Theory α}
{𝔽 : LO.Kripke.FrameClass}
[char : 𝔽(Ax).Characteraizable 𝔽]
:
Equations
- LO.Modal.Kripke.instCharacteraizableFrameClassOfHilbertExtKOfFrameClassOfTheory = { characterize := ⋯, nonempty := ⋯ }
@[reducible, inline]
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
instance
LO.Modal.Kripke.instDefinedByFiniteFrameClassOfHilbertExtKOfFiniteFrameClassOfTheory
{α : Type u_1}
{Ax : Set (LO.Modal.Formula α)}
{𝔽 : LO.Kripke.FiniteFrameClass}
[defi : 𝔽ꟳ(Ax).DefinedBy 𝔽]
:
Equations
- LO.Modal.Kripke.instDefinedByFiniteFrameClassOfHilbertExtKOfFiniteFrameClassOfTheory = { define := ⋯, nonempty := ⋯ }
instance
LO.Modal.Kripke.instCharacteraizableFiniteFrameClassOfHilbertExtKOfFiniteFrameClassOfTheory
{α : Type u_1}
{Ax : Set (LO.Modal.Formula α)}
{𝔽 : LO.Kripke.FiniteFrameClass}
[char : 𝔽ꟳ(Ax).Characteraizable 𝔽]
:
Equations
- LO.Modal.Kripke.instCharacteraizableFiniteFrameClassOfHilbertExtKOfFiniteFrameClassOfTheory = { characterize := ⋯, nonempty := ⋯ }
instance
LO.Modal.Kripke.instSoundHilbertFormulaDepFrameClassOfHilbert
{α : Type u}
{Λ : LO.Modal.Hilbert α}
:
Equations
- ⋯ = ⋯
theorem
LO.Modal.Kripke.sound_finite
{α : Type u}
{Λ : LO.Modal.Hilbert α}
{p : LO.Modal.Formula α}
:
instance
LO.Modal.Kripke.instSoundHilbertFormulaDepFiniteFrameClassOfHilbert
{α : Type u}
{Λ : LO.Modal.Hilbert α}
:
Equations
- ⋯ = ⋯
theorem
LO.Modal.Kripke.unprovable_bot
{α : Type u}
{Λ : LO.Modal.Hilbert α}
(hc : Set.Nonempty 𝔽(Λ))
:
instance
LO.Modal.Kripke.instConsistentFormulaHilbertOfNonemptyFrameFrameClassOfHilbert
{α : Type u}
{Λ : LO.Modal.Hilbert α}
(hc : Set.Nonempty 𝔽(Λ))
:
Equations
- ⋯ = ⋯
theorem
LO.Modal.Kripke.unprovable_bot_finite
{α : Type u}
{Λ : LO.Modal.Hilbert α}
(hc : Set.Nonempty 𝔽ꟳ(Λ))
:
instance
LO.Modal.Kripke.instConsistentFormulaHilbertOfNonemptyFiniteFrameFiniteFrameClassOfHilbert
{α : Type u}
{Λ : LO.Modal.Hilbert α}
(hc : Set.Nonempty 𝔽ꟳ(Λ))
:
Equations
- ⋯ = ⋯
theorem
LO.Modal.Kripke.sound_of_characterizability
{α : Type u}
{Λ : LO.Modal.Hilbert α}
{p : LO.Modal.Formula α}
{𝔽 : LO.Kripke.FrameClass}
[char : LO.Kripke.FrameClass.Characteraizable 𝔽(Λ) 𝔽]
:
instance
LO.Modal.Kripke.instSoundHilbertFormulaDepAltOfCharacteraizableFrameClassOfHilbert
{α : Type u}
{Λ : LO.Modal.Hilbert α}
{𝔽 : LO.Kripke.FrameClass}
[LO.Kripke.FrameClass.Characteraizable 𝔽(Λ) 𝔽]
:
Equations
- ⋯ = ⋯
theorem
LO.Modal.Kripke.sound_of_finite_characterizability
{α : Type u}
{Λ : LO.Modal.Hilbert α}
{p : LO.Modal.Formula α}
{𝔽 : LO.Kripke.FiniteFrameClass}
[char : LO.Kripke.FiniteFrameClass.Characteraizable 𝔽ꟳ(Λ) 𝔽]
:
instance
LO.Modal.Kripke.instSoundHilbertFormulaDepAltOfCharacteraizableFiniteFrameClassOfHilbert
{α : Type u}
{Λ : LO.Modal.Hilbert α}
{𝔽 : LO.Kripke.FiniteFrameClass}
[LO.Kripke.FiniteFrameClass.Characteraizable 𝔽ꟳ(Λ) 𝔽]
:
Equations
- ⋯ = ⋯
theorem
LO.Modal.Kripke.unprovable_bot_of_characterizability
{α : Type u}
{Λ : LO.Modal.Hilbert α}
{𝔽 : LO.Kripke.FrameClass}
[char : LO.Kripke.FrameClass.Characteraizable 𝔽(Λ) 𝔽]
:
instance
LO.Modal.Kripke.instConsistentFormulaHilbertOfCharacteraizableFrameClassOfHilbert
{𝔽 : LO.Kripke.FrameClass}
{α : Type u}
{Λ : LO.Modal.Hilbert α}
[LO.Kripke.FrameClass.Characteraizable 𝔽(Λ) 𝔽]
:
Equations
- ⋯ = ⋯
theorem
LO.Modal.Kripke.unprovable_bot_of_finite_characterizability
{α : Type u}
{Λ : LO.Modal.Hilbert α}
{𝔽 : LO.Kripke.FiniteFrameClass}
[char : LO.Kripke.FiniteFrameClass.Characteraizable 𝔽ꟳ(Λ) 𝔽]
:
instance
LO.Modal.Kripke.instConsistentFormulaHilbertOfCharacteraizableFiniteFrameClassOfHilbert
{α : Type u}
{Λ : LO.Modal.Hilbert α}
{𝔽 : LO.Kripke.FiniteFrameClass}
[LO.Kripke.FiniteFrameClass.Characteraizable 𝔽ꟳ(Λ) 𝔽]
:
Equations
- ⋯ = ⋯
instance
LO.Modal.Kripke.empty_axiom_definability
{α : Type u_1}
:
𝔽(∅).DefinedBy LO.Kripke.AllFrameClass
Equations
- LO.Modal.Kripke.empty_axiom_definability = { define := ⋯, nonempty := LO.Modal.Kripke.empty_axiom_definability.proof_2 }
Equations
- LO.Modal.Kripke.K_definability = ⋯.mpr LO.Modal.Kripke.K_definability'
Equations
- ⋯ = ⋯
theorem
LO.Modal.Kripke.restrict_finite
{α : Type u_1}
{𝔽 : LO.Kripke.FrameClass}
{p : LO.Modal.Formula α}
:
instance
LO.Modal.Kripke.instSoundHilbertFormulaDepAltToFiniteFrameClassOfDepAlt
{α : Type u_1}
{𝔽 : LO.Kripke.FrameClass}
{Λ : LO.Modal.Hilbert α}
[sound : LO.Sound Λ 𝔽#α]
:
Equations
- ⋯ = ⋯
instance
LO.Modal.Kripke.instSoundHilbertFormulaDepKAltToFiniteFrameClassAllFrameClass
{α : Type u_1}
:
Equations
- ⋯ = ⋯
theorem
LO.Modal.Kripke.exists_finite_frame
{α : Type u_1}
{𝔽 : LO.Kripke.FrameClass}
{p : LO.Modal.Formula α}
:
class
LO.Modal.Kripke.FiniteFrameProperty
{α : Type u_1}
(Λ : LO.Modal.Hilbert α)
(𝔽 : LO.Kripke.FrameClass)
:
- complete : LO.Complete Λ 𝔽ꟳ#α
Instances
theorem
LO.Modal.Kripke.FiniteFrameProperty.complete
{α : Type u_1}
{Λ : LO.Modal.Hilbert α}
{𝔽 : LO.Kripke.FrameClass}
[self : LO.Modal.Kripke.FiniteFrameProperty Λ 𝔽]
:
LO.Complete Λ 𝔽ꟳ#α
theorem
LO.Modal.Kripke.FiniteFrameProperty.sound
{α : Type u_1}
{Λ : LO.Modal.Hilbert α}
{𝔽 : LO.Kripke.FrameClass}
[self : LO.Modal.Kripke.FiniteFrameProperty Λ 𝔽]
:
theorem
LO.Modal.weakerThan_of_subset_FrameClass
{α : Type u_2}
{Ax₁ : LO.Modal.Theory α}
{Ax₂ : LO.Modal.Theory α}
(𝔽₁ : LO.Kripke.FrameClass)
(𝔽₂ : LO.Kripke.FrameClass)
[sound₁ : LO.Sound (𝜿Ax₁) 𝔽₁#α]
[complete₂ : LO.Complete (𝜿Ax₂) 𝔽₂#α]
(h𝔽 : 𝔽₂ ⊆ 𝔽₁)
:
theorem
LO.Modal.equiv_of_eq_FrameClass
{α : Type u_2}
{Ax₁ : LO.Modal.Theory α}
{Ax₂ : LO.Modal.Theory α}
(𝔽₁ : LO.Kripke.FrameClass)
(𝔽₂ : LO.Kripke.FrameClass)
[sound₁ : LO.Sound (𝜿Ax₁) 𝔽₁#α]
[sound₂ : LO.Sound (𝜿Ax₂) 𝔽₂#α]
[complete₁ : LO.Complete (𝜿Ax₁) 𝔽₁#α]
[complete₂ : LO.Complete (𝜿Ax₂) 𝔽₂#α]
(h𝔽 : 𝔽₁ = 𝔽₂)
: