Documentation

Foundation.Modal.VanBentham.StandardTranslation

source
inductive LO.FirstOrder.Language.Frame.Rel :
ℕ → Type
  • pred : ℕ → Rel 1

    propositional variable

  • lt : Rel 2

    binary relation

Instances For
    source
    @[reducible]
    def LO.FirstOrder.Language.frame :
    Language

    Language of Kripke frame for basic modal logic.

    Equations
    Instances For
      source
      def LO.FirstOrder.Language.term𝓛𝓕 :
      Lean.ParserDescr
      Equations
      Instances For
        source
        instance LO.FirstOrder.Language.instLTFrame :
        𝓛𝓕.LT
        Equations
        source
        def LO.FirstOrder.Frame.forces (a : ℕ) :
        Semiformula.Operator 𝓛𝓕 1
        Equations
        Instances For
          source
          def LO.FirstOrder.Frame.«first_order_formula_⊩_» :
          Lean.ParserDescr
          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            source
            def LO.FirstOrder.Frame.transitive :
            Sentence 𝓛𝓕
            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              source
              def LO.FirstOrder.Frame.monotone (a : ℕ) :
              Sentence 𝓛𝓕
              Equations
              • One or more equations did not get rendered due to their size.
              Instances For
                source
                def LO.Modal.standardTranslation :
                NNFormula ℕ → FirstOrder.Semisentence 𝓛𝓕 1
                Equations
                Instances For
                  source
                  def LO.Modal.«term_¹» :
                  Lean.TrailingParserDescr
                  Equations
                  Instances For
                    source
                    instance LO.Modal.Kripke.FirstOrder.instStructureFrameWorld {M : Model} :
                    FirstOrder.Structure 𝓛𝓕 M.World
                    Equations
                    • One or more equations did not get rendered due to their size.
                    source
                    @[simp]
                    theorem LO.Modal.Kripke.FirstOrder.forces_iff_val {M : Model} {x : M.World} {a : ℕ} :
                    (FirstOrder.Frame.forces a).val ![x] ↔ M.Val x a
                    source
                    @[simp]
                    theorem LO.Modal.Kripke.FirstOrder.lt_iff_rel {M : Model} {x y : M.World} :
                    op(<).val ![x, y] ↔ x ≺ y
                    source
                    theorem LO.Modal.Kripke.FirstOrder.correspondence_satisfies {M : Model} {x : M.World} {φ : NNFormula ℕ} :
                    x ⊧ φ ↔ M.World ⊧/![x] φ¹

                    BdRV Prop 2.47 (i)

                    source
                    theorem LO.Modal.Kripke.FirstOrder.correspondence_validOnModel {M : Model} {φ : NNFormula ℕ} :
                    M ⊧ φ ↔ M.World ⊧ₘ ∀' φ¹

                    BdRV Prop 2.47 (ii)