def
LO.Modal.Standard.Formula.Kripke.Satisfies
{α : Type u_1}
(M : LO.Kripke.Model α)
(x : M.World)
:
Equations
- LO.Modal.Standard.Formula.Kripke.Satisfies M x (LO.Modal.Standard.Formula.atom a) = M.Valuation x a
- LO.Modal.Standard.Formula.Kripke.Satisfies M x LO.Modal.Standard.Formula.falsum = False
- LO.Modal.Standard.Formula.Kripke.Satisfies M x (p.imp q) = LO.Modal.Standard.Formula.Kripke.Satisfies M x p ⟶ LO.Modal.Standard.Formula.Kripke.Satisfies M x q
- LO.Modal.Standard.Formula.Kripke.Satisfies M x p.box = ∀ (y : M.Frame.World), x ≺ y → LO.Modal.Standard.Formula.Kripke.Satisfies M y p
Instances For
instance
LO.Modal.Standard.Formula.Kripke.Satisfies.semantics
{α : Type u_1}
{M : LO.Kripke.Model α}
:
LO.Semantics (LO.Modal.Standard.Formula α) M.World
Equations
- LO.Modal.Standard.Formula.Kripke.Satisfies.semantics = { Realize := fun (x : M.World) => LO.Modal.Standard.Formula.Kripke.Satisfies M x }
@[simp]
theorem
LO.Modal.Standard.Formula.Kripke.Satisfies.iff_models
{α : Type u_1}
{M : LO.Kripke.Model α}
{x : M.World}
{p : LO.Modal.Standard.Formula α}
:
x ⊧ p ↔ LO.Modal.Standard.Formula.Kripke.Satisfies M x p
theorem
LO.Modal.Standard.Formula.Kripke.Satisfies.box_def
{α : Type u_1}
{M : LO.Kripke.Model α}
{x : M.World}
{p : LO.Modal.Standard.Formula α}
:
theorem
LO.Modal.Standard.Formula.Kripke.Satisfies.dia_def
{α : Type u_1}
{M : LO.Kripke.Model α}
{x : M.World}
{p : LO.Modal.Standard.Formula α}
:
theorem
LO.Modal.Standard.Formula.Kripke.Satisfies.not_def
{α : Type u_1}
{M : LO.Kripke.Model α}
{x : M.World}
{p : LO.Modal.Standard.Formula α}
:
instance
LO.Modal.Standard.Formula.Kripke.Satisfies.instNotWorld
{α : Type u_1}
{M : LO.Kripke.Model α}
:
LO.Semantics.Not M.World
Equations
- LO.Modal.Standard.Formula.Kripke.Satisfies.instNotWorld = { realize_not := ⋯ }
theorem
LO.Modal.Standard.Formula.Kripke.Satisfies.imp_def
{α : Type u_1}
{M : LO.Kripke.Model α}
{x : M.World}
{p : LO.Modal.Standard.Formula α}
{q : LO.Modal.Standard.Formula α}
:
instance
LO.Modal.Standard.Formula.Kripke.Satisfies.instImpWorld
{α : Type u_1}
{M : LO.Kripke.Model α}
:
LO.Semantics.Imp M.World
Equations
- LO.Modal.Standard.Formula.Kripke.Satisfies.instImpWorld = { realize_imp := ⋯ }
theorem
LO.Modal.Standard.Formula.Kripke.Satisfies.or_def
{α : Type u_1}
{M : LO.Kripke.Model α}
{x : M.World}
{p : LO.Modal.Standard.Formula α}
{q : LO.Modal.Standard.Formula α}
:
instance
LO.Modal.Standard.Formula.Kripke.Satisfies.instOrWorld
{α : Type u_1}
{M : LO.Kripke.Model α}
:
LO.Semantics.Or M.World
Equations
- LO.Modal.Standard.Formula.Kripke.Satisfies.instOrWorld = { realize_or := ⋯ }
theorem
LO.Modal.Standard.Formula.Kripke.Satisfies.and_def
{α : Type u_1}
{M : LO.Kripke.Model α}
{x : M.World}
{p : LO.Modal.Standard.Formula α}
{q : LO.Modal.Standard.Formula α}
:
instance
LO.Modal.Standard.Formula.Kripke.Satisfies.instAndWorld
{α : Type u_1}
{M : LO.Kripke.Model α}
:
LO.Semantics.And M.World
Equations
- LO.Modal.Standard.Formula.Kripke.Satisfies.instAndWorld = { realize_and := ⋯ }
instance
LO.Modal.Standard.Formula.Kripke.Satisfies.instTarskiWorld
{α : Type u_1}
{M : LO.Kripke.Model α}
:
LO.Semantics.Tarski M.World
Equations
- LO.Modal.Standard.Formula.Kripke.Satisfies.instTarskiWorld = LO.Semantics.Tarski.mk
theorem
LO.Modal.Standard.Formula.Kripke.Satisfies.negneg_def
{α : Type u_1}
{M : LO.Kripke.Model α}
{x : M.World}
{p : LO.Modal.Standard.Formula α}
:
theorem
LO.Modal.Standard.Formula.Kripke.Satisfies.multibox_def
{α : Type u_1}
{M : LO.Kripke.Model α}
{x : M.World}
{p : LO.Modal.Standard.Formula α}
{n : ℕ}
:
theorem
LO.Modal.Standard.Formula.Kripke.Satisfies.multidia_def
{α : Type u_1}
{M : LO.Kripke.Model α}
{x : M.World}
{p : LO.Modal.Standard.Formula α}
{n : ℕ}
:
theorem
LO.Modal.Standard.Formula.Kripke.Satisfies.trans
{α : Type u_1}
{M : LO.Kripke.Model α}
{x : M.World}
{p : LO.Modal.Standard.Formula α}
{q : LO.Modal.Standard.Formula α}
{r : LO.Modal.Standard.Formula α}
(hpq : x ⊧ p ⟶ q)
(hqr : x ⊧ q ⟶ r)
:
theorem
LO.Modal.Standard.Formula.Kripke.Satisfies.mdp
{α : Type u_1}
{M : LO.Kripke.Model α}
{x : M.World}
{p : LO.Modal.Standard.Formula α}
{q : LO.Modal.Standard.Formula α}
(hpq : x ⊧ p ⟶ q)
(hp : x ⊧ p)
:
x ⊧ q
theorem
LO.Modal.Standard.Formula.Kripke.Satisfies.dia_dual
{α : Type u_1}
{M : LO.Kripke.Model α}
{x : M.World}
{p : LO.Modal.Standard.Formula α}
:
theorem
LO.Modal.Standard.Formula.Kripke.Satisfies.box_dual
{α : Type u_1}
{M : LO.Kripke.Model α}
{x : M.World}
{p : LO.Modal.Standard.Formula α}
:
theorem
LO.Modal.Standard.Formula.Kripke.Satisfies.not_imp
{α : Type u_1}
{M : LO.Kripke.Model α}
{x : M.World}
{p : LO.Modal.Standard.Formula α}
{q : LO.Modal.Standard.Formula α}
:
def
LO.Modal.Standard.Formula.Kripke.ValidOnModel
{α : Type u_1}
(M : LO.Kripke.Model α)
(p : LO.Modal.Standard.Formula α)
:
Equations
- LO.Modal.Standard.Formula.Kripke.ValidOnModel M p = ∀ (x : M.World), x ⊧ p
Instances For
Equations
- LO.Modal.Standard.Formula.Kripke.ValidOnModel.semantics = { Realize := fun (M : LO.Kripke.Model α) => LO.Modal.Standard.Formula.Kripke.ValidOnModel M }
@[simp]
theorem
LO.Modal.Standard.Formula.Kripke.ValidOnModel.iff_models
{α : Type u_1}
{f : LO.Modal.Standard.Formula α}
{M : LO.Kripke.Model α}
:
Equations
- LO.Modal.Standard.Formula.Kripke.ValidOnModel.instBotModel = { realize_bot := ⋯ }
theorem
LO.Modal.Standard.Formula.Kripke.ValidOnModel.mdp
{α : Type u_1}
{M : LO.Kripke.Model α}
{p : LO.Modal.Standard.Formula α}
{q : LO.Modal.Standard.Formula α}
(hpq : M ⊧ p ⟶ q)
(hp : M ⊧ p)
:
M ⊧ q
theorem
LO.Modal.Standard.Formula.Kripke.ValidOnModel.nec
{α : Type u_1}
{M : LO.Kripke.Model α}
{p : LO.Modal.Standard.Formula α}
(h : M ⊧ p)
:
theorem
LO.Modal.Standard.Formula.Kripke.ValidOnModel.verum
{α : Type u_1}
{M : LO.Kripke.Model α}
:
theorem
LO.Modal.Standard.Formula.Kripke.ValidOnModel.imply₁
{α : Type u_1}
{M : LO.Kripke.Model α}
{p : LO.Modal.Standard.Formula α}
{q : LO.Modal.Standard.Formula α}
:
M ⊧ LO.Axioms.Imply₁ p q
theorem
LO.Modal.Standard.Formula.Kripke.ValidOnModel.imply₂
{α : Type u_1}
{M : LO.Kripke.Model α}
{p : LO.Modal.Standard.Formula α}
{q : LO.Modal.Standard.Formula α}
{r : LO.Modal.Standard.Formula α}
:
M ⊧ LO.Axioms.Imply₂ p q r
theorem
LO.Modal.Standard.Formula.Kripke.ValidOnModel.elimContra
{α : Type u_1}
{M : LO.Kripke.Model α}
{p : LO.Modal.Standard.Formula α}
{q : LO.Modal.Standard.Formula α}
:
M ⊧ LO.Axioms.ElimContra p q
theorem
LO.Modal.Standard.Formula.Kripke.ValidOnModel.axiomK
{α : Type u_1}
{M : LO.Kripke.Model α}
{p : LO.Modal.Standard.Formula α}
{q : LO.Modal.Standard.Formula α}
:
M ⊧ LO.Axioms.K p q
def
LO.Modal.Standard.Formula.Kripke.ValidOnFrame
{α : Type u_1}
(F : LO.Kripke.Frame)
(p : LO.Modal.Standard.Formula α)
:
Equations
- LO.Modal.Standard.Formula.Kripke.ValidOnFrame F p = ∀ (V : LO.Kripke.Valuation F α), { Frame := F, Valuation := V } ⊧ p
Instances For
Equations
- LO.Modal.Standard.Formula.Kripke.ValidOnFrame.semantics = { Realize := fun (F : LO.Kripke.Frame.Dep α) => LO.Modal.Standard.Formula.Kripke.ValidOnFrame F }
@[simp]
theorem
LO.Modal.Standard.Formula.Kripke.ValidOnFrame.models_iff
{α : Type u_1}
{F : LO.Kripke.Frame.Dep α}
{p : LO.Modal.Standard.Formula α}
:
Equations
- LO.Modal.Standard.Formula.Kripke.ValidOnFrame.instBotDep = { realize_bot := ⋯ }
theorem
LO.Modal.Standard.Formula.Kripke.ValidOnFrame.nec
{α : Type u_1}
{F : LO.Kripke.Frame.Dep α}
{p : LO.Modal.Standard.Formula α}
(h : F ⊧ p)
:
theorem
LO.Modal.Standard.Formula.Kripke.ValidOnFrame.mdp
{α : Type u_1}
{F : LO.Kripke.Frame.Dep α}
{p : LO.Modal.Standard.Formula α}
{q : LO.Modal.Standard.Formula α}
(hpq : F ⊧ p ⟶ q)
(hp : F ⊧ p)
:
F ⊧ q
theorem
LO.Modal.Standard.Formula.Kripke.ValidOnFrame.verum
{α : Type u_1}
{F : LO.Kripke.Frame.Dep α}
:
theorem
LO.Modal.Standard.Formula.Kripke.ValidOnFrame.imply₁
{α : Type u_1}
{F : LO.Kripke.Frame.Dep α}
{p : LO.Modal.Standard.Formula α}
{q : LO.Modal.Standard.Formula α}
:
F ⊧ LO.Axioms.Imply₁ p q
theorem
LO.Modal.Standard.Formula.Kripke.ValidOnFrame.imply₂
{α : Type u_1}
{F : LO.Kripke.Frame.Dep α}
{p : LO.Modal.Standard.Formula α}
{q : LO.Modal.Standard.Formula α}
{r : LO.Modal.Standard.Formula α}
:
F ⊧ LO.Axioms.Imply₂ p q r
theorem
LO.Modal.Standard.Formula.Kripke.ValidOnFrame.elimContra
{α : Type u_1}
{F : LO.Kripke.Frame.Dep α}
{p : LO.Modal.Standard.Formula α}
{q : LO.Modal.Standard.Formula α}
:
F ⊧ LO.Axioms.ElimContra p q
theorem
LO.Modal.Standard.Formula.Kripke.ValidOnFrame.axiomK
{α : Type u_1}
{F : LO.Kripke.Frame.Dep α}
{p : LO.Modal.Standard.Formula α}
{q : LO.Modal.Standard.Formula α}
:
F ⊧ LO.Axioms.K p q
theorem
LO.Modal.Standard.Formula.Kripke.ValidOnFrame.axiomK_set
{α : Type u_2}
{F : LO.Kripke.Frame.Dep α}
:
def
LO.Modal.Standard.Formula.Kripke.ValidOnFrameClass
{α : Type u_1}
(𝔽 : LO.Kripke.FrameClass)
(p : LO.Modal.Standard.Formula α)
:
Equations
- LO.Modal.Standard.Formula.Kripke.ValidOnFrameClass 𝔽 p = ∀ {F : LO.Kripke.Frame}, F ∈ 𝔽 → F#α ⊧ p
Instances For
Equations
- LO.Modal.Standard.Formula.Kripke.ValidOnFrameClass.semantics = { Realize := fun (𝔽 : LO.Kripke.FrameClass.Dep α) => LO.Modal.Standard.Formula.Kripke.ValidOnFrameClass 𝔽 }
@[simp]
theorem
LO.Modal.Standard.Formula.Kripke.ValidOnFrameClass.models_iff
{α : Type u_1}
{𝔽 : LO.Kripke.FrameClass.Dep α}
{p : LO.Modal.Standard.Formula α}
:
theorem
LO.Modal.Standard.Formula.Kripke.ValidOnFrameClass.nec
{α : Type u_1}
{𝔽 : LO.Kripke.FrameClass.Dep α}
{p : LO.Modal.Standard.Formula α}
(h : 𝔽 ⊧ p)
:
theorem
LO.Modal.Standard.Formula.Kripke.ValidOnFrameClass.mdp
{α : Type u_1}
{𝔽 : LO.Kripke.FrameClass.Dep α}
{p : LO.Modal.Standard.Formula α}
{q : LO.Modal.Standard.Formula α}
(hpq : 𝔽 ⊧ p ⟶ q)
(hp : 𝔽 ⊧ p)
:
𝔽 ⊧ q
@[reducible, inline]
abbrev
LO.Modal.Standard.Formula.Kripke.ValidOnFiniteFrameClass
{α : Type u_1}
(𝔽 : LO.Kripke.FiniteFrameClass)
(p : LO.Modal.Standard.Formula α)
:
Equations
- LO.Modal.Standard.Formula.Kripke.ValidOnFiniteFrameClass 𝔽 p = (𝔽.toFrameClass#α ⊧ p)
Instances For
Equations
- One or more equations did not get rendered due to their size.
@[simp]
theorem
LO.Modal.Standard.Formula.Kripke.ValidOnFiniteFrameClass.models_iff
{α : Type u_1}
{𝔽 : LO.Kripke.FiniteFrameClass.Dep α}
{p : LO.Modal.Standard.Formula α}
:
theorem
LO.Modal.Standard.Kripke.nec
{α : Type u_1}
{𝔽 : LO.Kripke.FrameClass}
{p : LO.Modal.Standard.Formula α}
(h : 𝔽#α ⊧ p)
:
theorem
LO.Modal.Standard.Kripke.mdp
{α : Type u_1}
{𝔽 : LO.Kripke.FrameClass}
{p : LO.Modal.Standard.Formula α}
{q : LO.Modal.Standard.Formula α}
(hpq : 𝔽#α ⊧ p ⟶ q)
(hp : 𝔽#α ⊧ p)
:
theorem
LO.Modal.Standard.Kripke.iff_not_validOnFrameClass
{α : Type u_1}
{𝔽 : LO.Kripke.FrameClass}
{p : LO.Modal.Standard.Formula α}
:
¬𝔽#α ⊧ p ↔ ∃ F ∈ 𝔽,
∃ (V : LO.Kripke.Valuation F α) (x : { Frame := F, Valuation := V }.World),
¬LO.Modal.Standard.Formula.Kripke.Satisfies { Frame := F, Valuation := V } x p
theorem
LO.Modal.Standard.Kripke.iff_not_set_validOnFrameClass
{α : Type u_1}
{𝔽 : LO.Kripke.FrameClass}
{T : Set (LO.Modal.Standard.Formula α)}
:
¬𝔽#α ⊧* T ↔ ∃ p ∈ T,
∃ F ∈ 𝔽,
∃ (V : LO.Kripke.Valuation F α) (x : { Frame := F, Valuation := V }.World),
¬LO.Modal.Standard.Formula.Kripke.Satisfies { Frame := F, Valuation := V } x p
theorem
LO.Modal.Standard.Kripke.iff_not_validOnFrame
{α : Type u_1}
{F : LO.Kripke.Frame}
{T : Set (LO.Modal.Standard.Formula α)}
:
¬F#α ⊧* T ↔ ∃ p ∈ T,
∃ (V : LO.Kripke.Valuation F α) (x : { Frame := F, Valuation := V }.World),
¬LO.Modal.Standard.Formula.Kripke.Satisfies { Frame := F, Valuation := V } x p
@[reducible, inline]
abbrev
LO.Modal.Standard.Kripke.FrameClassOfTheory
{α : Type u_1}
(T : LO.Modal.Standard.Theory α)
:
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[reducible, inline]
abbrev
LO.Modal.Standard.Kripke.FiniteFrameClassOfTheory
{α : Type u_1}
(T : LO.Modal.Standard.Theory α)
:
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
def
LO.Modal.Standard.Kripke.definability_union_frameclass_of_theory
{α : Type u_1}
{𝔽₁ : LO.Kripke.FrameClass}
{𝔽₂ : LO.Kripke.FrameClass}
{T₁ : LO.Modal.Standard.Theory α}
{T₂ : LO.Modal.Standard.Theory α}
(defi₁ : 𝔽(T₁).DefinedBy 𝔽₁)
(defi₂ : 𝔽(T₂).DefinedBy 𝔽₂)
(nonempty : Set.Nonempty (𝔽₁ ∩ 𝔽₂))
:
Equations
- LO.Modal.Standard.Kripke.definability_union_frameclass_of_theory defi₁ defi₂ nonempty = { define := ⋯, nonempty := nonempty }
Instances For
def
LO.Modal.Standard.Kripke.characterizability_union_frameclass_of_theory
{α : Type u_1}
{𝔽₁ : LO.Kripke.FrameClass}
{𝔽₂ : LO.Kripke.FrameClass}
{T₁ : LO.Modal.Standard.Theory α}
{T₂ : LO.Modal.Standard.Theory α}
(char₁ : 𝔽(T₁).Characteraizable 𝔽₁)
(char₂ : 𝔽(T₂).Characteraizable 𝔽₂)
(nonempty : Set.Nonempty (𝔽₁ ∩ 𝔽₂))
:
Equations
- LO.Modal.Standard.Kripke.characterizability_union_frameclass_of_theory char₁ char₂ nonempty = { characterize := ⋯, nonempty := nonempty }
Instances For
@[reducible, inline]
abbrev
LO.Modal.Standard.Kripke.FrameClassOfHilbert
{α : Type u_1}
(Λ : LO.Modal.Standard.DeductionParameter α)
:
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
instance
LO.Modal.Standard.Kripke.instDefinedByFrameClassOfHilbertNormalOfFrameClassOfTheory
{α : Type u_1}
{Ax : Set (LO.Modal.Standard.Formula α)}
{𝔽 : LO.Kripke.FrameClass}
[defi : 𝔽(Ax).DefinedBy 𝔽]
:
Equations
- LO.Modal.Standard.Kripke.instDefinedByFrameClassOfHilbertNormalOfFrameClassOfTheory = { define := ⋯, nonempty := ⋯ }
instance
LO.Modal.Standard.Kripke.instCharacteraizableFrameClassOfHilbertNormalOfFrameClassOfTheory
{α : Type u_1}
{Ax : Set (LO.Modal.Standard.Formula α)}
{𝔽 : LO.Kripke.FrameClass}
[char : 𝔽(Ax).Characteraizable 𝔽]
:
Equations
- LO.Modal.Standard.Kripke.instCharacteraizableFrameClassOfHilbertNormalOfFrameClassOfTheory = { characterize := ⋯, nonempty := ⋯ }
@[reducible, inline]
abbrev
LO.Modal.Standard.Kripke.FiniteFrameClassOfHilbert
{α : Type u_1}
(Λ : LO.Modal.Standard.DeductionParameter α)
:
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
instance
LO.Modal.Standard.Kripke.instDefinedByFiniteFrameClassOfHilbertNormalOfFiniteFrameClassOfTheory
{α : Type u_1}
{Ax : Set (LO.Modal.Standard.Formula α)}
{𝔽 : LO.Kripke.FiniteFrameClass}
[defi : 𝔽ꟳ(Ax).DefinedBy 𝔽]
:
Equations
- LO.Modal.Standard.Kripke.instDefinedByFiniteFrameClassOfHilbertNormalOfFiniteFrameClassOfTheory = { define := ⋯, nonempty := ⋯ }
instance
LO.Modal.Standard.Kripke.instCharacteraizableFiniteFrameClassOfHilbertNormalOfFiniteFrameClassOfTheory
{α : Type u_1}
{Ax : Set (LO.Modal.Standard.Formula α)}
{𝔽 : LO.Kripke.FiniteFrameClass}
[char : 𝔽ꟳ(Ax).Characteraizable 𝔽]
:
Equations
- LO.Modal.Standard.Kripke.instCharacteraizableFiniteFrameClassOfHilbertNormalOfFiniteFrameClassOfTheory = { characterize := ⋯, nonempty := ⋯ }
theorem
LO.Modal.Standard.Kripke.sound
{α : Type u}
{Λ : LO.Modal.Standard.DeductionParameter α}
{p : LO.Modal.Standard.Formula α}
:
instance
LO.Modal.Standard.Kripke.instSoundDeductionParameterFormulaDepFrameClassOfHilbert
{α : Type u}
{Λ : LO.Modal.Standard.DeductionParameter α}
:
Equations
- ⋯ = ⋯
theorem
LO.Modal.Standard.Kripke.sound_finite
{α : Type u}
{Λ : LO.Modal.Standard.DeductionParameter α}
{p : LO.Modal.Standard.Formula α}
:
instance
LO.Modal.Standard.Kripke.instSoundDeductionParameterFormulaDepFiniteFrameClassOfHilbert
{α : Type u}
{Λ : LO.Modal.Standard.DeductionParameter α}
:
Equations
- ⋯ = ⋯
theorem
LO.Modal.Standard.Kripke.unprovable_bot
{α : Type u}
{Λ : LO.Modal.Standard.DeductionParameter α}
(hc : Set.Nonempty 𝔽(Λ))
:
instance
LO.Modal.Standard.Kripke.instConsistentFormulaDeductionParameterOfNonemptyFrameFrameClassOfHilbert
{α : Type u}
{Λ : LO.Modal.Standard.DeductionParameter α}
(hc : Set.Nonempty 𝔽(Λ))
:
Equations
- ⋯ = ⋯
theorem
LO.Modal.Standard.Kripke.unprovable_bot_finite
{α : Type u}
{Λ : LO.Modal.Standard.DeductionParameter α}
(hc : Set.Nonempty 𝔽ꟳ(Λ))
:
instance
LO.Modal.Standard.Kripke.instConsistentFormulaDeductionParameterOfNonemptyFiniteFrameFiniteFrameClassOfHilbert
{α : Type u}
{Λ : LO.Modal.Standard.DeductionParameter α}
(hc : Set.Nonempty 𝔽ꟳ(Λ))
:
Equations
- ⋯ = ⋯
theorem
LO.Modal.Standard.Kripke.sound_of_characterizability
{α : Type u}
{Λ : LO.Modal.Standard.DeductionParameter α}
{p : LO.Modal.Standard.Formula α}
{𝔽 : LO.Kripke.FrameClass}
[char : LO.Kripke.FrameClass.Characteraizable 𝔽(Λ) 𝔽]
:
instance
LO.Modal.Standard.Kripke.instSoundDeductionParameterFormulaDepAltOfCharacteraizableFrameClassOfHilbert
{α : Type u}
{Λ : LO.Modal.Standard.DeductionParameter α}
{𝔽 : LO.Kripke.FrameClass}
[LO.Kripke.FrameClass.Characteraizable 𝔽(Λ) 𝔽]
:
Equations
- ⋯ = ⋯
theorem
LO.Modal.Standard.Kripke.sound_of_finite_characterizability
{α : Type u}
{Λ : LO.Modal.Standard.DeductionParameter α}
{p : LO.Modal.Standard.Formula α}
{𝔽 : LO.Kripke.FiniteFrameClass}
[char : LO.Kripke.FiniteFrameClass.Characteraizable 𝔽ꟳ(Λ) 𝔽]
:
instance
LO.Modal.Standard.Kripke.instSoundDeductionParameterFormulaDepAltOfCharacteraizableFiniteFrameClassOfHilbert
{α : Type u}
{Λ : LO.Modal.Standard.DeductionParameter α}
{𝔽 : LO.Kripke.FiniteFrameClass}
[LO.Kripke.FiniteFrameClass.Characteraizable 𝔽ꟳ(Λ) 𝔽]
:
Equations
- ⋯ = ⋯
theorem
LO.Modal.Standard.Kripke.unprovable_bot_of_characterizability
{α : Type u}
{Λ : LO.Modal.Standard.DeductionParameter α}
{𝔽 : LO.Kripke.FrameClass}
[char : LO.Kripke.FrameClass.Characteraizable 𝔽(Λ) 𝔽]
:
instance
LO.Modal.Standard.Kripke.instConsistentFormulaDeductionParameterOfCharacteraizableFrameClassOfHilbert
{𝔽 : LO.Kripke.FrameClass}
{α : Type u}
{Λ : LO.Modal.Standard.DeductionParameter α}
[LO.Kripke.FrameClass.Characteraizable 𝔽(Λ) 𝔽]
:
Equations
- ⋯ = ⋯
theorem
LO.Modal.Standard.Kripke.unprovable_bot_of_finite_characterizability
{α : Type u}
{Λ : LO.Modal.Standard.DeductionParameter α}
{𝔽 : LO.Kripke.FiniteFrameClass}
[char : LO.Kripke.FiniteFrameClass.Characteraizable 𝔽ꟳ(Λ) 𝔽]
:
instance
LO.Modal.Standard.Kripke.instConsistentFormulaDeductionParameterOfCharacteraizableFiniteFrameClassOfHilbert
{α : Type u}
{Λ : LO.Modal.Standard.DeductionParameter α}
{𝔽 : LO.Kripke.FiniteFrameClass}
[LO.Kripke.FiniteFrameClass.Characteraizable 𝔽ꟳ(Λ) 𝔽]
:
Equations
- ⋯ = ⋯
instance
LO.Modal.Standard.Kripke.empty_axiom_definability
{α : Type u_1}
:
𝔽(∅).DefinedBy LO.Kripke.AllFrameClass
Equations
- LO.Modal.Standard.Kripke.empty_axiom_definability = { define := ⋯, nonempty := LO.Modal.Standard.Kripke.empty_axiom_definability.proof_2 }
Equations
- LO.Modal.Standard.Kripke.K_definability = ⋯.mpr LO.Modal.Standard.Kripke.K_definability'
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
theorem
LO.Modal.Standard.Kripke.restrict_finite
{α : Type u_1}
{𝔽 : LO.Kripke.FrameClass}
{p : LO.Modal.Standard.Formula α}
:
instance
LO.Modal.Standard.Kripke.instSoundDeductionParameterFormulaDepAltToFiniteFrameClassOfDepAlt
{α : Type u_1}
{𝔽 : LO.Kripke.FrameClass}
{Λ : LO.Modal.Standard.DeductionParameter α}
[sound : LO.Sound Λ 𝔽#α]
:
Equations
- ⋯ = ⋯
instance
LO.Modal.Standard.Kripke.instSoundDeductionParameterFormulaDepKAltToFiniteFrameClassAllFrameClass
{α : Type u_1}
:
Equations
- ⋯ = ⋯
theorem
LO.Modal.Standard.Kripke.exists_finite_frame
{α : Type u_1}
{𝔽 : LO.Kripke.FrameClass}
{p : LO.Modal.Standard.Formula α}
:
class
LO.Modal.Standard.Kripke.FiniteFrameProperty
{α : Type u_1}
(Λ : LO.Modal.Standard.DeductionParameter α)
(𝔽 : LO.Kripke.FrameClass)
:
- complete : LO.Complete Λ 𝔽ꟳ#α
Instances
theorem
LO.Modal.Standard.Kripke.FiniteFrameProperty.complete
{α : Type u_1}
{Λ : LO.Modal.Standard.DeductionParameter α}
{𝔽 : LO.Kripke.FrameClass}
[self : LO.Modal.Standard.Kripke.FiniteFrameProperty Λ 𝔽]
:
LO.Complete Λ 𝔽ꟳ#α
theorem
LO.Modal.Standard.Kripke.FiniteFrameProperty.sound
{α : Type u_1}
{Λ : LO.Modal.Standard.DeductionParameter α}
{𝔽 : LO.Kripke.FrameClass}
[self : LO.Modal.Standard.Kripke.FiniteFrameProperty Λ 𝔽]
:
theorem
LO.Modal.Standard.Kripke.K_strictlyWeakerThan_KD
{α : Type u_1}
[Inhabited α]
[DecidableEq α]
:
theorem
LO.Modal.Standard.Kripke.K_strictlyWeakerThan_K4
{α : Type u_1}
[Inhabited α]
[DecidableEq α]
:
theorem
LO.Modal.Standard.Kripke.K_strictlyWeakerThan_KB
{α : Type u_1}
[Inhabited α]
[DecidableEq α]
:
theorem
LO.Modal.Standard.Kripke.K_strictlyWeakerThan_K5
{α : Type u_1}
[Inhabited α]
[DecidableEq α]
: