Equations
- LO.IntProp.Formula.Kripke.Satisfies M w (LO.IntProp.Formula.atom a) = M.Valuation w a
- LO.IntProp.Formula.Kripke.Satisfies M w LO.IntProp.Formula.verum = True
- LO.IntProp.Formula.Kripke.Satisfies M w LO.IntProp.Formula.falsum = False
- LO.IntProp.Formula.Kripke.Satisfies M w (p.and q) = (LO.IntProp.Formula.Kripke.Satisfies M w p ∧ LO.IntProp.Formula.Kripke.Satisfies M w q)
- LO.IntProp.Formula.Kripke.Satisfies M w (p.or q) = (LO.IntProp.Formula.Kripke.Satisfies M w p ∨ LO.IntProp.Formula.Kripke.Satisfies M w q)
- LO.IntProp.Formula.Kripke.Satisfies M w p.neg = ∀ {w' : M.World}, w ≺ w' → ¬LO.IntProp.Formula.Kripke.Satisfies M w' p
- LO.IntProp.Formula.Kripke.Satisfies M w (p.imp q) = ∀ {w' : M.World}, w ≺ w' → LO.IntProp.Formula.Kripke.Satisfies M w' p → LO.IntProp.Formula.Kripke.Satisfies M w' q
Instances For
instance
LO.IntProp.Formula.Kripke.Satisfies.semantics
{α : Type u}
(M : LO.Kripke.Model α)
:
LO.Semantics (LO.IntProp.Formula α) M.World
Equations
- LO.IntProp.Formula.Kripke.Satisfies.semantics M = { Realize := fun (w : M.World) => LO.IntProp.Formula.Kripke.Satisfies M w }
@[simp]
theorem
LO.IntProp.Formula.Kripke.Satisfies.iff_models
{α : Type u}
{M : LO.Kripke.Model α}
{w : M.World}
{p : LO.IntProp.Formula α}
:
w ⊧ p ↔ LO.IntProp.Formula.Kripke.Satisfies M w p
@[simp]
theorem
LO.IntProp.Formula.Kripke.Satisfies.atom_def
{α : Type u}
{M : LO.Kripke.Model α}
{w : M.World}
{a : α}
:
w ⊧ LO.IntProp.Formula.atom a ↔ M.Valuation w a
@[simp]
theorem
LO.IntProp.Formula.Kripke.Satisfies.top_def
{α : Type u}
{M : LO.Kripke.Model α}
{w : M.World}
:
@[simp]
theorem
LO.IntProp.Formula.Kripke.Satisfies.bot_def
{α : Type u}
{M : LO.Kripke.Model α}
{w : M.World}
:
@[simp]
theorem
LO.IntProp.Formula.Kripke.Satisfies.and_def
{α : Type u}
{M : LO.Kripke.Model α}
{w : M.World}
{p : LO.IntProp.Formula α}
{q : LO.IntProp.Formula α}
:
@[simp]
theorem
LO.IntProp.Formula.Kripke.Satisfies.or_def
{α : Type u}
{M : LO.Kripke.Model α}
{w : M.World}
{p : LO.IntProp.Formula α}
{q : LO.IntProp.Formula α}
:
@[simp]
theorem
LO.IntProp.Formula.Kripke.Satisfies.imp_def
{α : Type u}
{M : LO.Kripke.Model α}
{w : M.World}
{p : LO.IntProp.Formula α}
{q : LO.IntProp.Formula α}
:
@[simp]
theorem
LO.IntProp.Formula.Kripke.Satisfies.neg_def
{α : Type u}
{M : LO.Kripke.Model α}
{w : M.World}
{p : LO.IntProp.Formula α}
:
instance
LO.IntProp.Formula.Kripke.Satisfies.instTopWorld
{α : Type u}
{M : LO.Kripke.Model α}
:
LO.Semantics.Top M.World
Equations
- LO.IntProp.Formula.Kripke.Satisfies.instTopWorld = { realize_top := ⋯ }
instance
LO.IntProp.Formula.Kripke.Satisfies.instBotWorld
{α : Type u}
{M : LO.Kripke.Model α}
:
LO.Semantics.Bot M.World
Equations
- LO.IntProp.Formula.Kripke.Satisfies.instBotWorld = { realize_bot := ⋯ }
instance
LO.IntProp.Formula.Kripke.Satisfies.instAndWorld
{α : Type u}
{M : LO.Kripke.Model α}
:
LO.Semantics.And M.World
Equations
- LO.IntProp.Formula.Kripke.Satisfies.instAndWorld = { realize_and := ⋯ }
instance
LO.IntProp.Formula.Kripke.Satisfies.instOrWorld
{α : Type u}
{M : LO.Kripke.Model α}
:
LO.Semantics.Or M.World
Equations
- LO.IntProp.Formula.Kripke.Satisfies.instOrWorld = { realize_or := ⋯ }
theorem
LO.IntProp.Formula.Kripke.Satisfies.formula_hereditary
{α : Type u}
{M : LO.Kripke.Model α}
{w : M.World}
{p : LO.IntProp.Formula α}
{w' : M.Frame.World}
(herditary : M.Valuation.atomic_hereditary)
(F_trans : Transitive M.Frame.Rel)
(hw : w ≺ w')
:
theorem
LO.IntProp.Formula.Kripke.Satisfies.neg_equiv
{α : Type u}
{M : LO.Kripke.Model α}
{w : M.World}
{p : LO.IntProp.Formula α}
:
def
LO.IntProp.Formula.Kripke.ValidOnModel
{α : Type u}
(M : LO.Kripke.Model α)
(p : LO.IntProp.Formula α)
:
Equations
- LO.IntProp.Formula.Kripke.ValidOnModel M p = ∀ (w : M.World), w ⊧ p
Instances For
Equations
- LO.IntProp.Formula.Kripke.ValidOnModel.semantics = { Realize := fun (M : LO.Kripke.Model α) => LO.IntProp.Formula.Kripke.ValidOnModel M }
@[simp]
theorem
LO.IntProp.Formula.Kripke.ValidOnModel.iff_models
{α : Type u}
{M : LO.Kripke.Model α}
{p : LO.IntProp.Formula α}
:
M ⊧ p ↔ LO.IntProp.Formula.Kripke.ValidOnModel M p
theorem
LO.IntProp.Formula.Kripke.ValidOnModel.and₁
{α : Type u}
{M : LO.Kripke.Model α}
{p : LO.IntProp.Formula α}
{q : LO.IntProp.Formula α}
:
theorem
LO.IntProp.Formula.Kripke.ValidOnModel.and₂
{α : Type u}
{M : LO.Kripke.Model α}
{p : LO.IntProp.Formula α}
{q : LO.IntProp.Formula α}
:
theorem
LO.IntProp.Formula.Kripke.ValidOnModel.and₃
{α : Type u}
{M : LO.Kripke.Model α}
{p : LO.IntProp.Formula α}
{q : LO.IntProp.Formula α}
(atom_hereditary : ∀ {w₁ w₂ : M.World}, w₁ ≺ w₂ → ∀ {a : α}, M.Valuation w₁ a → M.Valuation w₂ a)
(F_trans : autoParam (Transitive M.Frame.Rel) _auto✝)
:
theorem
LO.IntProp.Formula.Kripke.ValidOnModel.or₁
{α : Type u}
{M : LO.Kripke.Model α}
{p : LO.IntProp.Formula α}
{q : LO.IntProp.Formula α}
:
theorem
LO.IntProp.Formula.Kripke.ValidOnModel.or₂
{α : Type u}
{M : LO.Kripke.Model α}
{p : LO.IntProp.Formula α}
{q : LO.IntProp.Formula α}
:
theorem
LO.IntProp.Formula.Kripke.ValidOnModel.or₃
{α : Type u}
{M : LO.Kripke.Model α}
{p : LO.IntProp.Formula α}
{q : LO.IntProp.Formula α}
{r : LO.IntProp.Formula α}
(F_trans : autoParam (Transitive M.Frame.Rel) _auto✝)
:
theorem
LO.IntProp.Formula.Kripke.ValidOnModel.imply₁
{α : Type u}
{M : LO.Kripke.Model α}
{p : LO.IntProp.Formula α}
{q : LO.IntProp.Formula α}
(atom_hereditary : ∀ {w₁ w₂ : M.World}, w₁ ≺ w₂ → ∀ {a : α}, M.Valuation w₁ a → M.Valuation w₂ a)
(F_trans : autoParam (Transitive M.Frame.Rel) _auto✝)
:
theorem
LO.IntProp.Formula.Kripke.ValidOnModel.imply₂
{α : Type u}
{M : LO.Kripke.Model α}
{p : LO.IntProp.Formula α}
{q : LO.IntProp.Formula α}
{r : LO.IntProp.Formula α}
(F_trans : autoParam (Transitive M.Frame.Rel) _auto✝)
(F_refl : autoParam (Reflexive M.Frame.Rel) _auto✝)
:
theorem
LO.IntProp.Formula.Kripke.ValidOnModel.mdp
{α : Type u}
{M : LO.Kripke.Model α}
{p : LO.IntProp.Formula α}
{q : LO.IntProp.Formula α}
(F_refl : autoParam (Reflexive M.Frame.Rel) _auto✝)
(hpq : M ⊧ p ➝ q)
(hp : M ⊧ p)
:
M ⊧ q
theorem
LO.IntProp.Formula.Kripke.ValidOnModel.efq
{α : Type u}
{M : LO.Kripke.Model α}
{p : LO.IntProp.Formula α}
:
M ⊧ LO.Axioms.EFQ p
theorem
LO.IntProp.Formula.Kripke.ValidOnModel.neg_equiv
{α : Type u}
{M : LO.Kripke.Model α}
{p : LO.IntProp.Formula α}
:
M ⊧ LO.Axioms.NegEquiv p
theorem
LO.IntProp.Formula.Kripke.ValidOnModel.lem
{α : Type u}
{M : LO.Kripke.Model α}
{p : LO.IntProp.Formula α}
(atom_hereditary : ∀ {w₁ w₂ : M.World}, w₁ ≺ w₂ → ∀ {a : α}, M.Valuation w₁ a → M.Valuation w₂ a)
(F_trans : autoParam (Transitive M.Frame.Rel) _auto✝)
:
Symmetric M.Frame.Rel → M ⊧ LO.Axioms.LEM p
theorem
LO.IntProp.Formula.Kripke.ValidOnModel.dum
{α : Type u}
{M : LO.Kripke.Model α}
{p : LO.IntProp.Formula α}
{q : LO.IntProp.Formula α}
(atom_hereditary : ∀ {w₁ w₂ : M.World}, w₁ ≺ w₂ → ∀ {a : α}, M.Valuation w₁ a → M.Valuation w₂ a)
(F_trans : autoParam (Transitive M.Frame.Rel) _auto✝)
:
Connected M.Frame.Rel → M ⊧ LO.Axioms.GD p q
theorem
LO.IntProp.Formula.Kripke.ValidOnModel.wlem
{α : Type u}
{M : LO.Kripke.Model α}
{p : LO.IntProp.Formula α}
(atom_hereditary : ∀ {w₁ w₂ : M.World}, w₁ ≺ w₂ → ∀ {a : α}, M.Valuation w₁ a → M.Valuation w₂ a)
(F_trans : autoParam (Transitive M.Frame.Rel) _auto✝)
:
Confluent M.Frame.Rel → M ⊧ LO.Axioms.WeakLEM p
def
LO.IntProp.Formula.Kripke.ValidOnFrame
{α : Type u}
(F : LO.Kripke.Frame)
(p : LO.IntProp.Formula α)
:
Equations
- LO.IntProp.Formula.Kripke.ValidOnFrame F p = ∀ {V : LO.Kripke.Valuation F α}, V.atomic_hereditary → { Frame := F, Valuation := V } ⊧ p
Instances For
Equations
- LO.IntProp.Formula.Kripke.ValidOnFrame.semantics = { Realize := fun (F : LO.Kripke.Frame.Dep α) => LO.IntProp.Formula.Kripke.ValidOnFrame F }
@[simp]
theorem
LO.IntProp.Formula.Kripke.ValidOnFrame.models_iff
{α : Type u}
{F : LO.Kripke.Frame.Dep α}
{f : LO.IntProp.Formula α}
:
F ⊧ f ↔ LO.IntProp.Formula.Kripke.ValidOnFrame F f
theorem
LO.IntProp.Formula.Kripke.ValidOnFrame.and₁
{α : Type u}
{F : LO.Kripke.Frame.Dep α}
{p : LO.IntProp.Formula α}
{q : LO.IntProp.Formula α}
:
theorem
LO.IntProp.Formula.Kripke.ValidOnFrame.and₂
{α : Type u}
{F : LO.Kripke.Frame.Dep α}
{p : LO.IntProp.Formula α}
{q : LO.IntProp.Formula α}
:
theorem
LO.IntProp.Formula.Kripke.ValidOnFrame.and₃
{α : Type u}
{F : LO.Kripke.Frame.Dep α}
{p : LO.IntProp.Formula α}
{q : LO.IntProp.Formula α}
(F_trans : Transitive F.Rel)
:
theorem
LO.IntProp.Formula.Kripke.ValidOnFrame.or₁
{α : Type u}
{F : LO.Kripke.Frame.Dep α}
{p : LO.IntProp.Formula α}
{q : LO.IntProp.Formula α}
:
theorem
LO.IntProp.Formula.Kripke.ValidOnFrame.or₂
{α : Type u}
{F : LO.Kripke.Frame.Dep α}
{p : LO.IntProp.Formula α}
{q : LO.IntProp.Formula α}
:
theorem
LO.IntProp.Formula.Kripke.ValidOnFrame.or₃
{α : Type u}
{F : LO.Kripke.Frame.Dep α}
{p : LO.IntProp.Formula α}
{q : LO.IntProp.Formula α}
{r : LO.IntProp.Formula α}
(F_trans : Transitive F.Rel)
:
theorem
LO.IntProp.Formula.Kripke.ValidOnFrame.imply₁
{α : Type u}
{F : LO.Kripke.Frame.Dep α}
{p : LO.IntProp.Formula α}
{q : LO.IntProp.Formula α}
(F_trans : Transitive F.Rel)
:
theorem
LO.IntProp.Formula.Kripke.ValidOnFrame.imply₂
{α : Type u}
{F : LO.Kripke.Frame.Dep α}
{p : LO.IntProp.Formula α}
{q : LO.IntProp.Formula α}
{r : LO.IntProp.Formula α}
(F_trans : Transitive F.Rel)
(F_refl : Reflexive F.Rel)
:
theorem
LO.IntProp.Formula.Kripke.ValidOnFrame.mdp
{α : Type u}
{F : LO.Kripke.Frame.Dep α}
{p : LO.IntProp.Formula α}
{q : LO.IntProp.Formula α}
(F_refl : Reflexive F.Rel)
(hpq : F ⊧ p ➝ q)
(hp : F ⊧ p)
:
F ⊧ q
theorem
LO.IntProp.Formula.Kripke.ValidOnFrame.efq
{α : Type u}
{F : LO.Kripke.Frame.Dep α}
{p : LO.IntProp.Formula α}
:
F ⊧ LO.Axioms.EFQ p
theorem
LO.IntProp.Formula.Kripke.ValidOnFrame.neg_equiv
{α : Type u}
{F : LO.Kripke.Frame.Dep α}
{p : LO.IntProp.Formula α}
:
F ⊧ LO.Axioms.NegEquiv p
theorem
LO.IntProp.Formula.Kripke.ValidOnFrame.lem
{α : Type u}
{F : LO.Kripke.Frame.Dep α}
{p : LO.IntProp.Formula α}
(F_trans : Transitive F.Rel)
(F_symm : Symmetric F.Rel)
:
F ⊧ LO.Axioms.LEM p
theorem
LO.IntProp.Formula.Kripke.ValidOnFrame.dum
{α : Type u}
{F : LO.Kripke.Frame.Dep α}
{p : LO.IntProp.Formula α}
{q : LO.IntProp.Formula α}
(F_trans : Transitive F.Rel)
(F_conn : Connected F.Rel)
:
F ⊧ LO.Axioms.GD p q
theorem
LO.IntProp.Formula.Kripke.ValidOnFrame.wlem
{α : Type u}
{F : LO.Kripke.Frame.Dep α}
{p : LO.IntProp.Formula α}
(F_trans : Transitive F.Rel)
(F_conf : Confluent F.Rel)
:
F ⊧ LO.Axioms.WeakLEM p
Equations
- LO.IntProp.Formula.Kripke.ValidOnFrame.instBotDep = { realize_bot := ⋯ }
def
LO.IntProp.Formula.Kripke.ValidOnFrameClass
{α : Type u}
(𝔽 : LO.Kripke.FrameClass)
(p : LO.IntProp.Formula α)
:
Equations
- LO.IntProp.Formula.Kripke.ValidOnFrameClass 𝔽 p = ∀ {F : LO.Kripke.Frame}, F ∈ 𝔽 → F#α ⊧ p
Instances For
Equations
- LO.IntProp.Formula.Kripke.ValidOnFrameClass.semantics = { Realize := fun (𝔽 : LO.Kripke.FrameClass.Dep α) => LO.IntProp.Formula.Kripke.ValidOnFrameClass 𝔽 }
@[simp]
theorem
LO.IntProp.Formula.Kripke.ValidOnFrameClass.models_iff
{α : Type u}
{𝔽 : LO.Kripke.FrameClass.Dep α}
{p : LO.IntProp.Formula α}
:
@[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
theorem
LO.IntProp.Kripke.sound
{α : Type u}
{Λ : LO.IntProp.Hilbert α}
{p : LO.IntProp.Formula α}
:
instance
LO.IntProp.Kripke.instSoundHilbertFormulaDepFrameClassOfHilbert
{α : Type u}
{Λ : LO.IntProp.Hilbert α}
:
Equations
- ⋯ = ⋯
theorem
LO.IntProp.Kripke.unprovable_bot
{α : Type u}
{Λ : LO.IntProp.Hilbert α}
(hc : Set.Nonempty 𝔽(Λ))
:
instance
LO.IntProp.Kripke.instConsistentFormulaHilbertOfNonemptyFrameFrameClassOfHilbert
{α : Type u}
{Λ : LO.IntProp.Hilbert α}
(hc : Set.Nonempty 𝔽(Λ))
:
Equations
- ⋯ = ⋯
theorem
LO.IntProp.Kripke.sound_of_characterizability
{α : Type u}
{Λ : LO.IntProp.Hilbert α}
{p : LO.IntProp.Formula α}
{𝔽₂ : LO.Kripke.FrameClass}
[characterizability : LO.Kripke.FrameClass.Characteraizable 𝔽(Λ) 𝔽₂]
:
instance
LO.IntProp.Kripke.instSoundOfCharacterizability
{α : Type u}
{Λ : LO.IntProp.Hilbert α}
{𝔽₂ : LO.Kripke.FrameClass}
[LO.Kripke.FrameClass.Characteraizable 𝔽(Λ) 𝔽₂]
:
Equations
- ⋯ = ⋯
theorem
LO.IntProp.Kripke.unprovable_bot_of_characterizability
{α : Type u}
{Λ : LO.IntProp.Hilbert α}
{𝔽₂ : LO.Kripke.FrameClass}
[characterizability : LO.Kripke.FrameClass.Characteraizable 𝔽(Λ) 𝔽₂]
:
instance
LO.IntProp.Kripke.instConsistentOfCharacterizability
{α : Type u}
{Λ : LO.IntProp.Hilbert α}
{𝔽₂ : LO.Kripke.FrameClass}
[LO.Kripke.FrameClass.Characteraizable 𝔽(Λ) 𝔽₂]
:
Equations
- ⋯ = ⋯
Equations
- LO.IntProp.Kripke.Int_Characteraizable = { characterize := ⋯, nonempty := LO.IntProp.Kripke.Int_Characteraizable.proof_2 }
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
Equations
- LO.IntProp.Kripke.Cl_Characteraizable = { characterize := ⋯, nonempty := ⋯ }
Equations
- ⋯ = ⋯
Equations
- LO.IntProp.Kripke.KC_Characteraizable = { characterize := ⋯, nonempty := LO.IntProp.Kripke.KC_Characteraizable.proof_2 }
Equations
- ⋯ = ⋯
Equations
- LO.IntProp.Kripke.LC_Characteraizable = { characterize := ⋯, nonempty := LO.IntProp.Kripke.LC_Characteraizable.proof_2 }
Equations
- ⋯ = ⋯
@[reducible, inline]
abbrev
LO.IntProp.Formula.Kripke.ClassicalSatisfies
{α : Type u}
(V : LO.Kripke.ClassicalValuation α)
(p : LO.IntProp.Formula α)
:
Equations
Instances For
Equations
- LO.IntProp.Formula.Kripke.instSemanticsClassicalValuation = { Realize := LO.IntProp.Formula.Kripke.ClassicalSatisfies }
@[simp]
theorem
LO.IntProp.Formula.Kripke.ClassicalSatisfies.atom_def
{α : Type u}
{V : LO.Kripke.ClassicalValuation α}
{a : α}
:
V ⊧ LO.IntProp.Formula.atom a ↔ V a
Equations
- LO.IntProp.Formula.Kripke.ClassicalSatisfies.instTarskiClassicalValuation = LO.Semantics.Tarski.mk
theorem
LO.IntProp.Kripke.notClassicalValid_of_exists_ClassicalValuation
{α : Type u}
{p : LO.IntProp.Formula α}
:
theorem
LO.IntProp.Kripke.unprovable_classical_of_exists_ClassicalValuation
{α : Type u}
{p : LO.IntProp.Formula α}
(h : ∃ (V : LO.Kripke.ClassicalValuation α), ¬V ⊧ p)
: