3.7. Algebraic terms and term algebras

Algebraic drafts

As the concept of term was only intuitively introduced in 1.5, let us now formalize the case of terms using a purely algebraic language (without logical symbols), called algebraic terms, as mathematical systems in a set theoretical framework.
For convenience, let us work with only one type (the generalization to many types is easy) and introduce a class of systems more general than terms, that we shall call drafts. Variables will have a special treatment, without adding them as constants in the language.

Given an algebraic language L, an L-draft will be an L'-system (D,D) where D⊂ (LDD, such that:

Let us denote ∀xOD, ΨD(x)=(σ(x), lx) ∈ LD where s(x)∈L and lxDnσ(x). We can also denote σD(x)=σ(x) to let σD be a function with domain OD.
Well-foundedness can be equivalently written in any of these forms

AOD, (∀xOD, Im lxAVDxA) ⇒ A=OD
AD, (VDAD*(LA) ⊂A) ⇒ A = D
AD, VDAD ⇒∃xOD\A, Im lxA
AOD, A≠∅ ⇒ ∃xA, A⋂ Im lx = ∅

The set of used variables of (D,D), those which effectively occur, is VD⋂⋃xOD Im lx. Unused variables can be added or removed in D while keeping D fixed (by changing DOD∪(⋃xOD Im lx)), so that their presence may be irrelevant.
A ground draft is a draft with no variable, i.e. VD=∅. Thus, ΨD: DLD and SubLD = {D}.
More generally a draft is ground-like if it has no used variable (Dom DLOD).

Sub-drafts and terms

Drafts do not have interesting stable subsets (by well-foundedness), but let us introduce another stability concept for them.
A subset AD is a sub-draft of D (or a co-stable subset of D) if, denoting OA = AOD and ΨA= ΨD|OA, we have (Im ΨALA), i.e. ∀xOA, Im lxA.
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 also a sub-draft; the sub-draft co-generated by a subset is the intersection of all sub-drafts that include it.
A term is a draft co-generated by a single element which is its root.
Moreover, any union of sub-drafts is also a sub-draft (which was not the case for sub-algebras because an operation with arity >1 whose arguments take values in different sub-algebras may give a result outside their union).

There is a natural order relation on each draft D defined by xy ⇔ x∈ (the term with root y). It is obviously a preorder. Its antisymmetry is less obvious; a proof for integers will be given in 3.6, while the general case will come from properties of well-founded relations in the study of Galois connections.

Categories of drafts

As particular relational systems, classes of L-drafts form concrete categories. Between two L-drafts D,E,

f ∈MorL(D,E) ⇔ (f[OD]⊂OE ∧ ΨEf|OD= fL০ΨD)

where the equality condition can be split as

σEf|OD = σD
xOD, lf(x)=flx

Another kind of category of drafts can be considered, with objects also L-drafts but with a common set of variables (VD=VE=V) and taking smaller sets of morphisms: the variables-preserving morphisms, i.e. moreover satisfying f|V = IdV.
But for any element t in any draft, the term T co-generated by {t} has as set of variables TV (which is the set of used variables of T unless T={t}⊂V) generally smaller than V, so the admission of terms defined as subsets co-generated by singletons in such a category requires this loosening of the condition. This naturally simplifies when reformulating such categories as those of ground (LV)-drafts: in each draft, variable symbols are replaced (reinterpreted) by constant symbols added to the language, so ΨE is extended by IdV, to form a ground (LV)-draft.

Intepretations of drafts in algebras

For any L-draft D and any L-algebra E, an interpretation of D in E is a morphism f∈MorL(D,E), i.e. f|OD= φEfL০ΨD, which can also be written

xOD, f(x) = σ(x)E(flx)

Theorem. For any L-draft D with set of variables V and any L-algebra E, any vEV is uniquely extensible to an interpretation of D:
∃!h∈MorL(D,E), h|V = v, equivalently ∃!hEOD, vh ∈MorL(D,E).

The uniqueness comes from a previous proposition.

Proof of existence.
S = {AD | VA∧ Im ΨALA}
vK = ⋃AS {f∈MorL(A,E) | f|V =v}
f,gK, B = Dom f ⋂ Dom g ⇒ (f|BKg|BK) ⇒ f|B=g|B
fK Gr f = Gr h
C= Dom h = ⋃fK Dom fS
(CD*(LC) ∋ x↦ (xC ? h(x) : φE(hLD(x))))) ∈ K (see conditional operator)
D*(LC) ⊂ C

Operations defined by terms

A new operation symbol can be defined by any element t of an L-draft D : it is the V-ary operation defined by the L-term with root t, that is co-generated by t in D. Its interpretation in each E is defined by ∀vEV, tE(v) = h(t) for the unique h∈MorL(T,E) such that h|TV=v.

As a particular case of a relation defined by a tuple, here (IdV,t), these operations are preserved by all morphisms between L-algebras, and can thus be added to L without changing the sets of morphisms.

Another way to see it is as a particular case of conservation of relations defined by formulas in categories of relational systems, since any term defining an operation can be re-expressed as a formula defining the graph of this operation, using logical symbols ∃ and ∧. The advantage now that it is established for the general case of abstractly conceived terms no matter their size, instead of concretely written terms on which the conservation property must be repeatedly used for each occurrence of symbol it contains.

Term algebras

An L-algebra (EE) is called a term algebra if it is injective and 〈E\Im φEL = E. Thus it is also an L-draft with ΨE = φE-1. As such, it is ground if moreover E=Im φE. So, a ground term algebra is an algebra both minimal and injective, and thus also bijective.

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.
The existence of term algebras in other cases will be discussed in the next section; let us admit it for now.

Whenever present as object, any ground term L-algebra is a final object in any category of ground L-drafts, and an initial object in any category of L-algebras. In any variables-preserving category of L-drafts with a fixed set V of variables (category of ground (LV)-drafts), any term L-algebra F, when present, is a final object.

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

Proof 1. By a previous result, {xK | ∀yK, f(x) = f(y) ⇒ x=y} ∈ SubLK, thus = K.

Proof 2. The subalgebra Im f of M is both injective and minimal, thus a ground term L-algebra, so the morphism f between initial L-algebras K and Im f is an isomorphism.

Role of term algebras as sets of all terms

Any term algebra F plays the role of the "set of all terms" with its list V of variable symbols, for the following reason:
Each element of F bijectively defines a term in F as the sub-draft of F it co-generates, thus where it is the root.
For any L-term T with root t and variables ⊂V, the unique f∈Mor(T,F) such that f|TV = IdTV represents it in F as the term Imf with root f(t).
Then its interpretation in any L-algebra E extending any vEV, is determined by the unique g∈MorL(F,E) extending v, as gf∈Mor(T,E), with result g(f(t)).
The same for terms whose set of variables V' is interpreted in E by the composite of a function from V' to V, with one from V to E (instead of having V'V).
For any subset A of an L-algebra E, any term algebra FA whose set of variables is a copy of A, represents the set of all L-terms with variables interpreted in A. Then, the L-subalgebra 〈AL of E is the image of the interpretation of FA in E, i.e. the set of all values of these terms.

The monoid of unary terms

Let M be a unary term L-algebra (unary = with one variable; this algebra is essentially unique for each L). Then its elements play the roles of the function symbols defined by all possible unary L-terms, and preserved by morphisms across all L-algebras, including M itself. Therefore, thanks to a previous remark, M is natually a monoid acting on all L-algebras.
If L is only made of function symbols then for any L-algebra E, the image of M in EE is the transformation monoid generated by the image of L.

Interpretation of first-order formulas

Trying to extend these formal definitions of terms interpreted in algebras, to formalize the general concept of formula interpreted in systems, the difficulty is to cope with the interpretation of quantifiers (or generally binders, if we wish to still generalize). A possible solution, is to treat all variables as bound throughout the formula.
Binding all variables modifies the view on the above concept of interpretation of a term T with set of variables V in an algebra E by re-currying the family (hv) of functions from T to E where v runs over EV, into a function from T to EEV. So, a first-order formula interpreted in a system E can be understood as a term interpreted in an algebra whose base set is the set OpE ∪ RelE of all operations and all relations in E where OpE = ⋃n∈ℕ OpE(n) and RelE = ⋃n∈ℕ ℘(En).
We might not need the full sets of these, but at least, an algebra of these (a subset stable by all needed logical operations).
We took ℕ for the case we would need to see "all possible formulas" as terms interpreted in one same algebra. By the way, what is ℕ ? This is the object of the next section.
Set theory and foundations of mathematics
1. First foundations of mathematics
2. Set theory (continued)
3. Algebra 1
3.1. Morphisms of relational systems and concrete categories
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
4. Model Theory