Function symbols occurring in a term

Term.functionsIn records function symbols together with their arities. The set is finite, unchanged by relabelling variables, bounded under substitution by the symbols of the substituted terms, mapped to its image under a language homomorphism (with LHom.exists_eq_onTerm_of_functionsIn_subset pulling back terms whose occurring symbols lie in the image of a given set), and determines which interpretations a term can observe. These facts supply the term cases of symbol locality for infinitary formulas.

def FirstOrder.Language.Term.functionsIn {L : Language} {α : Type uα} : L.Term α → Set ((n : ℕ) × L.Functions n)

The function symbols occurring in a term, tagged by arity.

@[simp]

theorem FirstOrder.Language.Term.functionsIn_var {L : Language} {α : Type uα} (a : α) : (var a).functionsIn = ∅

@[simp]

theorem FirstOrder.Language.Term.functionsIn_func {L : Language} {α : Type uα} {n : ℕ} (f : L.Functions n) (ts : Fin n → L.Term α) : (func f ts).functionsIn = {⟨n, f⟩} ∪ ⋃ (i : Fin n), (ts i).functionsIn

theorem FirstOrder.Language.Term.functionsIn_finite {L : Language} {α : Type uα} (t : L.Term α) : t.functionsIn.Finite

Every term mentions only finitely many function symbols, even over an arbitrary language.

@[simp]

theorem FirstOrder.Language.Term.functionsIn_relabel {L : Language} {α : Type uα} {β : Type uβ} (t : L.Term α) (g : α → β) : (relabel g t).functionsIn = t.functionsIn

Relabelling variables does not change the function symbols of a term.

theorem FirstOrder.Language.Term.functionsIn_subset_functionsIn_subst {L : Language} {α : Type uα} {β : Type uβ} (t : L.Term α) (f : α → L.Term β) : t.functionsIn ⊆ (t.subst f).functionsIn

Substitution keeps every function symbol of the original term.

theorem FirstOrder.Language.Term.functionsIn_subst_subset {L : Language} {α : Type uα} {β : Type uβ} (t : L.Term α) (f : α → L.Term β) : (t.subst f).functionsIn ⊆ t.functionsIn ∪ ⋃ (a : α), (f a).functionsIn

Substitution adds at most the function symbols of the substituted terms.

theorem FirstOrder.Language.Term.subst_eq_or_exists_functionsIn_subset {L : Language} {α : Type uα} {β : Type uβ} (t : L.Term α) (f g : α → L.Term β) : t.subst f = t.subst g ∨ ∃ (a : α), f a ≠ g a ∧ (f a).functionsIn ⊆ (t.subst f).functionsIn

Two substitutions either give a term the same image, or they differ at a variable whose substituted term has all its function symbols in the image of the term.

@[simp]

theorem FirstOrder.Language.Term.functionsIn_onTerm {L : Language} {α : Type uα} (t : L.Term α) {L' : Language} (g : L →ᴸ L') : (g.onTerm t).functionsIn = (fun (f : (n : ℕ) × L.Functions n) => ⟨f.fst, g.onFunction f.snd⟩) '' t.functionsIn

A language map sends the occurring function symbols to their images.

theorem FirstOrder.Language.Term.realize_congr_of_agreeOn {L : Language} {α : Type uα} {M : Type w} (t : L.Term α) (S S' : L.Structure M) (h : ∀ {n : ℕ} (f : L.Functions n), ⟨n, f⟩ ∈ t.functionsIn → ∀ (xs : Fin n → M), Structure.funMap f xs = Structure.funMap f xs) (v : α → M) : realize v t = realize v t

Interpretations agreeing on the occurring symbols give the same value to a term.

theorem FirstOrder.Language.LHom.exists_eq_onTerm_of_functionsIn_subset {L : Language} {L' : Language} {α : Type uα} (g : L →ᴸ L') {F : Set ((k : ℕ) × L.Functions k)} (t : L'.Term α) (hF : t.functionsIn ⊆ (fun (f : (k : ℕ) × L.Functions k) => ⟨f.fst, g.onFunction f.snd⟩) '' F) : ∃ (t₀ : L.Term α), g.onTerm t₀ = t ∧ t₀.functionsIn ⊆ F

A term of L' whose occurring function symbols lie in the image of a set F under a language homomorphism g : L →ᴸ L' is the image under g of a term of L whose occurring function symbols lie in F. No injectivity of g is needed.