@[reducible]
Language of Kripke frame for basic modal logic.
Equations
- 𝓛𝓕 = { Func := fun (x : ℕ) => PEmpty.{1}, Rel := LO.FirstOrder.Language.Frame.Rel }
Instances For
Equations
- LO.FirstOrder.Language.term𝓛𝓕 = Lean.ParserDescr.node `LO.FirstOrder.Language.term𝓛𝓕 1024 (Lean.ParserDescr.symbol "𝓛𝓕")
Instances For
Equations
Equations
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- (LO.Modal.NNFormula.atom a)¹ = (LO.FirstOrder.Frame.forces a).operator ![LO.FirstOrder.Semiterm.bvar 0]
- (LO.Modal.NNFormula.natom a)¹ = ∼(LO.FirstOrder.Frame.forces a).operator ![LO.FirstOrder.Semiterm.bvar 0]
- LO.Modal.NNFormula.verum¹ = ⊤
- LO.Modal.NNFormula.falsum¹ = ⊥
- (φ.and ψ)¹ = φ¹/[LO.FirstOrder.Semiterm.bvar 0] ⋏ ψ¹/[LO.FirstOrder.Semiterm.bvar 0]
- (φ.or ψ)¹ = φ¹/[LO.FirstOrder.Semiterm.bvar 0] ⋎ ψ¹/[LO.FirstOrder.Semiterm.bvar 0]
- φ.box¹ = (“∀' (!!(LO.FirstOrder.Semiterm.bvar 1) < !!(LO.FirstOrder.Semiterm.bvar 0) → !(φ¹/[LO.FirstOrder.Semiterm.bvar 0]))”)
- φ.dia¹ = (“∃' (!!(LO.FirstOrder.Semiterm.bvar 1) < !!(LO.FirstOrder.Semiterm.bvar 0) ∧ !(φ¹/[LO.FirstOrder.Semiterm.bvar 0]))”)
Instances For
Equations
- LO.Modal.«term_¹» = Lean.ParserDescr.trailingNode `LO.Modal.«term_¹» 1024 1024 (Lean.ParserDescr.symbol "¹")
Instances For
Equations
- One or more equations did not get rendered due to their size.