Documentation

Logic.Modal.PLoN.Semantics

source
structure LO.Modal.PLoN.Frame (α : Type u_2) :
Type (max (u_1 + 1) u_2)
Instances For
source
theorem LO.Modal.PLoN.Frame.World_nonempty {α : Type u_2} (self : LO.Modal.PLoN.Frame α) :
Nonempty self.World
source
@[reducible, inline]
noncomputable abbrev LO.Modal.PLoN.Frame.default {α : Type u_1} {F : LO.Modal.PLoN.Frame α} :
F.World
Equations
  • LO.Modal.PLoN.Frame.default = ⋯.some
source
def LO.Modal.PLoN.«term﹫» :
Lean.ParserDescr
Equations
source
instance LO.Modal.PLoN.instCoeFunFrameForallFormulaForallWorldForallProp {α : Type u_1} :
CoeFun (LO.Modal.PLoN.Frame α) fun (F : LO.Modal.PLoN.Frame α) => LO.Modal.Formula α → F.World → F.World → Prop
Equations
  • LO.Modal.PLoN.instCoeFunFrameForallFormulaForallWorldForallProp = { coe := LO.Modal.PLoN.Frame.Rel }
source
@[reducible, inline]
abbrev LO.Modal.PLoN.Frame.Rel' {α : Type u_1} {F : LO.Modal.PLoN.Frame α} (p : LO.Modal.Formula α) (x : F.World) (y : F.World) :
Prop
Equations
source
def LO.Modal.PLoN.«term_≺[_]_» :
Lean.TrailingParserDescr
Equations
  • One or more equations did not get rendered due to their size.
source
structure LO.Modal.PLoN.FiniteFrame (α : Type u_1) extends LO.Modal.PLoN.Frame :
Type (max u_1 (u_2 + 1))
Instances For
source
theorem LO.Modal.PLoN.FiniteFrame.World_finite {α : Type u_1} (self : LO.Modal.PLoN.FiniteFrame α) :
Finite self.World
source
instance LO.Modal.PLoN.instCoeFiniteFrameFrame {α : Type u_1} :
Coe (LO.Modal.PLoN.FiniteFrame α) (LO.Modal.PLoN.Frame α)
Equations
source
@[reducible, inline]
abbrev LO.Modal.PLoN.terminalFrame (α : Type u_1) :
LO.Modal.PLoN.FiniteFrame α
Equations
source
@[reducible, inline]
abbrev LO.Modal.PLoN.FrameClass (α : Type u_1) :
Type (max u_1 (u_2 + 1))
Equations
Instances For
source
@[reducible, inline]
abbrev LO.Modal.PLoN.Valuation {α : Type u_2} (F : LO.Modal.PLoN.Frame α✝) (α : Type u_1) :
Type (max u_1 u_3)
Equations
source
structure LO.Modal.PLoN.Model (α : Type u_1) :
Type (max u_1 (u_2 + 1))
Instances For
source
@[reducible, inline]
abbrev LO.Modal.PLoN.Model.World {α : Type u_1} (M : LO.Modal.PLoN.Model α) :
Type u_2
Equations
  • M.World = M.Frame.World
Instances For
source
instance LO.Modal.PLoN.instCoeSortModelType {α : Type u_1} :
CoeSort (LO.Modal.PLoN.Model α) (Type u_2)
Equations
  • LO.Modal.PLoN.instCoeSortModelType = { coe := LO.Modal.PLoN.Model.World }
source
def LO.Modal.Formula.PLoN.Satisfies {α : Type u_1} (M : LO.Modal.PLoN.Model α) (w : M.World) :
LO.Modal.Formula α → Prop
Equations
source
instance LO.Modal.Formula.PLoN.Satisfies.semantics {α : Type u_1} (M : LO.Modal.PLoN.Model α) :
LO.Semantics (LO.Modal.Formula α) M.World
Equations
source
@[simp]
theorem LO.Modal.Formula.PLoN.Satisfies.iff_models {α : Type u_1} {M : LO.Modal.PLoN.Model α} {x : M.World} {p : LO.Modal.Formula α} :
x ⊧ p ↔ LO.Modal.Formula.PLoN.Satisfies M x p
source
theorem LO.Modal.Formula.PLoN.Satisfies.box_def {α : Type u_1} {M : LO.Modal.PLoN.Model α} {x : M.World} {p : LO.Modal.Formula α} :
x ⊧ □p ↔ ∀ (y : M.Frame.World), LO.Modal.PLoN.Frame.Rel' p x y → y ⊧ p
source
theorem LO.Modal.Formula.PLoN.Satisfies.not_def {α : Type u_1} {M : LO.Modal.PLoN.Model α} {x : M.World} {p : LO.Modal.Formula α} :
x ⊧ ∼p ↔ ¬x ⊧ p
source
instance LO.Modal.Formula.PLoN.Satisfies.instNotWorld {α : Type u_1} {M : LO.Modal.PLoN.Model α} :
LO.Semantics.Not M.World
Equations
  • LO.Modal.Formula.PLoN.Satisfies.instNotWorld = { realize_not := ⋯ }
source
theorem LO.Modal.Formula.PLoN.Satisfies.imp_def {α : Type u_1} {M : LO.Modal.PLoN.Model α} {x : M.World} {p : LO.Modal.Formula α} {q : LO.Modal.Formula α} :
x ⊧ p ➝ q ↔ x ⊧ p → x ⊧ q
source
instance LO.Modal.Formula.PLoN.Satisfies.instImpWorld {α : Type u_1} {M : LO.Modal.PLoN.Model α} :
LO.Semantics.Imp M.World
Equations
  • LO.Modal.Formula.PLoN.Satisfies.instImpWorld = { realize_imp := ⋯ }
source
theorem LO.Modal.Formula.PLoN.Satisfies.or_def {α : Type u_1} {M : LO.Modal.PLoN.Model α} {x : M.World} {p : LO.Modal.Formula α} {q : LO.Modal.Formula α} :
x ⊧ p ⋎ q ↔ x ⊧ p ∨ x ⊧ q
source
instance LO.Modal.Formula.PLoN.Satisfies.instOrWorld {α : Type u_1} {M : LO.Modal.PLoN.Model α} :
LO.Semantics.Or M.World
Equations
  • LO.Modal.Formula.PLoN.Satisfies.instOrWorld = { realize_or := ⋯ }
source
theorem LO.Modal.Formula.PLoN.Satisfies.and_def {α : Type u_1} {M : LO.Modal.PLoN.Model α} {x : M.World} {p : LO.Modal.Formula α} {q : LO.Modal.Formula α} :
x ⊧ p ⋏ q ↔ x ⊧ p ∧ x ⊧ q
source
instance LO.Modal.Formula.PLoN.Satisfies.instAndWorld {α : Type u_1} {M : LO.Modal.PLoN.Model α} :
LO.Semantics.And M.World
Equations
  • LO.Modal.Formula.PLoN.Satisfies.instAndWorld = { realize_and := ⋯ }
source
instance LO.Modal.Formula.PLoN.Satisfies.instTarskiWorld {α : Type u_1} {M : LO.Modal.PLoN.Model α} :
LO.Semantics.Tarski M.World
Equations
  • LO.Modal.Formula.PLoN.Satisfies.instTarskiWorld = LO.Semantics.Tarski.mk
source
def LO.Modal.Formula.PLoN.ValidOnModel {α : Type u_1} (M : LO.Modal.PLoN.Model α) (p : LO.Modal.Formula α) :
Prop
Equations
source
instance LO.Modal.Formula.PLoN.ValidOnModel.instSemanticsModel {α : Type u_1} :
LO.Semantics (LO.Modal.Formula α) (LO.Modal.PLoN.Model α)
Equations
source
@[simp]
theorem LO.Modal.Formula.PLoN.ValidOnModel.iff_models {α : Type u_1} {M : LO.Modal.PLoN.Model α} {p : LO.Modal.Formula α} :
M ⊧ p ↔ LO.Modal.Formula.PLoN.ValidOnModel M p
source
instance LO.Modal.Formula.PLoN.ValidOnModel.instBotModel {α : Type u_1} :
LO.Semantics.Bot (LO.Modal.PLoN.Model α)
Equations
  • LO.Modal.Formula.PLoN.ValidOnModel.instBotModel = { realize_bot := ⋯ }
source
theorem LO.Modal.Formula.PLoN.ValidOnModel.imply₁ {α : Type u_1} {M : LO.Modal.PLoN.Model α} {p : LO.Modal.Formula α} {q : LO.Modal.Formula α} :
M ⊧ LO.Axioms.Imply₁ p q
source
theorem LO.Modal.Formula.PLoN.ValidOnModel.imply₂ {α : Type u_1} {M : LO.Modal.PLoN.Model α} {p : LO.Modal.Formula α} {q : LO.Modal.Formula α} {r : LO.Modal.Formula α} :
M ⊧ LO.Axioms.Imply₂ p q r
source
theorem LO.Modal.Formula.PLoN.ValidOnModel.elim_contra {α : Type u_1} {M : LO.Modal.PLoN.Model α} {p : LO.Modal.Formula α} {q : LO.Modal.Formula α} :
M ⊧ LO.Axioms.ElimContra p q
source
def LO.Modal.Formula.PLoN.ValidOnFrame {α : Type u_1} (F : LO.Modal.PLoN.Frame α) (p : LO.Modal.Formula α) :
Prop
Equations
source
instance LO.Modal.Formula.PLoN.ValidOnFrame.instSemanticsFrame {α : Type u_1} :
LO.Semantics (LO.Modal.Formula α) (LO.Modal.PLoN.Frame α)
Equations
source
@[simp]
theorem LO.Modal.Formula.PLoN.ValidOnFrame.iff_models {α : Type u_1} {F : LO.Modal.PLoN.Frame α} {p : LO.Modal.Formula α} :
F ⊧ p ↔ LO.Modal.Formula.PLoN.ValidOnFrame F p
source
instance LO.Modal.Formula.PLoN.ValidOnFrame.instBotFrame {α : Type u_1} :
LO.Semantics.Bot (LO.Modal.PLoN.Frame α)
Equations
  • LO.Modal.Formula.PLoN.ValidOnFrame.instBotFrame = { realize_bot := ⋯ }
source
theorem LO.Modal.Formula.PLoN.ValidOnFrame.nec {α : Type u_1} {F : LO.Modal.PLoN.Frame α} {p : LO.Modal.Formula α} (h : F ⊧ p) :
F ⊧ □p
source
theorem LO.Modal.Formula.PLoN.ValidOnFrame.mdp {α : Type u_1} {F : LO.Modal.PLoN.Frame α} {p : LO.Modal.Formula α} {q : LO.Modal.Formula α} (hpq : F ⊧ p ➝ q) (hp : F ⊧ p) :
F ⊧ q
source
theorem LO.Modal.Formula.PLoN.ValidOnFrame.imply₁ {α : Type u_1} {F : LO.Modal.PLoN.Frame α} {p : LO.Modal.Formula α} {q : LO.Modal.Formula α} :
F ⊧ LO.Axioms.Imply₁ p q
source
theorem LO.Modal.Formula.PLoN.ValidOnFrame.imply₂ {α : Type u_1} {F : LO.Modal.PLoN.Frame α} {p : LO.Modal.Formula α} {q : LO.Modal.Formula α} {r : LO.Modal.Formula α} :
F ⊧ LO.Axioms.Imply₂ p q r
source
theorem LO.Modal.Formula.PLoN.ValidOnFrame.elim_contra {α : Type u_1} {F : LO.Modal.PLoN.Frame α} {p : LO.Modal.Formula α} {q : LO.Modal.Formula α} :
F ⊧ LO.Axioms.ElimContra p q
source
def LO.Modal.Formula.PLoN.ValidOnFrameClass {α : Type u_1} (𝔽 : LO.Modal.PLoN.FrameClass α) (p : LO.Modal.Formula α) :
Prop
Equations
source
instance LO.Modal.Formula.PLoN.ValidOnFrameClass.instSemanticsFrameClass {α : Type u_1} :
LO.Semantics (LO.Modal.Formula α) (LO.Modal.PLoN.FrameClass α)
Equations
source
@[simp]
theorem LO.Modal.Formula.PLoN.ValidOnFrameClass.iff_models {α : Type u_1} {𝔽 : LO.Modal.PLoN.FrameClass α} {p : LO.Modal.Formula α} :
𝔽 ⊧ p ↔ LO.Modal.Formula.PLoN.ValidOnFrameClass 𝔽 p
source
theorem LO.Modal.Formula.PLoN.ValidOnFrameClass.nec {α : Type u_1} {𝔽 : LO.Modal.PLoN.FrameClass α} {p : LO.Modal.Formula α} (h : 𝔽 ⊧ p) :
𝔽 ⊧ □p
source
theorem LO.Modal.Formula.PLoN.ValidOnFrameClass.mdp {α : Type u_1} {𝔽 : LO.Modal.PLoN.FrameClass α} {p : LO.Modal.Formula α} {q : LO.Modal.Formula α} (hpq : 𝔽 ⊧ p ➝ q) (hp : 𝔽 ⊧ p) :
𝔽 ⊧ q
source
theorem LO.Modal.Formula.PLoN.ValidOnFrameClass.imply₁ {α : Type u_1} {𝔽 : LO.Modal.PLoN.FrameClass α} {p : LO.Modal.Formula α} {q : LO.Modal.Formula α} :
𝔽 ⊧ LO.Axioms.Imply₁ p q
source
theorem LO.Modal.Formula.PLoN.ValidOnFrameClass.imply₂ {α : Type u_1} {𝔽 : LO.Modal.PLoN.FrameClass α} {p : LO.Modal.Formula α} {q : LO.Modal.Formula α} {r : LO.Modal.Formula α} :
𝔽 ⊧ LO.Axioms.Imply₂ p q r
source
theorem LO.Modal.Formula.PLoN.ValidOnFrameClass.elim_contra {α : Type u_1} {𝔽 : LO.Modal.PLoN.FrameClass α} {p : LO.Modal.Formula α} {q : LO.Modal.Formula α} :
𝔽 ⊧ LO.Axioms.ElimContra p q
source
def LO.Modal.Hilbert.DefinesPLoNFrameClass {α : Type u_1} (Λ : LO.Modal.Hilbert α) (𝔽 : LO.Modal.PLoN.FrameClass α) :
Prop
Equations
source
@[reducible, inline]
abbrev LO.Modal.PLoN.AllFrameClass (α : Type u_2) :
LO.Modal.PLoN.FrameClass α
Equations
Instances For
source
theorem LO.Modal.PLoN.AllFrameClass.nonempty {α : Type u_1} :
Set.Nonempty (LO.Modal.PLoN.AllFrameClass α)
source
theorem LO.Modal.PLoN.N_defines {α : Type u_1} :
𝐍.DefinesPLoNFrameClass (LO.Modal.PLoN.AllFrameClass α)