3.8. Algebraic terms

Algebraic drafts

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⊂ (LDD, such that:

Let us denote ∀xOD, ΨD(x) = (σ(x), lx) ∈ LD where σ∈LOD and lxDnσ(x).
Equivalent formulations of well-foundedness are

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

A ground draft is a draft with no variable, i.e. VD=∅. Thus, ΨD: DLD and SubLD = {D}.
Variables in a draft may be reinterpreted as constants: extending ΨD by IdVD : VDV, forms a ground (LV)-draft.

Sub-drafts and terms

Drafts do not have interesting stable subsets (by well-foundedness), but another stability concept: 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 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. A term is a draft co-generated by a single element that is its root. Each x in a draft D defines a term Tx with root x, sub-draft of D co-generated by {x}.
Each draft D is ordered by xyxTy. It is obviously a preorder. Proof of antisymmetry (uniqueness of the root):
xOD, VDA={yD|xTy} which is a sub-draft by transitivity of ≤.
xA ∴ ∃zOD\A, Im lzA.
A∪{z} is a sub-draft, thus TzA∪{z} by definition of Tz.
zOD\AxTzx=z. Thus x is determined by A. ∎
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.

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 concrete category is that of drafts with variables-preserving morphisms, where V is fixed and morphisms f from a draft D are subject to f|VD = IdVD. This is equivalently expressed reinterpreting variables as constants, as the category of ground (LV)-drafts.

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, also expressible as

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

Any interpretation vEV of variables in an algebra E determines an interpretation of any draft D in E. To simplify formulations, restricting v to VD reduces the problem to the case VD=V.

Theorem. For any L-draft D with VD=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).

Uniqueness is deduced from well-foundedness : ∀g,h∈MorL(D,E), g|V = v = h|VV⊂ {xD|g(x) = h(x)} ∈ SubLDg=h.
Let us now prove existence (using conditional operator).
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
hK
(CD*(LC) ∋ x↦ (xC ? h(x) : φE(hLD(x))))) ∈ K
D*(LC) ⊂ C
C=D

Operations defined by terms

Any element t of an L-draft D defines a V-ary operation symbol, interpreted in each L-algebra E by ∀vEV, tE(v) = h(t) for the unique h∈MorL(D,E) such that h|VD = v|VD. This formalizes the operation defined by a term, namely the L-term with root t in D (which can replace D here without modifying the interpretations of t).

This interpreted operation symbol being the structure defined by (IdV,t), is preserved by all L-morphisms, thus can be added to L without changing the category of L-algebras.
Symbols sL come back as the particular cases of the terms they form themselves where Ψ(t) = (s, IdV).
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.
Set theory and foundations of mathematics
1. First foundations of mathematics
2. Set theory (continued)
3. Algebra 1
3.1. Relational systems and concrete categories
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
3.9. Term algebras
3.10. Integers and recursion
3.11. Presburger Arithmetic
4. Model Theory