The concept of *algebraic term* with a purely algebraic language *L*
and a set *V* of variable symbols (no predicate, logical symbols nor
binders), which was first intuitively introduced in
1.5), is going to be formalized as systems
in a set theoretical framework. For convenience let us work with one type
(the generalization to many types is easy), and start with a wider class of
systems.

Let us call *L*-*draft*
any *L'*-system
(*D*,**D**) where **D**⊂ (*L*⋆*D*)×*D*, such that:

- The transpose
^{t}**D**of**D**is the graph of a function Ψ_{D}:*O*→_{D}*L*⋆*D*, with domain*O*= Im_{D}**D**=*D*\*V*called the set of*occurrences*in*D*(which differs from our first intuitive notion of occurrences), and its complement*V*=_{D}*D*∩*V*is the set of*used variables*of*D*; - 〈
*V*〉_{D}_{L}=*D*(well-foundedness condition).

Equivalent formulations of well-foundedness are

∀*A*⊂*O _{D}*, (∀

∀

∀

∀

Variables in a draft may be reinterpreted as constants: extending Ψ

Indeed, it remains well-founded, as can be seen on the last formulation of well-foundedness.

Like with stable subsets, any intersection of sub-drafts is a sub-draft. Moreover, any union of sub-drafts is also a sub-draft (unlike for sub-algebras with an operation with arity >1, which from arguments in different sub-algebras may give a result escaping their union).

The sub-draft co-generated by a subset of a draft, is the intersection of all sub-drafts that include it. AEach draft

∀More properties of this order will be seen for natural numbers in 3.6, and in the general case with well-founded relations in the study of Galois connections.x∈O,_{D}V⊂_{D}A={y∈D|x∉T} which is a sub-draft by transitivity of ≤._{y}

x∉A∴ ∃z∈O\_{D}A, Iml⊂_{z}A.

A∪{z} is a sub-draft, thusT⊂_{z}A∪{z} by definition ofT._{z}z∈O\_{D}A∴x∈T∴_{z}x=z. Thusxis determined byA. ∎

*f* ∈Mor_{L}(*D*,*E*) ⇔
(*f*[*O _{D}*]⊂

σ* _{E}*০

∀

∀*x*∈*O _{D}*,

**Theorem.** For any *L*-draft *D* with *V _{D}*=

∃!

Let us now prove existence (using conditional operator).

∀

⋃

(

Symbols

For the case of "small" (concretely written) terms, this preservation also has a schema of one proof for each term: re-expressing the term as a formula defining a relation (graph of the operation) using symbols ∃ and ∧, we can use the preservation of structures defined by such formulas.

Set theory and foundations of mathematics

1. First foundations of mathematics

2. Set theory (continued)

3.1. Relational systems and concrete categories4. Model Theory

3.2. Algebras

3.3. Special morphisms

3.4. Monoids

3.5. Actions of monoids

3.6. Invertibility and groups

3.7. Categories

3.8.Algebraic terms

3.9. Term algebras

3.10. Integers and recursion

3.11. Presburger Arithmetic