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

∀

These categories have coproducts directly given by disjoint union. In the variables-preserving case, these are made of the unions of the

Products in these categories cannot be directly made of the products of underlying sets. The description of products in the variables-preserving case is left as an exercise after reading about condensed drafts (4.2).

∀*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.

An equivalent condition for an algebraic language to be an abstract clone is that there exists a class of interpretations (algebras), such that this language is stable by definitions by terms, while any two symbols keeping the same interpretation throughout this class are confused.

Set theory and foundations of mathematics

1. First foundations of mathematics

2. Set theory (continued)

3. Algebra 1

4.1. **Algebraic terms**

4.2. Term algebras

4.3. Integers and recursion

4.4. Presburger Arithmetic

4.5. Finiteness and countability

4.6. The Completeness Theorem

4.7. Non-standard models of Arithmetic

4.8. Developing theories : definitions

4.9. Constructions

5. Second-order foundations 4.2. Term algebras

4.3. Integers and recursion

4.4. Presburger Arithmetic

4.5. Finiteness and countability

4.6. The Completeness Theorem

4.7. Non-standard models of Arithmetic

4.8. Developing theories : definitions

4.9. Constructions

6. Foundations of Geometry