Documentation

InfinitaryLogic.ModelTheory.Morleyization

Canonical definitional expansions (Morleyization) for a formula family #

Given an arity-tagged family Φ of L_{ω₁ω}-formulas over L, the language L.morleyize Φ keeps the whole base signature and adds one relation symbol R_φ of arity n for each ⟨n, φ⟩ ∈ Φ. Every L-structure has a canonical expansion (morleyExpansion) in which R_φ(a) holds iff φ(a) holds; nothing is chosen.

Universe boundary of the back-translation #

unMorleyize and realize_unMorleyize take their free-variable type in Type, not Type*: the substitution API BoundedFormulaω.subst shares one universe between its source and target variable types, and the bound-variable slots being substituted are Fin n : Type. Sentences and finite tuples are covered; the language and carrier universes stay general. The rest of the module is universe-polymorphic in the usual way.

What the witness-free claim rests on #

Function symbols are unchanged and every new relation symbol is interpreted by the complete satisfaction proposition of its formula, so the canonical expansion selects nothing. The isomorphism lift carries the given bijection (morleyEquiv_toEquiv); that theorem certifies that the lift chooses no new bijection, and the construction certifies the rest.

These are infinitary definitions when Φ contains infinitary formulas; they are not a first-order presentation with omitted types (Marker, Lectures on Infinitary Model Theory, Cambridge, 2016, Theorem 1.2.1 and Exercise 1.2.2, for that classical construction). No closure of Φ is assumed: Φ is any set of tagged formulas, and no fragment structure is required merely to name them. Coded structures, Borelness of the expansion map, and refined topologies are separate.

The expanded language #

source
def FirstOrder.Language.DefinedSym {L : Language} (Φ : Set ((n : ℕ) × L.BoundedFormulaω Empty n)) (n : ℕ) :
Type (max u v)

The defined-relation symbols of arity n: the members of Φ at arity n.

Equations
Instances For
    source
    def FirstOrder.Language.morleyize (L : Language) (Φ : Set ((n : ℕ) × L.BoundedFormulaω Empty n)) :
    Language

    The Morleyization of L by Φ: the base signature retained, one new relation symbol per member of Φ, at that member's arity.

    Equations
    Instances For
      source
      def FirstOrder.Language.lhomMorleyize {L : Language} (Φ : Set ((n : ℕ) × L.BoundedFormulaω Empty n)) :
      L →ᴸ L.morleyize Φ

      The inclusion of the base language.

      Equations
      Instances For
        source
        instance FirstOrder.Language.morleyize_isRelational {L : Language} (Φ : Set ((n : ℕ) × L.BoundedFormulaω Empty n)) [L.IsRelational] :
        (L.morleyize Φ).IsRelational

        The canonical expansion #

        source
        @[instance_reducible]
        def FirstOrder.Language.morleyExpansion {L : Language} (Φ : Set ((n : ℕ) × L.BoundedFormulaω Empty n)) (M : Type w) [L.Structure M] :
        (L.morleyize Φ).Structure M

        The canonical expansion: base symbols as before, R_φ(a) iff φ(a).

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          theorem FirstOrder.Language.relMap_morleyExpansion_inl {L : Language} {Φ : Set ((n : ℕ) × L.BoundedFormulaω Empty n)} {M : Type w} [L.Structure M] {n : ℕ} (R : L.Relations n) (x : Fin n → M) :
          Structure.RelMap (Sum.inl R) x = Structure.RelMap R x
          source
          theorem FirstOrder.Language.relMap_morleyExpansion_inr {L : Language} {Φ : Set ((n : ℕ) × L.BoundedFormulaω Empty n)} {M : Type w} [L.Structure M] {n : ℕ} (φ : DefinedSym Φ n) (x : Fin n → M) :
          Structure.RelMap (Sum.inr φ) x = (↑φ).Realize Empty.elim x

          The truth lemma for a defined symbol, definitional.

          source
          theorem FirstOrder.Language.isExpansionOn_morleyExpansion {L : Language} {Φ : Set ((n : ℕ) × L.BoundedFormulaω Empty n)} {M : Type w} [L.Structure M] :
          (lhomMorleyize Φ).IsExpansionOn M

          The canonical expansion is an expansion along the inclusion.

          source
          theorem FirstOrder.Language.reduct_morleyExpansion {L : Language} {Φ : Set ((n : ℕ) × L.BoundedFormulaω Empty n)} {M : Type w} [L.Structure M] :
          (lhomMorleyize Φ).reduct M = inst✝

          Reduct after expansion is the identity, definitionally.

          The defining axioms and uniqueness #

          source
          def FirstOrder.Language.alls {L' : Language} {n : ℕ} :
          L'.BoundedFormulaω Empty n → L'.Sentenceω

          Universal closure of all bound variables.

          Equations
          Instances For
            source
            theorem FirstOrder.Language.realize_alls {L' : Language} {N : Type w'} [L'.Structure N] {n : ℕ} (φ : L'.BoundedFormulaω Empty n) :
            (alls φ).Realize N ↔ ∀ (xs : Fin n → N), φ.Realize Empty.elim xs
            source
            def FirstOrder.Language.liftTerm {L : Language} (Φ : Set ((n : ℕ) × L.BoundedFormulaω Empty n)) {β : Type u_1} :
            L.Term β → (L.morleyize Φ).Term β

            Base terms as expanded-language terms: the function symbols are the same.

            Equations
            Instances For
              source
              def FirstOrder.Language.liftMorleyize {L : Language} (Φ : Set ((n : ℕ) × L.BoundedFormulaω Empty n)) {α : Type u_1} {k : ℕ} :
              L.BoundedFormulaω α k → (L.morleyize Φ).BoundedFormulaω α k

              Base formulas read in the expanded language: the structural relabelling of symbols along the inclusion. (mapLanguage is stated for a target in the same universes as L; the expanded language lives in Language.{u, max u v}.)

              Equations
              Instances For
                source
                theorem FirstOrder.Language.realize_liftTerm_of_isExpansionOn {L : Language} {Φ : Set ((n : ℕ) × L.BoundedFormulaω Empty n)} {M : Type w} [L.Structure M] {S : (L.morleyize Φ).Structure M} (hS : (lhomMorleyize Φ).IsExpansionOn M) {β : Type u_1} (t : L.Term β) (w : β → M) :
                Term.realize w (liftTerm Φ t) = Term.realize w t

                Over any expansion along the inclusion, lifted terms realize as in the base.

                source
                theorem FirstOrder.Language.realize_liftMorleyize_of_isExpansionOn {L : Language} {Φ : Set ((n : ℕ) × L.BoundedFormulaω Empty n)} {M : Type w} [L.Structure M] {S : (L.morleyize Φ).Structure M} (hS : (lhomMorleyize Φ).IsExpansionOn M) {α : Type u_1} {k : ℕ} (φ : L.BoundedFormulaω α k) (v : α → M) (xs : Fin k → M) :
                (liftMorleyize Φ φ).Realize v xs ↔ φ.Realize v xs

                Over any expansion along the inclusion, lifted formulas realize as in the base.

                source
                theorem FirstOrder.Language.realize_liftMorleyize {L : Language} {Φ : Set ((n : ℕ) × L.BoundedFormulaω Empty n)} {M : Type w} [L.Structure M] {α : Type u_1} {k : ℕ} (φ : L.BoundedFormulaω α k) (v : α → M) (xs : Fin k → M) :
                (liftMorleyize Φ φ).Realize v xs ↔ φ.Realize v xs

                Over the canonical expansion, lifted formulas realize as in the base.

                source
                def FirstOrder.Language.definingAxiom {L : Language} (Φ : Set ((n : ℕ) × L.BoundedFormulaω Empty n)) {n : ℕ} (φ : DefinedSym Φ n) :
                (L.morleyize Φ).Sentenceω

                The defining axiom of a defined symbol: ∀x̄ (R_φ(x̄) ↔ φ(x̄)), with φ read in the expanded language along the inclusion.

                Equations
                • One or more equations did not get rendered due to their size.
                Instances For
                  source
                  def FirstOrder.Language.definingTheory {L : Language} (Φ : Set ((n : ℕ) × L.BoundedFormulaω Empty n)) :
                  (L.morleyize Φ).Theoryω

                  The defining theory: all defining axioms.

                  Equations
                  Instances For
                    source
                    theorem FirstOrder.Language.morleyExpansion_model_definingTheory {L : Language} {Φ : Set ((n : ℕ) × L.BoundedFormulaω Empty n)} {M : Type w} [L.Structure M] :
                    (definingTheory Φ).Model M

                    The canonical expansion satisfies the defining theory.

                    source
                    theorem FirstOrder.Language.eq_morleyExpansion_of_model_definingTheory {L : Language} {Φ : Set ((n : ℕ) × L.BoundedFormulaω Empty n)} {M : Type w} [L.Structure M] (S : (L.morleyize Φ).Structure M) (hS : (lhomMorleyize Φ).IsExpansionOn M) (hax : (definingTheory Φ).Model M) :
                    S = morleyExpansion Φ M

                    Uniqueness: an expansion along the inclusion that satisfies the defining theory is the canonical expansion.

                    Back-translation #

                    source
                    def FirstOrder.Language.unMorleyize {L : Language} {Φ : Set ((n : ℕ) × L.BoundedFormulaω Empty n)} {α : Type} {k : ℕ} :
                    (L.morleyize Φ).BoundedFormulaω α k → L.BoundedFormulaω α k

                    The back-translation: each atom R_φ(t̄) becomes φ with t̄ substituted for its bound variable slots; everything else is structural.

                    Equations
                    Instances For
                      source
                      theorem FirstOrder.Language.realize_unMorleyize {L : Language} {Φ : Set ((n : ℕ) × L.BoundedFormulaω Empty n)} {M : Type w} [L.Structure M] {α : Type} {k : ℕ} (ψ : (L.morleyize Φ).BoundedFormulaω α k) (v : α → M) (xs : Fin k → M) :
                      (unMorleyize ψ).Realize v xs ↔ ψ.Realize v xs

                      Realization equivalence: over the canonical expansion, a formula and its back-translation agree.

                      Isomorphism transport #

                      source
                      def FirstOrder.Language.morleyEquiv {L : Language} {M : Type w} [L.Structure M] (Φ : Set ((n : ℕ) × L.BoundedFormulaω Empty n)) {N : Type w} [L.Structure N] (e : L.Equiv M N) :
                      (L.morleyize Φ).Equiv M N

                      An L-isomorphism lifts to an isomorphism of the canonical expansions; no witnesses are selected.

                      Equations
                      Instances For
                        source
                        def FirstOrder.Language.morleyEquivRestrict {L : Language} {Φ : Set ((n : ℕ) × L.BoundedFormulaω Empty n)} {M : Type w} [L.Structure M] {N : Type w} [L.Structure N] (g : (L.morleyize Φ).Equiv M N) :
                        L.Equiv M N

                        Restriction: an isomorphism of the canonical expansions is an L-isomorphism with the same bijection, through the base symbols.

                        Equations
                        Instances For
                          source
                          theorem FirstOrder.Language.morleyEquivRestrict_toEquiv {L : Language} {Φ : Set ((n : ℕ) × L.BoundedFormulaω Empty n)} {M : Type w} [L.Structure M] {N : Type w} [L.Structure N] (g : (L.morleyize Φ).Equiv M N) :
                          (morleyEquivRestrict g).toEquiv = g.toEquiv
                          source
                          theorem FirstOrder.Language.nonempty_morleyEquiv_iff {L : Language} {Φ : Set ((n : ℕ) × L.BoundedFormulaω Empty n)} {M : Type w} [L.Structure M] {N : Type w} [L.Structure N] :
                          Nonempty ((L.morleyize Φ).Equiv M N) ↔ Nonempty (L.Equiv M N)

                          Isomorphism transport, both directions: the canonical expansions are isomorphic iff the base structures are.

                          source
                          theorem FirstOrder.Language.morleyEquiv_toEquiv {L : Language} {Φ : Set ((n : ℕ) × L.BoundedFormulaω Empty n)} {M : Type w} [L.Structure M] {N : Type w} [L.Structure N] (e : L.Equiv M N) :
                          (morleyEquiv Φ e).toEquiv = e.toEquiv

                          The lifted isomorphism has the given underlying bijection.