def LO.Modal.NNFormula.Kripke.Satisfies (M : Kripke.Model) (x : M.World) : 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 : Kripke.Model} : Semantics (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 {φ : NNFormula ℕ} {M : Kripke.Model} {x : M.World} : x ⊧ φ ↔ Satisfies M x φ

@[simp]

theorem LO.Modal.NNFormula.Kripke.Satisfies.atom_def {M : Kripke.Model} {x : M.World} (a : ℕ) : x ⊧ atom a ↔ M.Val x a

@[simp]

theorem LO.Modal.NNFormula.Kripke.Satisfies.natom_def {M : Kripke.Model} {x : M.World} (a : ℕ) : x ⊧ natom a ↔ ¬M.Val x a

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

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

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

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

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

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

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

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

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

def LO.Modal.NNFormula.Kripke.ValidOnModel (M : Kripke.Model) (φ : 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 : Semantics (NNFormula ℕ) 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 {φ : NNFormula ℕ} {M : Kripke.Model} : M ⊧ φ ↔ ValidOnModel M φ

def LO.Modal.NNFormula.Kripke.ValidOnFrame (F : Kripke.Frame) (φ : 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 : Semantics (NNFormula ℕ) 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 {φ : NNFormula ℕ} {F : Kripke.Frame} : F ⊧ φ ↔ ValidOnFrame F φ

def LO.Modal.NNFormula.Kripke.ValidOnFrameClass (C : Kripke.FrameClass) (φ : 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 : Semantics (NNFormula ℕ) 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 {φ : NNFormula ℕ} {C : Kripke.FrameClass} : C ⊧ φ ↔ ValidOnFrameClass C φ

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

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

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

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

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

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

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

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