Documentation

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ω.castLE_refl {L : Language} {α : Type u'} {n : ℕ} (φ : L.BoundedFormulaω α n) :
      castLE ⋯ φ = φ

      castLE (le_refl n) is the identity on formulas.

      source
      theorem FirstOrder.Language.BoundedFormulaω.realize_castLE_of_eq {L : Language} {α : Type u'} {M : Type u_1} [L.Structure M] {m n : ℕ} (φ : L.BoundedFormulaω α m) (h : m ≤ n) (heq : m = n) (v : α → M) (xs : Fin n → M) :
      (castLE h φ).Realize v xs ↔ φ.Realize v (xs ∘ Fin.cast heq)

      castLE over a proof of m ≤ m preserves semantics. This is more general than matching on le_refl directly, as it works for any proof h : m ≤ m regardless of how it was constructed.

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

      castLE (le_refl n) preserves semantics.

      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
            def FirstOrder.Language.BoundedFormulaω.mapFreeVars {L : Language} {α β : Type u'} (f : α → β) {n : ℕ} :
            L.BoundedFormulaω α n → L.BoundedFormulaω β n

            Renames free variables in a bounded formula using a function f : α → β.

            Unlike relabel, which can move free variables into bound positions, mapFreeVars simply renames free variables while preserving the bound variable structure.

            Equations
            Instances For
              source
              theorem FirstOrder.Language.BoundedFormulaω.realize_mapFreeVars {L : Language} {α β : Type u'} {n : ℕ} {M : Type u_2} [L.Structure M] (f : α → β) (φ : L.BoundedFormulaω α n) (v : β → M) (xs : Fin n → M) :
              (mapFreeVars f φ).Realize v xs ↔ φ.Realize (v ∘ f) xs

              Realization commutes with free variable renaming.

              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 #

                source
                theorem FirstOrder.Language.BoundedFormulaω.castLE_self {L : Language} {α : Type u'} {n : ℕ} (φ : L.BoundedFormulaω α n) (h : n ≤ n) :
                castLE h φ = φ

                castLE h φ = φ for any proof h : n ≤ n, not just le_refl.

                source
                theorem FirstOrder.Language.BoundedFormulaω.castLE_eq_cast {L : Language} {α : Type u'} {n m : ℕ} (φ : L.BoundedFormulaω α m) (h : m ≤ n) (heq : m = n) :
                castLE h φ = heq ▸ φ

                castLE with a proof of m = n is transport.

                source
                theorem FirstOrder.Language.BoundedFormulaω.insertLastBound_eq_finSumFinEquiv_symm (n : ℕ) :
                insertLastBound = ⇑finSumFinEquiv.symm

                insertLastBound is the inverse of finSumFinEquiv restricted to splitting the last element of Fin (n+1) into Fin n ⊕ Fin 1.

                source
                theorem FirstOrder.Language.BoundedFormulaω.relabel_insertLastBound_comp_finSumFinEquiv {L : Language} (n k : ℕ) {l : ℕ} (φ : L.BoundedFormulaω (Fin (n + k + 1)) l) :
                relabel (fun (i : Fin (n + k)) => finSumFinEquiv.symm i) (relabel insertLastBound φ) = castLE ⋯ (relabel (fun (i : Fin (n + k + 1)) => finSumFinEquiv.symm i) φ)

                Composing relabel insertLastBound and relabel finSumFinEquiv.symm at the formula level.

                source
                theorem FirstOrder.Language.BoundedFormulaω.relabel_finSumFinEquiv_symm_zero {L : Language} {n : ℕ} (φ : L.Formulaω (Fin n)) :
                relabel (fun (i : Fin (n + 0)) => finSumFinEquiv.symm i) φ = φ

                relabel (fun i => finSumFinEquiv.symm i) at k = 0 is the identity, since finSumFinEquiv.symm : Fin n → Fin n ⊕ Fin 0 maps everything to Sum.inl.

                source
                theorem FirstOrder.Language.BoundedFormulaω.openBounds_relabel_sumInr {L : Language} {n : ℕ} (φ : L.Formulaω (Fin n)) :
                (relabel Sum.inr φ).openBounds = φ

                Roundtrip: openBounds after relabel Sum.inr is the identity on Formulaω (Fin n).

                This bridges between the two representations of a formula with one free variable: BoundedFormulaω Empty 1 (free variable as bound) and Formulaω (Fin 1) (free variable as free). Used to connect the proof system's all_elim with ConsistencyPropertyEq's C7.

                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.

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

                  mapLanguage commutes with ex.

                  source
                  theorem FirstOrder.Language.BoundedFormulaω.LHom.onTerm_relabel {L L' : Language} (g : L →ᴸ L') {γ : Type u_2} {δ : Type u_3} (f : γ → δ) (t : L.Term γ) :
                  g.onTerm (Term.relabel f t) = Term.relabel f (g.onTerm t)

                  LHom.onTerm commutes with Term.relabel.

                  source
                  theorem FirstOrder.Language.BoundedFormulaω.LHom.onTerm_subst {L L' : Language} (g : L →ᴸ L') {γ : Type u_2} {δ : Type u_3} (tf : γ → L.Term δ) (t : L.Term γ) :
                  g.onTerm (t.subst tf) = (g.onTerm t).subst fun (a : γ) => g.onTerm (tf a)

                  LHom.onTerm commutes with Term.subst.

                  source
                  theorem FirstOrder.Language.BoundedFormulaω.mapLanguage_castLE {L : Language} {α : Type u'} {n m : ℕ} {L' : Language} (g : L →ᴸ L') (h : m ≤ n) (φ : L.BoundedFormulaω α m) :
                  mapLanguage g (castLE h φ) = castLE h (mapLanguage g φ)

                  mapLanguage commutes with castLE.

                  source
                  theorem FirstOrder.Language.BoundedFormulaω.mapLanguage_relabel {L : Language} {α : Type u'} {n m : ℕ} {L' : Language} (g : L →ᴸ L') {γ : Type u'} (f : α → γ ⊕ Fin n) (φ : L.BoundedFormulaω α m) :
                  mapLanguage g (relabel f φ) = relabel f (mapLanguage g φ)

                  mapLanguage commutes with relabel.

                  source
                  theorem FirstOrder.Language.BoundedFormulaω.mapLanguage_subst {L : Language} {α β : Type u'} {n : ℕ} {L' : Language} (g : L →ᴸ L') (tf : α → L.Term β) (φ : L.BoundedFormulaω α n) :
                  mapLanguage g (φ.subst tf) = (mapLanguage g φ).subst fun (a : α) => g.onTerm (tf a)

                  mapLanguage commutes with subst.

                  source
                  def FirstOrder.Language.Formulaω.toSentenceω {L : Language} (φ : L.Formulaω (Fin 0)) :
                  L.Sentenceω

                  Converts a formula with Fin 0 free variables to a sentence (with Empty free variables).

                  Since both Fin 0 and Empty are empty types, this is a purely type-theoretic conversion that does not change the semantics of the formula.

                  Equations
                  Instances For
                    source
                    theorem FirstOrder.Language.Formulaω.realize_toSentenceω {L : Language} {M : Type u_1} [L.Structure M] (φ : L.Formulaω (Fin 0)) :
                    φ.toSentenceω.Realize M ↔ φ.Realize Fin.elim0

                    toSentenceω preserves semantics: the sentence realizes in M iff the original formula realizes with the Fin.elim0 assignment.

                    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] [Nonempty M] (φ : L.Sentence) :
                          φ.toLω.Realize M ↔ M ⊨ φ