The concept of term, intuitively
introduced in 1.5, is going to be formalized as mathematical systems in
a set theoretical framework, in the case of only one type (the generalization to many
types is easy). We shall start by those with a purely algebraic language
(without logical symbols), called *algebraic terms*, but for this, let us first introduce
a more general class of systems.

- The transpose
^{t}**D**of**D**is the graph of a function Ψ_{D}:*O*→_{D}*L*⋆*D*, whose domain*O*= Im_{D}**D**⊂*D*is called the set of*occurrences*in*D*, and its complement*V*=_{D}*D*\*O*is called the set of_{D}*variables*of*D*; - 〈
*V*〉_{D}_{L}=*D*(well-foundedness condition).

Equivalent expressions of well-foundedness are

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

∀

∀

∀

A

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 (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).

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

For eachMore properties of this order will be seen for integers 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}*০

∀

But for any element

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

∃!

The uniqueness comes from a previous proposition.

∀

⋃

(

As a particular case of a relation defined by a tuple, here (Id

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

Each element ofThe same for terms whose set of variablesFbijectively defines a term inFas the sub-draft ofFit co-generates, thus where it is the root.

For anyL-termTwith roottand variables ⊂V, the uniquef∈Mor(T,F) such thatf_{|T⋂V}= Id_{T⋂V}represents it inFas the term Imfwith rootf(t).

Then its interpretation in anyL-algebraEextending anyv∈E, is determined by the unique^{V}g∈Mor_{L}(F,E) extendingv, asg০f∈Mor(T,E), with resultg(f(t)).

For any subset

If

Set theory and foundations of mathematics

1. First foundations of mathematics

2. Set theory (continued)

3.1. Morphisms of relational systems and concrete categories4. Model Theory

3.2. Algebras

3.3. Special morphisms

3.4. Monoids

3.5. Actions of monoids

3.6. Categories

3.7.Algebraic terms and term algebras

3.8. Integers and recursion

3.9. Arithmetic with addition