def LO.Modal.NNFormula.Kripke.Satisfies (M : LO.Modal.Kripke.Model) (x : M.World) : LO.Modal.NNFormula ℕ → Prop

Equations

• LO.Modal.NNFormula.Kripke.Satisfies M x (LO.Modal.NNFormula.atom a) = M.Val x a
• LO.Modal.NNFormula.Kripke.Satisfies M x (LO.Modal.NNFormula.natom a) = ¬M.Val x a
• LO.Modal.NNFormula.Kripke.Satisfies M x LO.Modal.NNFormula.verum = True
• LO.Modal.NNFormula.Kripke.Satisfies M x LO.Modal.NNFormula.falsum = False
• LO.Modal.NNFormula.Kripke.Satisfies M x (φ.or ψ) = (LO.Modal.NNFormula.Kripke.Satisfies M x φ ∨ LO.Modal.NNFormula.Kripke.Satisfies M x ψ)
• LO.Modal.NNFormula.Kripke.Satisfies M x (φ.and ψ) = (LO.Modal.NNFormula.Kripke.Satisfies M x φ ∧ LO.Modal.NNFormula.Kripke.Satisfies M x ψ)
• LO.Modal.NNFormula.Kripke.Satisfies M x φ.box = ∀ (y : M.World), x ≺ y → LO.Modal.NNFormula.Kripke.Satisfies M y φ
• LO.Modal.NNFormula.Kripke.Satisfies M x φ.dia = ∃ (y : M.World), x ≺ y ∧ LO.Modal.NNFormula.Kripke.Satisfies M y φ

instance LO.Modal.NNFormula.Kripke.Satisfies.semantics {M : LO.Modal.Kripke.Model} : LO.Semantics (LO.Modal.NNFormula ℕ) M.World

Equations

• LO.Modal.NNFormula.Kripke.Satisfies.semantics = { Realize := fun (x : M.World) => LO.Modal.NNFormula.Kripke.Satisfies M x }

theorem LO.Modal.NNFormula.Kripke.Satisfies.iff_models {φ : LO.Modal.NNFormula ℕ} {M : LO.Modal.Kripke.Model} {x : M.World} : x ⊧ φ ↔ LO.Modal.NNFormula.Kripke.Satisfies M x φ

theorem LO.Modal.NNFormula.Kripke.Satisfies.top_def {M : LO.Modal.Kripke.Model} {x : M.World} : x ⊧ ⊤

theorem LO.Modal.NNFormula.Kripke.Satisfies.bot_def {M : LO.Modal.Kripke.Model} {x : M.World} : ¬x ⊧ ⊥

theorem LO.Modal.NNFormula.Kripke.Satisfies.or_def {φ ψ : LO.Modal.NNFormula ℕ} {M : LO.Modal.Kripke.Model} {x : M.World} : x ⊧ φ ⋎ ψ ↔ x ⊧ φ ∨ x ⊧ ψ

theorem LO.Modal.NNFormula.Kripke.Satisfies.and_def {φ ψ : LO.Modal.NNFormula ℕ} {M : LO.Modal.Kripke.Model} {x : M.World} : x ⊧ φ ⋏ ψ ↔ x ⊧ φ ∧ x ⊧ ψ

theorem LO.Modal.NNFormula.Kripke.Satisfies.box_def {φ : LO.Modal.NNFormula ℕ} {M : LO.Modal.Kripke.Model} {x : M.World} : x ⊧ □φ ↔ ∀ (y : M.World), x ≺ y → y ⊧ φ

theorem LO.Modal.NNFormula.Kripke.Satisfies.dia_def {φ : LO.Modal.NNFormula ℕ} {M : LO.Modal.Kripke.Model} {x : M.World} : x ⊧ ◇φ ↔ ∃ (y : M.World), x ≺ y ∧ y ⊧ φ

theorem LO.Modal.NNFormula.Kripke.Satisfies.neg_def {φ : LO.Modal.NNFormula ℕ} {M : LO.Modal.Kripke.Model} {x : M.World} : x ⊧ ∼φ ↔ ¬x ⊧ φ

theorem LO.Modal.NNFormula.Kripke.Satisfies.imp_def {φ ψ : LO.Modal.NNFormula ℕ} {M : LO.Modal.Kripke.Model} {x : M.World} : x ⊧ φ ➝ ψ ↔ x ⊧ φ → x ⊧ ψ

instance LO.Modal.NNFormula.Kripke.Satisfies.instTarskiWorldNat {M : LO.Modal.Kripke.Model} : LO.Semantics.Tarski M.World

Equations

• ⋯ = ⋯

def LO.Modal.NNFormula.Kripke.ValidOnModel (M : LO.Modal.Kripke.Model) (φ : LO.Modal.NNFormula ℕ) : Prop

Equations

• LO.Modal.NNFormula.Kripke.ValidOnModel M φ = ∀ (x : M.World), LO.Modal.NNFormula.Kripke.Satisfies M x φ

instance LO.Modal.NNFormula.Kripke.ValidOnModel.semantics : LO.Semantics (LO.Modal.NNFormula ℕ) LO.Modal.Kripke.Model

Equations

• LO.Modal.NNFormula.Kripke.ValidOnModel.semantics = { Realize := fun (M : LO.Modal.Kripke.Model) => LO.Modal.NNFormula.Kripke.ValidOnModel M }

@[simp]

theorem LO.Modal.NNFormula.Kripke.ValidOnModel.iff_models {φ : LO.Modal.NNFormula ℕ} {M : LO.Modal.Kripke.Model} : M ⊧ φ ↔ LO.Modal.NNFormula.Kripke.ValidOnModel M φ

def LO.Modal.NNFormula.Kripke.ValidOnFrame (F : LO.Modal.Kripke.Frame) (φ : LO.Modal.NNFormula ℕ) : Prop

Equations

• LO.Modal.NNFormula.Kripke.ValidOnFrame F φ = ∀ (V : LO.Modal.Kripke.Valuation F), { toFrame := F, Val := V } ⊧ φ

instance LO.Modal.NNFormula.Kripke.ValidOnFrame.semantics : LO.Semantics (LO.Modal.NNFormula ℕ) LO.Modal.Kripke.Frame

Equations

• LO.Modal.NNFormula.Kripke.ValidOnFrame.semantics = { Realize := fun (F : LO.Modal.Kripke.Frame) => LO.Modal.NNFormula.Kripke.ValidOnFrame F }

@[simp]

theorem LO.Modal.NNFormula.Kripke.ValidOnFrame.iff_models {φ : LO.Modal.NNFormula ℕ} {F : LO.Modal.Kripke.Frame} : F ⊧ φ ↔ LO.Modal.NNFormula.Kripke.ValidOnFrame F φ

def LO.Modal.NNFormula.Kripke.ValidOnFrameClass (C : LO.Modal.Kripke.FrameClass) (φ : LO.Modal.NNFormula ℕ) : Prop

Equations

• LO.Modal.NNFormula.Kripke.ValidOnFrameClass C φ = ∀ {F : LO.Modal.Kripke.Frame}, F ∈ C → LO.Modal.NNFormula.Kripke.ValidOnFrame F φ

instance LO.Modal.NNFormula.Kripke.ValidOnFrameClass.semantics : LO.Semantics (LO.Modal.NNFormula ℕ) LO.Modal.Kripke.FrameClass

Equations

• LO.Modal.NNFormula.Kripke.ValidOnFrameClass.semantics = { Realize := fun (C : LO.Modal.Kripke.FrameClass) => LO.Modal.NNFormula.Kripke.ValidOnFrameClass C }

@[simp]

theorem LO.Modal.NNFormula.Kripke.ValidOnFrameClass.iff_models {φ : LO.Modal.NNFormula ℕ} {C : LO.Modal.Kripke.FrameClass} : C ⊧ φ ↔ LO.Modal.NNFormula.Kripke.ValidOnFrameClass C φ

theorem LO.Modal.NNFormula.Kripke.Satisfies.toFormula {φ : LO.Modal.NNFormula ℕ} {M : LO.Modal.Kripke.Model} {x : M.World} : LO.Modal.NNFormula.Kripke.Satisfies M x φ ↔ LO.Modal.Formula.Kripke.Satisfies M x φ.toFormula

theorem LO.Modal.NNFormula.Kripke.ValidOnModel.toFormula {φ : LO.Modal.NNFormula ℕ} {M : LO.Modal.Kripke.Model} : LO.Modal.NNFormula.Kripke.ValidOnModel M φ ↔ LO.Modal.Formula.Kripke.ValidOnModel M φ.toFormula

theorem LO.Modal.NNFormula.Kripke.ValidOnFrame.toFormula {φ : LO.Modal.NNFormula ℕ} {F : LO.Modal.Kripke.Frame} : LO.Modal.NNFormula.Kripke.ValidOnFrame F φ ↔ LO.Modal.Formula.Kripke.ValidOnFrame F φ.toFormula

theorem LO.Modal.NNFormula.Kripke.ValidOnFrameClass.toFormula {φ : LO.Modal.NNFormula ℕ} {C : LO.Modal.Kripke.FrameClass} : LO.Modal.NNFormula.Kripke.ValidOnFrameClass C φ ↔ LO.Modal.Formula.Kripke.ValidOnFrameClass C φ.toFormula

theorem LO.Modal.Formula.Kripke.Satisfies.toNNFormula {φ : LO.Modal.Formula ℕ} {M : LO.Modal.Kripke.Model} {x : M.World} : LO.Modal.Formula.Kripke.Satisfies M x φ ↔ LO.Modal.NNFormula.Kripke.Satisfies M x φ.toNNFormula

theorem LO.Modal.Formula.Kripke.ValidOnModel.toNNFormula {φ : LO.Modal.Formula ℕ} {M : LO.Modal.Kripke.Model} : LO.Modal.Formula.Kripke.ValidOnModel M φ ↔ LO.Modal.NNFormula.Kripke.ValidOnModel M φ.toNNFormula

theorem LO.Modal.Formula.Kripke.ValidOnFrame.toNNFormula {φ : LO.Modal.Formula ℕ} {F : LO.Modal.Kripke.Frame} : LO.Modal.Formula.Kripke.ValidOnFrame F φ ↔ LO.Modal.NNFormula.Kripke.ValidOnFrame F φ.toNNFormula

theorem LO.Modal.Formula.Kripke.ValidOnFrameClass.toNNFormula {φ : LO.Modal.Formula ℕ} {C : LO.Modal.Kripke.FrameClass} : LO.Modal.Formula.Kripke.ValidOnFrameClass C φ ↔ LO.Modal.NNFormula.Kripke.ValidOnFrameClass C φ.toNNFormula