Documentation

Linglib.Logic.Modal.FirstOrder.Correspondence

The correspondence language and the standard translation #

The standard translation of quantified modal logic into first-order logic, for an arbitrary signature: modal formulas over L translate into plain mathlib first-order formulas over the correspondence language L.correspondence — every symbol world-relativized to one arity higher, plus a binary accessibility relation and an individual-sort predicate — interpreted on the two-sorted-as-one carrier W ⊕ M. realize_st is satisfaction preservation.

Main declarations #

References #

The correspondence language #

source
def FirstOrder.Language.correspondence (L : Language) :
Language

The correspondence language of L has an (n + 1)-ary symbol for each n-ary L-symbol — the new first argument the world — together with an individual-sort predicate and an accessibility relation.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    @[reducible, inline]
    abbrev FirstOrder.Language.corrFunc {L : Language} {n : ℕ} (f : L.Functions n) :
    L.correspondence.Functions (n + 1)
    Equations
    Instances For
      source
      @[reducible, inline]
      abbrev FirstOrder.Language.corrRel {L : Language} {n : ℕ} (R : L.Relations n) :
      L.correspondence.Relations (n + 1)
      Instances For
        source
        @[reducible, inline]
        abbrev FirstOrder.Language.corrIndiv {L : Language} :
        L.correspondence.Relations 1

        The individual-sort predicate.

        Equations
        Instances For
          source
          @[reducible, inline]
          abbrev FirstOrder.Language.corrAcc {L : Language} :
          L.correspondence.Relations 2

          The accessibility relation symbol.

          Equations
          Instances For
            source
            @[reducible, inline]
            abbrev FirstOrder.Language.corrIndivVar {Var : Type u_3} {L : Language} (x : Var) :
            L.correspondence.Term (Var ⊕ ℕ)
            Equations
            Instances For
              source
              @[reducible, inline]
              abbrev FirstOrder.Language.corrWorldVar {Var : Type u_3} {L : Language} (k : ℕ) :
              L.correspondence.Term (Var ⊕ ℕ)
              Equations
              Instances For

                Sorted valuations #

                source
                def FirstOrder.Language.stVal {W : Type u_1} {M : Type u_2} {Var : Type u_3} (v : Var → M) (u : ℕ → W) :
                Var ⊕ ℕ → W ⊕ M

                The sorted valuation of an individual assignment v and a world assignment u. realize_st evaluates translations at these.

                Equations
                Instances For
                  source
                  @[simp]
                  theorem FirstOrder.Language.stVal_inl {W : Type u_1} {M : Type u_2} {Var : Type u_3} (v : Var → M) (u : ℕ → W) (x : Var) :
                  stVal v u (Sum.inl x) = Sum.inr (v x)
                  source
                  @[simp]
                  theorem FirstOrder.Language.stVal_inr {W : Type u_1} {M : Type u_2} {Var : Type u_3} (v : Var → M) (u : ℕ → W) (j : ℕ) :
                  stVal v u (Sum.inr j) = Sum.inl (u j)
                  source
                  theorem FirstOrder.Language.stVal_update_indiv {W : Type u_1} {M : Type u_2} {Var : Type u_3} [DecidableEq Var] (v : Var → M) (u : ℕ → W) (x : Var) (d : M) :
                  Function.update (stVal v u) (Sum.inl x) (Sum.inr d) = stVal (Function.update v x d) u

                  Updating an individual slot of a sorted valuation updates the individual assignment.

                  source
                  theorem FirstOrder.Language.stVal_update_world {W : Type u_1} {M : Type u_2} {Var : Type u_3} [DecidableEq Var] (v : Var → M) (u : ℕ → W) (j : ℕ) (w : W) :
                  Function.update (stVal v u) (Sum.inr j) (Sum.inl w) = stVal v (Function.update u j w)

                  Updating a world slot of a sorted valuation updates the world assignment.

                  The translation #

                  source
                  def FirstOrder.Language.stTerm {Var : Type u_3} {L : Language} (k : ℕ) :
                  L.Term Var → L.correspondence.Term (Var ⊕ ℕ)

                  stTerm translates terms: a variable stays put; a function symbol applies its world-relativized form at the current world variable.

                  Equations
                  Instances For
                    source
                    def FirstOrder.Language.ModalFormula.st {Var : Type u_3} {L : Language} [DecidableEq Var] (k : ℕ) :
                    L.ModalFormula Var → L.correspondence.Formula (Var ⊕ ℕ)

                    The standard translation ST_k of [BdRV01]. The current world is the free variable Sum.inr k; atoms world-relativize; box relativizes a fresh world variable Sum.inr (k + 1) along accessibility; quantifiers relativize to the individual sort.

                    Equations
                    Instances For

                      Sort-guarded sentence closure #

                      source
                      def FirstOrder.Language.stClose {Var : Type u_3} {L : Language} [DecidableEq Var] (k : ℕ) (ψ : L.correspondence.Formula (Var ⊕ ℕ)) :
                      L.correspondence.Formula (Var ⊕ ℕ)

                      stClose closes the current-world variable Sum.inr k under a sort-guarded existential, ∃z(¬IsIndiv(z) ∧ ψ). The guard is load-bearing on the mixed carrier — a bare ex₁ could be witnessed by a junk individual-as-world, which satisfies □⊥ vacuously.

                      Equations
                      Instances For
                        source
                        theorem FirstOrder.Language.realize_stClose {W : Type u_1} {M : Type u_2} {Var : Type u_3} {L : Language} [DecidableEq Var] [L.correspondence.Structure (W ⊕ M)] (k : ℕ) (ψ : L.correspondence.Formula (Var ⊕ ℕ)) (val : Var ⊕ ℕ → W ⊕ M) (hind : ∀ (z : W ⊕ M), Structure.RelMap corrIndiv ![z] ↔ ∃ (d : M), z = Sum.inr d) :
                        (stClose k ψ).Realize val ↔ ∃ (w : W), ψ.Realize (Function.update val (Sum.inr k) (Sum.inl w))

                        Over any correspondence structure on W ⊕ M whose individual-sort predicate holds exactly of the second summand — as ModalStructure.correspondence's does definitionally — the guarded witness of stClose is exactly a world.

                        The encoded structure #

                        source
                        @[instance_reducible]
                        def FirstOrder.Language.ModalStructure.correspondence {W : Type u_1} {M : Type u_2} {L : Language} [Inhabited M] (K : L.ModalStructure W M) :
                        L.correspondence.Structure (W ⊕ M)

                        K.correspondence encodes a modal structure as a single mathlib structure on W ⊕ M — the structure half of Language.correspondence: worlds and individuals share the carrier, sorted by corrIndiv; relational guards make all off-sort atoms false, and off-sort function arguments default.

                        Equations
                        • One or more equations did not get rendered due to their size.
                        Instances For
                          source
                          @[simp]
                          theorem FirstOrder.Language.correspondence_relMap_rel {W : Type u_1} {M : Type u_2} {L : Language} {n : ℕ} [Inhabited M] (K : L.ModalStructure W M) (R : L.Relations n) (z : Fin (n + 1) → W ⊕ M) :
                          Structure.RelMap (corrRel R) z ↔ ∃ (w : W) (ds : Fin n → M), z 0 = Sum.inl w ∧ (∀ (i : Fin n), z i.succ = Sum.inr (ds i)) ∧ K.relInterp R w ds
                          source
                          @[simp]
                          theorem FirstOrder.Language.correspondence_relMap_acc {W : Type u_1} {M : Type u_2} {L : Language} [Inhabited M] (K : L.ModalStructure W M) (z : Fin 2 → W ⊕ M) :
                          Structure.RelMap corrAcc z ↔ ∃ (w₁ : W) (w₂ : W), z 0 = Sum.inl w₁ ∧ z 1 = Sum.inl w₂ ∧ w₂ ∈ K.access w₁
                          source
                          @[simp]
                          theorem FirstOrder.Language.correspondence_relMap_indiv {W : Type u_1} {M : Type u_2} {L : Language} [Inhabited M] (K : L.ModalStructure W M) (z : Fin 1 → W ⊕ M) :
                          Structure.RelMap corrIndiv z ↔ ∃ (d : M), z 0 = Sum.inr d
                          source
                          theorem FirstOrder.Language.correspondence_funMap_inl {W : Type u_1} {M : Type u_2} {L : Language} {n : ℕ} [Inhabited M] (K : L.ModalStructure W M) (f : L.Functions n) (w : W) (z : Fin (n + 1) → W ⊕ M) (ds : Fin n → M) (hz : z 0 = Sum.inl w) (hds : ∀ (i : Fin n), z i.succ = Sum.inr (ds i)) :
                          Structure.funMap (corrFunc f) z = Sum.inr (K.funInterp f w ds)

                          Satisfaction preservation #

                          source
                          theorem FirstOrder.Language.realize_st {W : Type u_1} {M : Type u_2} {Var : Type u_3} {L : Language} [Inhabited M] (K : L.ModalStructure W M) [DecidableEq Var] {φ : L.ModalFormula Var} {k : ℕ} {v : Var → M} {u : ℕ → W} :
                          ModalFormula.Realize K (u k) φ v ↔ (ModalFormula.st k φ).Realize (stVal v u)

                          The standard translation preserves satisfaction. Kripke satisfaction at the world pinned at index k is first-order realization over K.correspondence at the sorted valuation. Off-sort quantifier instances are discharged by the relational guards, and box's fresh world variable k + 1 leaves index k untouched.