Abstracting constants out of terms

A term of the constant expansion L[[γ]] mentions only finitely many of the new constants, so it is obtained from a term of L by substituting a tuple of constants for its bound positions. In an expansion of an L-structure, such a term evaluates to the value of the term of L at the values of the constants.

Main results

• FirstOrder.Language.Term.exists_finite_forall_onTerm_subst_eq: the constants of a term of L[[γ]] lie in a finite set, and the term abstracts over every tuple listing that set.
• FirstOrder.Language.Term.exists_onTerm_subst_eq: every term of L[[γ]] without bound positions is obtained from a term of L by substituting constants for its bound positions.
• FirstOrder.Language.Term.realize_onTerm_subst_con: the value of such a term in an expansion.
• FirstOrder.Language.Term.exists_eq_con_of_isRelational: over a relational language, a closed term of L[[γ]] is a constant.
• FirstOrder.Language.coe_con_constantsOn_structure: in the expansion interpreting each constant c as e c, the constant L.con c is interpreted as e c.

@[simp]

theorem FirstOrder.Language.coe_con_constantsOn_structure {L : Language} {γ : Type w} {M : Type u_1} [L.Structure M] (e : γ → M) (c : γ) : ↑(L.con c) = e c

In the expansion of an L-structure interpreting each constant c of constantsOn γ as e c, the constant L.con c of L[[γ]] is interpreted as e c.

theorem FirstOrder.Language.Term.exists_finite_forall_onTerm_subst_eq {L : Language} {α : Type uα} {γ : Type w} (t : (L.withConstants γ).Term (α ⊕ Fin 0)) : ∃ (S : Set γ), S.Finite ∧ ∀ {n : ℕ} (c : Fin n → γ), S ⊆ Set.range c → ∃ (s : L.Term (α ⊕ Fin n)), ((L.lhomWithConstants γ).onTerm s).subst (Sum.elim (var ∘ Sum.inl) fun (i : Fin n) => (L.con (c i)).term) = t

Every term of L[[γ]] whose variables are free variables abstracts to a term of L: there is a finite set of constants such that, at every tuple listing them, the term is obtained from a term of L by substituting the constants of the tuple for its bound positions.

theorem FirstOrder.Language.Term.exists_onTerm_subst_eq {L : Language} {α : Type uα} {γ : Type w} (t : (L.withConstants γ).Term (α ⊕ Fin 0)) : ∃ (n : ℕ) (s : L.Term (α ⊕ Fin n)) (c : Fin n → γ), ((L.lhomWithConstants γ).onTerm s).subst (Sum.elim (var ∘ Sum.inl) fun (i : Fin n) => (L.con (c i)).term) = t

Terms abstract their constants: a term of L[[γ]] whose variables are free variables is obtained from a term of L by substituting a tuple of constants for its bound positions.

theorem FirstOrder.Language.Term.exists_eq_con_of_isRelational {L : Language} {α : Type uα} {γ : Type w} [L.IsRelational] [IsEmpty α] (t : (L.withConstants γ).Term (α ⊕ Fin 0)) : ∃ (c : γ), t = (L.con c).term

Over a relational language, a term of L[[γ]] without variables is one of the constants.

theorem FirstOrder.Language.Term.realize_onTerm_subst_con {L : Language} {α : Type uα} {γ : Type w} {M : Type u_1} [L.Structure M] [(L.withConstants γ).Structure M] [(L.lhomWithConstants γ).IsExpansionOn M] {n : ℕ} (s : L.Term (α ⊕ Fin n)) (c : Fin n → γ) (v : α → M) (xs : Fin 0 → M) : realize (Sum.elim v xs) (((L.lhomWithConstants γ).onTerm s).subst (Sum.elim (var ∘ Sum.inl) fun (i : Fin n) => (L.con (c i)).term)) = realize (Sum.elim v fun (i : Fin n) => ↑(L.con (c i))) s

The value of a term of L with constants substituted for its bound positions, in an expansion of an L-structure, is its value at the values of the constants.