Documentation

Mathlib.ModelTheory.Infinitary.Reindex

Carrier transport for infinitary formulas #

Infinitary formulas fix one branching carrier per formula (Infinitary/Syntax.lean); this file provides the transport layer between carriers, along IndexCodings:

Karp's theorem is the motivating consumer: its M-indexed and N-indexed separating conjunctions are iInfAlong at the two sum codings into the single carrier M ⊕ N.

source
def FirstOrder.Language.BoundedFormulaInf.iInfAlong {L : Language} {ι : Type uι} {κ : Type uκ} {α : Type u'} {n : ℕ} (c : IndexCoding ι κ) (φs : ι → L.BoundedFormulaInf κ α n) :
L.BoundedFormulaInf κ α n

An ι-indexed infinitary conjunction at carrier κ, along a coding: decoded indices select their conjunct, undecodable ones are padded with ⊤.

Equations
Instances For
    source
    def FirstOrder.Language.BoundedFormulaInf.iSupAlong {L : Language} {ι : Type uι} {κ : Type uκ} {α : Type u'} {n : ℕ} (c : IndexCoding ι κ) (φs : ι → L.BoundedFormulaInf κ α n) :
    L.BoundedFormulaInf κ α n

    An ι-indexed infinitary disjunction at carrier κ, along a coding: decoded indices select their disjunct, undecodable ones are padded with ⊥.

    Equations
    Instances For
      source
      def FirstOrder.Language.BoundedFormulaInf.reindex {L : Language} {ι : Type uι} {κ : Type uκ} {α : Type u'} (c : IndexCoding ι κ) {n : ℕ} :
      L.BoundedFormulaInf ι α n → L.BoundedFormulaInf κ α n

      Transport a formula along a coding of its carrier. Together with reindex_id and reindex_trans this makes carrier transport functorial; realize_reindex (in Infinitary/Semantics.lean) shows it is semantics-preserving.

      Equations
      Instances For
        source
        @[simp]
        theorem FirstOrder.Language.BoundedFormulaInf.reindex_falsum {L : Language} {ι : Type uι} {κ : Type uκ} {α : Type u'} {n : ℕ} (c : IndexCoding ι κ) :
        reindex c falsum = falsum
        source
        @[simp]
        theorem FirstOrder.Language.BoundedFormulaInf.reindex_equal {L : Language} {ι : Type uι} {κ : Type uκ} {α : Type u'} {n : ℕ} (c : IndexCoding ι κ) (t₁ t₂ : L.Term (α ⊕ Fin n)) :
        reindex c (equal t₁ t₂) = equal t₁ t₂
        source
        @[simp]
        theorem FirstOrder.Language.BoundedFormulaInf.reindex_rel {L : Language} {ι : Type uι} {κ : Type uκ} {α : Type u'} {n : ℕ} (c : IndexCoding ι κ) {l : ℕ} (R : L.Relations l) (ts : Fin l → L.Term (α ⊕ Fin n)) :
        reindex c (rel R ts) = rel R ts
        source
        @[simp]
        theorem FirstOrder.Language.BoundedFormulaInf.reindex_imp {L : Language} {ι : Type uι} {κ : Type uκ} {α : Type u'} {n : ℕ} (c : IndexCoding ι κ) (φ ψ : L.BoundedFormulaInf ι α n) :
        reindex c (φ.imp ψ) = (reindex c φ).imp (reindex c ψ)
        source
        @[simp]
        theorem FirstOrder.Language.BoundedFormulaInf.reindex_all {L : Language} {ι : Type uι} {κ : Type uκ} {α : Type u'} {n : ℕ} (c : IndexCoding ι κ) (φ : L.BoundedFormulaInf ι α (n + 1)) :
        reindex c φ.all = (reindex c φ).all
        source
        @[simp]
        theorem FirstOrder.Language.BoundedFormulaInf.reindex_iSup {L : Language} {ι : Type uι} {κ : Type uκ} {α : Type u'} {n : ℕ} (c : IndexCoding ι κ) (φs : ι → L.BoundedFormulaInf ι α n) :
        reindex c (iSup φs) = iSupAlong c fun (i : ι) => reindex c (φs i)
        source
        @[simp]
        theorem FirstOrder.Language.BoundedFormulaInf.reindex_iInf {L : Language} {ι : Type uι} {κ : Type uκ} {α : Type u'} {n : ℕ} (c : IndexCoding ι κ) (φs : ι → L.BoundedFormulaInf ι α n) :
        reindex c (iInf φs) = iInfAlong c fun (i : ι) => reindex c (φs i)
        source
        @[simp]
        theorem FirstOrder.Language.BoundedFormulaInf.reindex_not {L : Language} {ι : Type uι} {κ : Type uκ} {α : Type u'} {n : ℕ} (c : IndexCoding ι κ) (φ : L.BoundedFormulaInf ι α n) :
        reindex c φ.not = (reindex c φ).not
        source
        @[simp]
        theorem FirstOrder.Language.BoundedFormulaInf.reindex_ex {L : Language} {ι : Type uι} {κ : Type uκ} {α : Type u'} {n : ℕ} (c : IndexCoding ι κ) (φ : L.BoundedFormulaInf ι α (n + 1)) :
        reindex c φ.ex = (reindex c φ).ex
        source
        @[simp]
        theorem FirstOrder.Language.BoundedFormulaInf.reindex_top {L : Language} {ι : Type uι} {κ : Type uκ} {α : Type u'} {n : ℕ} (c : IndexCoding ι κ) :
        reindex c ⊤ = ⊤
        source
        @[simp]
        theorem FirstOrder.Language.BoundedFormulaInf.reindex_bot {L : Language} {ι : Type uι} {κ : Type uκ} {α : Type u'} {n : ℕ} (c : IndexCoding ι κ) :
        reindex c ⊥ = ⊥
        source
        theorem FirstOrder.Language.BoundedFormulaInf.reindex_id {L : Language} {ι : Type uι} {α : Type u'} {n : ℕ} (φ : L.BoundedFormulaInf ι α n) :
        reindex (IndexCoding.id ι) φ = φ

        Reindexing along the identity coding is syntactically the identity.

        source
        @[simp]
        theorem FirstOrder.Language.BoundedFormulaInf.reindex_alls {L : Language} {ι : Type uι} {κ : Type uκ} {α : Type u'} (c : IndexCoding ι κ) {n : ℕ} (φ : L.BoundedFormulaInf ι α n) :
        reindex c φ.alls = (reindex c φ).alls

        The universal bound-variable closure commutes with carrier transport, syntactically.

        source
        @[simp]
        theorem FirstOrder.Language.BoundedFormulaInf.reindex_exs {L : Language} {ι : Type uι} {κ : Type uκ} {α : Type u'} (c : IndexCoding ι κ) {n : ℕ} (φ : L.BoundedFormulaInf ι α n) :
        reindex c φ.exs = (reindex c φ).exs

        The existential bound-variable closure commutes with carrier transport, syntactically.

        source
        theorem FirstOrder.Language.BoundedFormulaInf.reindex_trans {L : Language} {ι : Type uι} {κ : Type uκ} {μ : Type uμ} {α : Type u'} (c₁ : IndexCoding ι κ) (c₂ : IndexCoding κ μ) {n : ℕ} (φ : L.BoundedFormulaInf ι α n) :
        reindex (c₁.trans c₂) φ = reindex c₂ (reindex c₁ φ)

        Reindexing along a composite coding is the composite of the reindexings — syntactically, not merely up to semantic equivalence. This is the coherence law that lets carrier transports be chained; it follows from the generic pad laws IndexCoding.pad_trans and IndexCoding.comp_pad, with no decoder analysis.

        source
        @[simp]
        theorem FirstOrder.Language.BoundedFormulaInf.reindex_ofEquiv_symm_reindex_ofEquiv {L : Language} {ι : Type uι} {κ : Type uκ} {α : Type u'} {n : ℕ} (e : ι ≃ κ) (φ : L.BoundedFormulaInf ι α n) :
        reindex (IndexCoding.ofEquiv e.symm) (reindex (IndexCoding.ofEquiv e) φ) = φ

        Equivalence codings give genuine syntactic transport: reindexing along an equivalence and back is the identity, syntactically. Instantiated at Equiv.ulift, this is the universe-lift operation on formulas together with its exact inverse — an arbitrary coding preserves semantics but pads; an equivalence coding round-trips.

        source
        def FirstOrder.Language.BoundedFormulaInf.reindexEquiv {L : Language} {ι : Type uι} {κ : Type uκ} {α : Type u'} {n : ℕ} (e : ι ≃ κ) :
        L.BoundedFormulaInf ι α n ≃ L.BoundedFormulaInf κ α n

        Carrier equivalences are actual syntax equivalences. In particular reindexEquiv Equiv.ulift.symm is the universe-lift operation on formulas, packaged with its exact syntactic inverse.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          def FirstOrder.Language.BoundedFormulaInf.toOmega {L : Language} {ι : Type uι} {α : Type u'} {n : ℕ} [Encodable ι] (φ : L.BoundedFormulaInf ι α n) :
          L.BoundedFormulaω α n

          Recode a formula over an encodable carrier into L_{ω₁ω}. No choice is involved; for a merely Countable carrier, obtain an Encodable instance via Encodable.ofCountable first. This is the uniform, whole-formula conversion; the formula-sensitive conversion from an IsCountable proof is ofCountable in Infinitary/Countability.lean.

          Equations
          Instances For
            source
            @[simp]
            theorem FirstOrder.Language.BoundedFormulaInf.realize_iInfAlong {L : Language} {ι : Type uι} {κ : Type uκ} {α : Type u'} {n : ℕ} {M : Type w} [L.Structure M] {v : α → M} {xs : Fin n → M} {c : IndexCoding ι κ} {φs : ι → L.BoundedFormulaInf κ α n} :
            (iInfAlong c φs).Realize v xs ↔ ∀ (i : ι), (φs i).Realize v xs

            The ⊤-padding of a coded conjunction is semantically neutral, generically in the coding.

            source
            @[simp]
            theorem FirstOrder.Language.BoundedFormulaInf.realize_iSupAlong {L : Language} {ι : Type uι} {κ : Type uκ} {α : Type u'} {n : ℕ} {M : Type w} [L.Structure M] {v : α → M} {xs : Fin n → M} {c : IndexCoding ι κ} {φs : ι → L.BoundedFormulaInf κ α n} :
            (iSupAlong c φs).Realize v xs ↔ ∃ (i : ι), (φs i).Realize v xs

            The ⊥-padding of a coded disjunction is semantically neutral, generically in the coding.

            source
            @[simp]
            theorem FirstOrder.Language.BoundedFormulaInf.realize_reindex {L : Language} {ι : Type uι} {κ : Type uκ} {α : Type u'} {M : Type w} [L.Structure M] (c : IndexCoding ι κ) {n : ℕ} (φ : L.BoundedFormulaInf ι α n) (v : α → M) (xs : Fin n → M) :
            (reindex c φ).Realize v xs ↔ φ.Realize v xs

            Carrier transport preserves realization. Being an iff, this transports semantic equivalence in both directions as well.

            source
            @[simp]
            theorem FirstOrder.Language.BoundedFormulaInf.realize_toOmega {L : Language} {ι : Type uι} {α : Type u'} {n : ℕ} {M : Type w} [L.Structure M] [Encodable ι] (φ : L.BoundedFormulaInf ι α n) (v : α → M) (xs : Fin n → M) :
            Realize φ.toOmega v xs ↔ φ.Realize v xs

            Recoding an encodable-carrier formula into L_{ω₁ω} preserves realization.

            source
            @[simp]
            theorem FirstOrder.Language.BoundedFormulaInf.reindex_toInf {L : Language} {ι : Type uι} {κ : Type uκ} {α : Type u'} (c : IndexCoding ι κ) {n : ℕ} (φ : L.BoundedFormula α n) :
            reindex c φ.toInf = φ.toInf

            Reindexing fixes the image of the finitary embedding: the finitary embedding at carrier κ factors through ANY coding into κ. This replaces the embedding-triangle lemma of a two-inductive design, and is syntactic.