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 of a draft *D* is a sub-draft
of *D*. Moreover, any union of sub-drafts is also a sub-draft (which did not work for
sub-algebras because an operation with arity >1 with arguments in different sub-algebras
may give a result outside their union).

Each draft

For eachMore 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, let_{D}A={y∈O|¬_{D}x≤y} andz∈O\_{D}Asuch that Iml⊂_{z}A. ThusA∪{z} is a sub-draft. Thusx=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}*=

∃!

∀

⋃

(

- A partial proof, namely a schema of one proof for each concretely written term, re-expresses the term defining an operation as a formula defining a relation (its graph), using symbols ∃ and ∧. This repeatedly uses the preservation property for each occurrence of symbol it contains.
- The full proof (for abstract terms regardless their size) sees them as relations
defined by tuples (Id
_{V},*t*).

If *L* does not contain any constant then
∅ is a ground term *L*-algebra.

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

**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. The subalgebra Im

Indeed, any

For any subset *A* of an *L*-algebra *E*, the *L-*subalgebra
〈*A*〉_{L} of *E* is the set of
values of all *L-*terms with variables interpreted in *A*. Indeed it is the image of the interpretation
in *E*, of a term algebra whose set of variables is a copy of *A*.

A **free monoid** on a set *X* is a unary term *X*-algebra
seeing *X* as made 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 a morphism of monoid (unique due to the previous condition).

The image 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