This section aims to formalize as systems
in a set theoretical framework, the concept of *algebraic term*, particular case of terms
(first intuitively
introduced in 1.5), with a purely algebraic language *L*
(no predicate, logical symbols nor binders) and a set *V* of variable symbols,
still assuming only one type (the generalization to many types is easy).

For convenience we need to 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 Ψ

A subset

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, as from arguments in different sub-algebras the result may escape 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, by re-expressing the term as a formula defining a relation (graph of the operation) using symbols ∃ and ∧, and using the preservation of structures defined by such formulas.

**D**is functional, i.e. Ψ_{D}is injective;*D*has an injective interpretation in some algebra;- For any two distinct elements of
*D*there is an algebra interpreting them differently.

2.⇒3.

3.⇒1. ∀

If *L* only has symbols with arity 0 or 1 then every *L*-term is condensed.

∀(

Then the interpretation of

If *L* has no constant then ∅ is a ground term *L*-algebra.

If *L* only has constants, then ground term *L*-algebras are the
copies of *L*.

From any injective *L*-algebra (*E*,φ_{E}) and
*V* ⊂ *E* \ Im φ_{E} one can form the term algebra
〈*V*〉_{L}. In particular the existence of an injective
algebra implies that of a ground term algebra.

**Proposition.** For any ground term *L*-algebra *K*
and any injective *L*-algebra *M*, the unique
*f*∈Mor_{L}(*K*,*M*) is injective.

Proof 2. Im

This

For any subset *A* of an *L*-algebra *E* and any term algebra
whose set of variables is a copy of *A*, the image of its interpretation
in *E* is 〈*A*〉_{L}.

Conversely if

A **free monoid** on a set *X* (essentially determined by *X*)
is a unary term *X*-algebra seeing *X* as a set of function symbols;
or equivalently, a monoid *M* such that *X* ⊂ *M* and

- 〈
*X*〉_{{e,•}}=*M* - Any function from
*X*to any monoid is extensible as an {*e*,•}-morphism (unique due to the previous condition).

When writing terms with multiple uses of an associative operation symbol, all parenthesis may be removed. For monoids, this removal of parenthesis and also of occurrences of

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 and term algebras

3.9. Integers and recursion

3.10. Arithmetic with addition