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}*=

∃!

∀

⋃

(

- 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 abstractly conceived terms regardless their size) sees them as relations
defined by tuples (Id
_{V},*t*).

**D**is functional, i.e. Ψ_{D}is injective;*D*has an injective interpretation in some algebra;- For any two distinct elements of
*D*there exists an algebra where their interpretations differ.

2.⇒3.

3.⇒1. ∀

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

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

Namely, any

Im

Im

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*; 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 an {*e*,•}-morphism (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