Documentation

LeanPool.InfinitaryLogic.Lomega1omega.Operations

Operations on Lω₁ω Formulas #

This file defines operations on Lω₁ω formulas including relabeling, casting, and substitution.

Main Definitions #

Implementation Notes #

These are the ω-facing operations, defined over BoundedFormulaInf ℕ. An operation that makes sense at an arbitrary branching carrier belongs upstream on BoundedFormulaInf; IndexCoding handles transport between carriers.

source
def FirstOrder.Language.insertLastBound {n : ℕ} :
Fin (n + 1) → Fin n ⊕ Fin 1

Maps the last variable of Fin (n+1) to a bound variable position, keeping the first n as free variables. Used for quantifying over the last position.

This function is used by openBounds (for the all case) and by existsLastVar/forallLastVar in Scott/Formula.lean.

Equations
Instances For
    source
    def FirstOrder.Language.BoundedFormulaω.castLE {L : Language} {α : Type u'} {m n : ℕ} (_h : m ≤ n) :
    L.BoundedFormulaω α m → L.BoundedFormulaω α n

    Casts a bounded formula to one with more bound variables.

    Equations
    Instances For
      source
      theorem FirstOrder.Language.BoundedFormulaω.realize_castLE_self {L : Language} {α : Type u'} {M : Type u_1} [L.Structure M] {n : ℕ} (φ : L.BoundedFormulaω α n) (h : n ≤ n) (v : α → M) (xs : Fin n → M) :
      (castLE h φ).Realize v xs ↔ φ.Realize v xs

      castLE over any proof h : n ≤ n preserves semantics. This handles the case where the proof term is not definitionally le_refl (e.g., constructed via rewriting or other means).

      source
      def FirstOrder.Language.BoundedFormulaω.relabelAux {α β : Type u'} {n : ℕ} (g : α → β ⊕ Fin n) (k : ℕ) :
      α ⊕ Fin k → β ⊕ Fin (n + k)

      A function to help relabel the variables in bounded formulas.

      Equations
      Instances For
        source
        def FirstOrder.Language.BoundedFormulaω.relabel {L : Language} {α β : Type u'} {n : ℕ} (g : α → β ⊕ Fin n) {k : ℕ} :
        L.BoundedFormulaω α k → L.BoundedFormulaω β (n + k)

        Relabels a bounded formula's free variables.

        Equations
        Instances For
          source
          theorem FirstOrder.Language.BoundedFormulaω.realize_relabel_sumInr {L : Language} {M : Type u_1} [L.Structure M] {n k : ℕ} (φ : L.BoundedFormulaω (Fin n) k) (xs : Fin (n + k) → M) :
          (relabel Sum.inr φ).Realize Empty.elim xs ↔ φ.Realize (xs ∘ Fin.castAdd k) (xs ∘ Fin.natAdd n)

          Realize commutes with relabel Sum.inr: relabeling free variables Fin n into bound positions via Sum.inr shifts them into the first n bound variable slots.

          For φ : L.BoundedFormulaω (Fin n) k:

          • The relabeled formula φ.relabel Sum.inr has type L.BoundedFormulaω Empty (n + k)
          • Realizing with Empty.elim and xs : Fin (n + k) → M is equivalent to realizing the original formula with xs ∘ Fin.castAdd k for free variables and xs ∘ Fin.natAdd n for bound variables.
          source
          theorem FirstOrder.Language.BoundedFormulaω.realize_relabel_sumInr_zero {L : Language} {M : Type u_1} [L.Structure M] {n : ℕ} (φ : L.Formulaω (Fin n)) (xs : Fin n → M) :
          (relabel Sum.inr φ).Realize Empty.elim xs ↔ φ.Realize xs

          Specialization of realize_relabel_sumInr for formulas (k = 0 bound variables).

          For φ : L.Formulaω (Fin n) (a formula with n free variables and 0 bound variables):

          • φ.relabel Sum.inr : L.BoundedFormulaω Empty n has 0 free vars and n bound vars
          • Realizing the relabeled formula with bound assignment xs : Fin n → M is equivalent to realizing the original formula with free variable assignment xs.
          source
          def FirstOrder.Language.BoundedFormulaω.subst {L : Language} {α β : Type u'} {n : ℕ} :
          L.BoundedFormulaω α n → (α → L.Term β) → L.BoundedFormulaω β n

          Substitutes the free variables in a bounded formula with terms.

          Equations
          Instances For
            source
            @[simp]
            theorem FirstOrder.Language.BoundedFormulaω.realize_subst {L : Language} {α β : Type u'} {n : ℕ} {M : Type u_2} [L.Structure M] (tf : α → L.Term β) (φ : L.BoundedFormulaω α n) (v : β → M) (xs : Fin n → M) :
            (φ.subst tf).Realize v xs ↔ φ.Realize (fun (a : α) => Term.realize v (tf a)) xs

            Realization commutes with free variable substitution.

            This is the Lω₁ω analogue of Mathlib's BoundedFormula.realize_subst.

            source
            def FirstOrder.Language.BoundedFormulaω.openBounds {L : Language} {n : ℕ} :
            L.BoundedFormulaω Empty n → L.Formulaω (Fin n)

            Convert a BoundedFormulaω Empty n to a Formulaω (Fin n) by reinterpreting bound variables as free variables. Since there are no free variables (Empty), the bound variables Fin n become the only variables, now treated as free.

            For the all case, the last free variable is re-bound using relabel with insertLastBound.

            Equations
            Instances For

              Bridge: openBounds ∘ relabel Sum.inr roundtrip #

              Language Maps #

              source
              def FirstOrder.Language.BoundedFormulaω.mapLanguage {L : Language} {α : Type u'} {L' : Language} (g : L →ᴸ L') {n : ℕ} :
              L.BoundedFormulaω α n → L'.BoundedFormulaω α n

              Lifts a bounded Lω₁ω formula along a language homomorphism L →ᴸ L'.

              This maps function and relation symbols in the formula using the language homomorphism, while preserving the variable structure. It is the Lω₁ω analogue of Mathlib's LHom.onBoundedFormula.

              Equations
              Instances For
                source
                theorem FirstOrder.Language.BoundedFormulaω.realize_mapLanguage {L : Language} {α : Type u'} {n : ℕ} {L' : Language} (g : L →ᴸ L') {M : Type u_2} [L.Structure M] [L'.Structure M] [g.IsExpansionOn M] (φ : L.BoundedFormulaω α n) (v : α → M) (xs : Fin n → M) :
                (mapLanguage g φ).Realize v xs ↔ φ.Realize v xs

                Realization of a formula is preserved by language homomorphisms that are expansions.

                If g : L →ᴸ L' is an expansion on M (i.e., g maps symbols to the corresponding symbols in M's L'-structure), then (φ.mapLanguage g).Realize v xs ↔ φ.Realize v xs where the left side uses the L'-structure and the right side uses the L-structure.

                source
                @[simp]
                theorem FirstOrder.Language.BoundedFormulaω.mapLanguage_not {L : Language} {α : Type u'} {n : ℕ} {L' : Language} (g : L →ᴸ L') (φ : L.BoundedFormulaω α n) :
                mapLanguage g φ.not = (mapLanguage g φ).not

                mapLanguage commutes with not.

                source
                @[simp]
                theorem FirstOrder.Language.BoundedFormulaω.mapLanguage_imp {L : Language} {α : Type u'} {n : ℕ} {L' : Language} (g : L →ᴸ L') (φ ψ : L.BoundedFormulaω α n) :
                mapLanguage g (φ.imp ψ) = (mapLanguage g φ).imp (mapLanguage g ψ)

                mapLanguage commutes with imp.

                Closed-term substitution #

                source
                theorem FirstOrder.Language.term_subst_empty_aux {L : Language} (t t' : L.Term Empty) :
                (Term.relabel (Sum.inl ∘ Empty.elim) t).subst (Sum.elim (Term.relabel Sum.inl ∘ fun (x : Fin 1) => t') (var ∘ Sum.inr)) = Term.relabel Sum.inl t

                Substituting a closed term into a term with no real variables reduces to the plain relabel. Shared by the maximal-consistency term model and the proof-theoretic consistency family; it lives here so that neither needs to import the other.

                source
                def FirstOrder.Language.BoundedFormula.toLω {L : Language} {α : Type u'} {n : ℕ} :
                L.BoundedFormula α n → L.BoundedFormulaω α n

                Embeds a first-order bounded formula into Lω₁ω.

                Equations
                Instances For
                  source
                  @[simp]
                  theorem FirstOrder.Language.BoundedFormula.realize_toLω {L : Language} {α : Type u'} {n : ℕ} {M : Type u_1} [L.Structure M] {v : α → M} {xs : Fin n → M} (φ : L.BoundedFormula α n) :
                  φ.toLω.Realize v xs ↔ φ.Realize v xs
                  source
                  def FirstOrder.Language.Formula.toLω {L : Language} {α : Type u'} (φ : L.Formula α) :
                  L.Formulaω α

                  Embeds a first-order formula into Lω₁ω.

                  Equations
                  Instances For
                    source
                    @[simp]
                    theorem FirstOrder.Language.Formula.realize_toLω {L : Language} {α : Type u'} {M : Type u_1} [L.Structure M] {v : α → M} (φ : L.Formula α) :
                    φ.toLω.Realize v ↔ φ.Realize v
                    source
                    def FirstOrder.Language.Sentence.toLω {L : Language} (φ : L.Sentence) :
                    L.Sentenceω

                    Embeds a first-order sentence into Lω₁ω.

                    Equations
                    Instances For
                      source
                      @[simp]
                      theorem FirstOrder.Language.Sentence.realize_toLω {L : Language} {M : Type u_1} [L.Structure M] [_nonemptyM : Nonempty M] (φ : L.Sentence) :
                      φ.toLω.Realize M ↔ M ⊨ φ