Documentation

InfinitaryLogic.Linf.Operations

Operations on L∞ω Formulas #

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

Main Definitions #

Implementation Notes #

The operations here (castLE, relabel, mapFreeVars, subst) closely mirror those in Lomega1omega/Operations.lean. The duplication exists because BoundedFormulaInf and BoundedFormulaω are separate inductive types: the former uses arbitrary {ι : Type uι} for iSup/iInf while the latter uses ℕ. Factoring into a shared abstraction would require a typeclass over the formula type, deferred for future work.

source
def FirstOrder.Language.BoundedFormulaInf.castLE {L : Language} {α : Type u'} {m n : ℕ} (_h : m ≤ n) :
L.BoundedFormulaInf α m → L.BoundedFormulaInf α n

Casts a bounded formula to one with more bound variables.

Equations
Instances For
    source
    theorem FirstOrder.Language.BoundedFormulaInf.castLE_refl {L : Language} {α : Type u'} {n : ℕ} (φ : L.BoundedFormulaInf α n) :
    castLE ⋯ φ = φ

    castLE (le_refl n) is the identity on formulas.

    source
    theorem FirstOrder.Language.BoundedFormulaInf.realize_castLE_of_eq {L : Language} {α : Type u'} {M : Type u_1} [L.Structure M] {m n : ℕ} (φ : L.BoundedFormulaInf α 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.BoundedFormulaInf.realize_castLE_refl {L : Language} {α : Type u'} {M : Type u_1} [L.Structure M] {n : ℕ} (φ : L.BoundedFormulaInf α n) (v : α → M) (xs : Fin n → M) :
    (castLE ⋯ φ).Realize v xs ↔ φ.Realize v xs

    castLE (le_refl n) preserves semantics.

    source
    theorem FirstOrder.Language.BoundedFormulaInf.realize_castLE_self {L : Language} {α : Type u'} {M : Type u_1} [L.Structure M] {n : ℕ} (φ : L.BoundedFormulaInf α 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.

    source
    def FirstOrder.Language.BoundedFormulaInf.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.BoundedFormulaInf.relabel {L : Language} {α β : Type u'} {n : ℕ} (g : α → β ⊕ Fin n) {k : ℕ} :
      L.BoundedFormulaInf α k → L.BoundedFormulaInf β (n + k)

      Relabels a bounded formula's free variables.

      Equations
      Instances For
        source
        def FirstOrder.Language.BoundedFormulaInf.mapFreeVars {L : Language} {α β : Type u'} (f : α → β) {n : ℕ} :
        L.BoundedFormulaInf α n → L.BoundedFormulaInf β 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.BoundedFormulaInf.realize_mapFreeVars {L : Language} {α β : Type u'} {n : ℕ} {M : Type u_2} [L.Structure M] (f : α → β) (φ : L.BoundedFormulaInf α n) (v : β → M) (xs : Fin n → M) :
          (mapFreeVars f φ).Realize v xs ↔ φ.Realize (v ∘ f) xs

          Realization commutes with free variable renaming.

          source
          def FirstOrder.Language.BoundedFormulaInf.subst {L : Language} {α β : Type u'} {n : ℕ} :
          L.BoundedFormulaInf α n → (α → L.Term β) → L.BoundedFormulaInf β n

          Substitutes the free variables in a bounded formula with terms.

          Equations
          Instances For

            Universe lifting for index types #

            source
            def FirstOrder.Language.BoundedFormulaInf.liftUI {L : Language} {α : Type u'} {n : ℕ} :
            L.BoundedFormulaInf α n → L.BoundedFormulaInf α n

            Lift a formula from index universe 0 to index universe w by ULifting each index type. This maps BoundedFormulaInf.{u,v,u',0} to BoundedFormulaInf.{u,v,u',w}, preserving semantics and quantifier rank.

            Equations
            Instances For
              source
              theorem FirstOrder.Language.BoundedFormulaInf.realize_liftUI {L : Language} {α : Type u'} {M : Type u_2} [L.Structure M] {n : ℕ} (φ : L.BoundedFormulaInf α n) (v : α → M) (xs : Fin n → M) :
              φ.liftUI.Realize v xs ↔ φ.Realize v xs

              Universe lifting preserves semantics.

              Quantifying over the last free variable #

              source
              def FirstOrder.Language.BoundedFormulaInf.existsLastVarInf {L : Language} {n : ℕ} (φ : L.FormulaInf (Fin (n + 1))) :
              L.FormulaInf (Fin n)

              Existentially quantify over the last free variable of an L∞ω formula.

              Equations
              Instances For
                source
                def FirstOrder.Language.BoundedFormulaInf.forallLastVarInf {L : Language} {n : ℕ} (φ : L.FormulaInf (Fin (n + 1))) :
                L.FormulaInf (Fin n)

                Universally quantify over the last free variable of an L∞ω formula.

                Equations
                Instances For
                  source
                  theorem FirstOrder.Language.BoundedFormulaInf.realize_existsLastVarInf {L : Language} {M : Type u_3} [L.Structure M] {n : ℕ} (φ : L.FormulaInf (Fin (n + 1))) (v : Fin n → M) :
                  (existsLastVarInf φ).Realize v ↔ ∃ (x : M), φ.Realize (Fin.snoc v x)

                  Semantics of existsLastVarInf: existentially quantifies over the last variable.

                  source
                  theorem FirstOrder.Language.BoundedFormulaInf.realize_forallLastVarInf {L : Language} {M : Type u_3} [L.Structure M] {n : ℕ} (φ : L.FormulaInf (Fin (n + 1))) (v : Fin n → M) :
                  (forallLastVarInf φ).Realize v ↔ ∀ (x : M), φ.Realize (Fin.snoc v x)

                  Semantics of forallLastVarInf: universally quantifies over the last variable.

                  source
                  def FirstOrder.Language.FormulaInf.toSentenceInf {L : Language} (φ : L.FormulaInf (Fin 0)) :
                  L.SentenceInf

                  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.FormulaInf.realize_toSentenceInf {L : Language} {M : Type u_1} [L.Structure M] (φ : L.FormulaInf (Fin 0)) :
                    φ.toSentenceInf.Realize M ↔ φ.Realize Fin.elim0

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

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

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

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

                      Embeds a first-order formula into L∞ω.

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

                        Embeds a first-order sentence into L∞ω.

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