Documentation

Foundation.Modal.PLoN.Semantics

source
structure LO.Modal.PLoN.Frame (α : Type u_2) :
Type (max (u_1 + 1) u_2)
Instances For
source
@[reducible, inline]
noncomputable abbrev LO.Modal.PLoN.Frame.default {α : Type u_1} {F : Frame α} :
F.World
Equations
source
def LO.Modal.PLoN.«term﹫» :
Lean.ParserDescr
Equations
source
instance LO.Modal.PLoN.instCoeFunFrameForallFormulaForallWorldForallProp {α : Type u_1} :
CoeFun (Frame α) fun (F : Frame α) => Formula α → F.World → F.World → Prop
Equations
source
@[reducible, inline]
abbrev LO.Modal.PLoN.Frame.Rel' {α : Type u_1} {F : Frame α} (φ : Formula α) (x 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
instance LO.Modal.PLoN.instCoeFiniteFrameFrame {α : Type u_1} :
Coe (FiniteFrame α) (Frame α)
Equations
source
@[reducible, inline]
abbrev LO.Modal.PLoN.terminalFrame (α : Type u_1) :
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 : 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 : Model α) :
Type u_2
Equations
  • M.World = M.Frame.World
Instances For
source
instance LO.Modal.PLoN.instCoeSortModelType {α : Type u_1} :
CoeSort (Model α) (Type u_2)
Equations
source
def LO.Modal.Formula.PLoN.Satisfies {α : Type u_1} (M : PLoN.Model α) (w : M.World) :
Formula α → Prop
Equations
source
instance LO.Modal.Formula.PLoN.Satisfies.semantics {α : Type u_1} (M : PLoN.Model α) :
Semantics (Formula α) M.World
Equations
source
@[simp]
theorem LO.Modal.Formula.PLoN.Satisfies.iff_models {α : Type u_1} {M : PLoN.Model α} {x : M.World} {φ : Formula α} :
x ⊧ φ ↔ Satisfies M x φ
source
theorem LO.Modal.Formula.PLoN.Satisfies.box_def {α : Type u_1} {M : PLoN.Model α} {x : M.World} {φ : Formula α} :
x ⊧ □φ ↔ ∀ (y : M.Frame.World), PLoN.Frame.Rel' φ x y → y ⊧ φ
source
theorem LO.Modal.Formula.PLoN.Satisfies.not_def {α : Type u_1} {M : PLoN.Model α} {x : M.World} {φ : Formula α} :
x ⊧ ∼φ ↔ ¬x ⊧ φ
source
instance LO.Modal.Formula.PLoN.Satisfies.instNotWorld {α : Type u_1} {M : PLoN.Model α} :
Semantics.Not M.World
source
theorem LO.Modal.Formula.PLoN.Satisfies.imp_def {α : Type u_1} {M : PLoN.Model α} {x : M.World} {φ ψ : Formula α} :
x ⊧ φ ➝ ψ ↔ x ⊧ φ → x ⊧ ψ
source
instance LO.Modal.Formula.PLoN.Satisfies.instImpWorld {α : Type u_1} {M : PLoN.Model α} :
Semantics.Imp M.World
source
theorem LO.Modal.Formula.PLoN.Satisfies.or_def {α : Type u_1} {M : PLoN.Model α} {x : M.World} {φ ψ : Formula α} :
x ⊧ φ ⋎ ψ ↔ x ⊧ φ ∨ x ⊧ ψ
source
instance LO.Modal.Formula.PLoN.Satisfies.instOrWorld {α : Type u_1} {M : PLoN.Model α} :
Semantics.Or M.World
source
theorem LO.Modal.Formula.PLoN.Satisfies.and_def {α : Type u_1} {M : PLoN.Model α} {x : M.World} {φ ψ : Formula α} :
x ⊧ φ ⋏ ψ ↔ x ⊧ φ ∧ x ⊧ ψ
source
instance LO.Modal.Formula.PLoN.Satisfies.instAndWorld {α : Type u_1} {M : PLoN.Model α} :
Semantics.And M.World
source
instance LO.Modal.Formula.PLoN.Satisfies.instTarskiWorld {α : Type u_1} {M : PLoN.Model α} :
Semantics.Tarski M.World
source
def LO.Modal.Formula.PLoN.ValidOnModel {α : Type u_1} (M : PLoN.Model α) (φ : Formula α) :
Prop
Equations
source
instance LO.Modal.Formula.PLoN.ValidOnModel.instSemanticsModel {α : Type u_1} :
Semantics (Formula α) (PLoN.Model α)
Equations
source
@[simp]
theorem LO.Modal.Formula.PLoN.ValidOnModel.iff_models {α : Type u_1} {M : PLoN.Model α} {φ : Formula α} :
M ⊧ φ ↔ ValidOnModel M φ
source
instance LO.Modal.Formula.PLoN.ValidOnModel.instBotModel {α : Type u_1} :
Semantics.Bot (PLoN.Model α)
source
theorem LO.Modal.Formula.PLoN.ValidOnModel.imply₁ {α : Type u_1} {M : PLoN.Model α} {φ ψ : Formula α} :
M ⊧ Axioms.Imply₁ φ ψ
source
theorem LO.Modal.Formula.PLoN.ValidOnModel.imply₂ {α : Type u_1} {M : PLoN.Model α} {φ ψ χ : Formula α} :
M ⊧ Axioms.Imply₂ φ ψ χ
source
theorem LO.Modal.Formula.PLoN.ValidOnModel.elim_contra {α : Type u_1} {M : PLoN.Model α} {φ ψ : Formula α} :
M ⊧ Axioms.ElimContra φ ψ
source
def LO.Modal.Formula.PLoN.ValidOnFrame {α : Type u_1} (F : PLoN.Frame α) (φ : Formula α) :
Prop
Equations
source
instance LO.Modal.Formula.PLoN.ValidOnFrame.instSemanticsFrame {α : Type u_1} :
Semantics (Formula α) (PLoN.Frame α)
Equations
source
@[simp]
theorem LO.Modal.Formula.PLoN.ValidOnFrame.iff_models {α : Type u_1} {F : PLoN.Frame α} {φ : Formula α} :
F ⊧ φ ↔ ValidOnFrame F φ
source
instance LO.Modal.Formula.PLoN.ValidOnFrame.instBotFrame {α : Type u_1} :
Semantics.Bot (PLoN.Frame α)
source
theorem LO.Modal.Formula.PLoN.ValidOnFrame.nec {α : Type u_1} {F : PLoN.Frame α} {φ : Formula α} (h : F ⊧ φ) :
F ⊧ □φ
source
theorem LO.Modal.Formula.PLoN.ValidOnFrame.mdp {α : Type u_1} {F : PLoN.Frame α} {φ ψ : Formula α} (hpq : F ⊧ φ ➝ ψ) (hp : F ⊧ φ) :
F ⊧ ψ
source
theorem LO.Modal.Formula.PLoN.ValidOnFrame.imply₁ {α : Type u_1} {F : PLoN.Frame α} {φ ψ : Formula α} :
F ⊧ Axioms.Imply₁ φ ψ
source
theorem LO.Modal.Formula.PLoN.ValidOnFrame.imply₂ {α : Type u_1} {F : PLoN.Frame α} {φ ψ χ : Formula α} :
F ⊧ Axioms.Imply₂ φ ψ χ
source
theorem LO.Modal.Formula.PLoN.ValidOnFrame.elim_contra {α : Type u_1} {F : PLoN.Frame α} {φ ψ : Formula α} :
F ⊧ Axioms.ElimContra φ ψ
source
def LO.Modal.Formula.PLoN.ValidOnFrameClass {α : Type u_1} (𝔽 : PLoN.FrameClass α) (φ : Formula α) :
Prop
Equations
source
instance LO.Modal.Formula.PLoN.ValidOnFrameClass.instSemanticsFrameClass {α : Type u_1} :
Semantics (Formula α) (PLoN.FrameClass α)
Equations
source
@[simp]
theorem LO.Modal.Formula.PLoN.ValidOnFrameClass.iff_models {α : Type u_1} {𝔽 : PLoN.FrameClass α} {φ : Formula α} :
𝔽 ⊧ φ ↔ ValidOnFrameClass 𝔽 φ
source
theorem LO.Modal.Formula.PLoN.ValidOnFrameClass.nec {α : Type u_1} {𝔽 : PLoN.FrameClass α} {φ : Formula α} (h : 𝔽 ⊧ φ) :
𝔽 ⊧ □φ
source
theorem LO.Modal.Formula.PLoN.ValidOnFrameClass.mdp {α : Type u_1} {𝔽 : PLoN.FrameClass α} {φ ψ : Formula α} (hpq : 𝔽 ⊧ φ ➝ ψ) (hp : 𝔽 ⊧ φ) :
𝔽 ⊧ ψ
source
theorem LO.Modal.Formula.PLoN.ValidOnFrameClass.imply₁ {α : Type u_1} {𝔽 : PLoN.FrameClass α} {φ ψ : Formula α} :
𝔽 ⊧ Axioms.Imply₁ φ ψ
source
theorem LO.Modal.Formula.PLoN.ValidOnFrameClass.imply₂ {α : Type u_1} {𝔽 : PLoN.FrameClass α} {φ ψ χ : Formula α} :
𝔽 ⊧ Axioms.Imply₂ φ ψ χ
source
theorem LO.Modal.Formula.PLoN.ValidOnFrameClass.elim_contra {α : Type u_1} {𝔽 : PLoN.FrameClass α} {φ ψ : Formula α} :
𝔽 ⊧ Axioms.ElimContra φ ψ
source
def LO.Modal.Hilbert.DefinesPLoNFrameClass {α : Type u_1} (H : Hilbert α) (𝔽 : PLoN.FrameClass α) :
Prop
Equations
source
@[reducible, inline]
abbrev LO.Modal.PLoN.AllFrameClass (α : Type u_2) :
FrameClass α
Equations
Instances For
source
theorem LO.Modal.PLoN.AllFrameClass.nonempty {α : Type u_1} :
Set.Nonempty (AllFrameClass α)
source
theorem LO.Modal.PLoN.N_defines {α : Type u_1} :
(Hilbert.N α).DefinesPLoNFrameClass (AllFrameClass α)