4. Arithmetic and first-order foundations

4.1. Algebraic terms

Introduction

The concept of algebraic term, namely a term with a purely algebraic language L and a set V of variable symbols (no predicate, logical symbols nor binders), was first intuitively introduced in 1.5. We shall now formalize it as a kind of systems in a set theoretical framework. For convenience let us work with only one type (the generalization to many types is easy), and start with a wider class of systems we shall call L-drafts.
The formalization of this concept has a few possible variants.

In a first approach, an L-draft is an L-equational system (V, D, b) such that (Gr bD) is injective (where b :VD and Gr bD = ∅). This injectivity means that

The set D means the set of occurrences of symbols, split between the set Im b of occurrences of variable symbols, and the set Im D of occurrences of algebraic symbols (those from L). But this definition for drafts would make each variable occur exactly once, thus cannot directly include algebraic terms, where a variable may have multiple occurrences or none, as particular cases. The solution is to first replace the use of b by that of its inverse b', function from a set VDD of the "occurrences of variables" to the set V of available variables, then remove from it the bijectivity requirement.
The injectivity of b' may be formally kept without restricting the generality of intended terms: any intended multiplicity of occurrences of a variable in a term, can be formalized by letting a single occurrence of it be multiply referenced by occurrences of algebraic symbols in the term (such drafts, with multiple references to a single occurrence, are abstractly conceived ignoring any care for visible notations).
But the use of non-surjective b' is still needed to distinguish which available variables are used, especially to formalize terms made of a single variable when multiple variables are available.
Hence the relevance of a formalization where VD = DV and b' = IdVD.

Drafts

Finally, let us formalize an L-draft as an injective L-system (D, tGr ψD) where: Let us denote ψD = σ ⊓ l, i.e. ∀xOD, ψD(x) = (σ(x), lx) ∈ LD where σ∈LOD and lxDnσ(x).
Let R = txOD Im lx.
The condition 〈VDL = D will be called well-foundedness, as its equivalent expressions include

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

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

Among subsets of drafts, the concept of stability is made worthless by well-foundedness. A worthy similar but other concept is co-stability, defined as stability by tR : a subset AD will be called a sub-draft of D if, denoting OA = AOD and ψA = ψD|OA we have Im ψALA, i.e. ∀xOA, Im lxA.
It is then also a draft, with the same V.
The surjective subsystems of drafts are the ground sub-drafts; generally, any surjective subsystem of an injective system is co-stable.
Any union or intersection of sub-drafts is also a sub-draft.

Each draft D has a natural order ⌈R⌉ we shall denote ≤.
For each element x of a draft D, the sub-term of D with root x is the sub-draft Tx = ≤(x) of D co-generated by {x} (intersection of all sub-drafts that contain x). A term is a draft co-generated by a single element that is its root.

The following proof of antisymmetry of ≤ (the uniqueness of the root of any term), was written here before section 3.12 was added with its more elegant proof:

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 = Lf⚬ψD)

where the equality condition can be split as

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

There, coproducts are given by disjoint union, like with relational systems.

Another concrete category is that of drafts with variables-preserving morphisms, where V is fixed, and

MorL,V(D,E) = {f ∈ MorL(D,E) | f|VD = IdVD}.

This is roughly the category of ground (LV)-drafts (reinterpreting variables as constants, except that a multiply used variable may be figured in the latter as multiple elements, but only as a multiply referenced single element in the former).
The definition of coproducts is modified there as

ViI Di = (⋃iI VDi) ∪ ∐iI ODi

with the structure defined like before. In the binary case this coproduct between drafts D,E will be written DV E.
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 once understood draft condensation (4.3).

Images of drafts

If D,E are L-drafts and f ∈ MorL(D,E) then

Intepretations of drafts in algebras

An interpretation of an L-draft D in an L-algebra E, is a morphism f∈MorL(D,E). Equivalently,

f|OD= φELf⚬ψD
xOD, f(x) = σ(x)E(flx)

Theorem. For any L-draft D and any L-algebra E,

uEV, ∃!h∈MorL(D,E), h|VD = u|VD.

Proof. For simplicity, let us eliminate variables (V = ∅) by reinterpreting them as constants. So we need to prove that MorL(D,E) is a singleton.
As said in 3.10, MorL(D,E) = {fED | Gr f ∈ SubL(D×E)}.
As MinL(D×E) is surjective and D is a ground draft, we get

{xD | ∃!yE, (x,y)∈MinL(D×E)} ∈ SubLD = {D}

We conclude that MinL(D×E) is the graph of the unique L-morphism from D to E. ∎
Generally, the graph of the unique h∈MorL(D,E) such that h|VD = u|VD is 〈Gr u|VDL,D×E.

In other words, every L-algebra E is a module for every L-draft.

This formally justifies the concept of operation symbol defined by a term and interpreted as an operation in every L-algebra, by the concepts explained in 3.11 : the role of V-ary operation symbol played by any element s of an L-draft D (interpreted in each L-algebra E by ∀uEV, sE(u) = h(s) for the unique h∈MorL(D,E) such that h|VD = u|VD), preserved by all L-morphisms, is that of the operation symbol defined by the sub-term of D with root s.

Interpretation of first-order formulas

Trying to extend this definition of the interpretation of terms in algebras, to the case of formulas interpreted in systems, the difficulty is to cope with the interpretation of quantifiers (or generally binders, for syntax systems like that of set theory).
In set theory with powerset, this more general case can be reduced to our previous (algebraic) case, by switching to a view over all variables as bound throughout the formula. For example, the family of interpretations hv∈ Mor(T,E) of a term T in an algebra E for every interpretation vEV of its set V of variables, is re-curried into an interpretation of T in the product algebra EEV, while binders are interpreted by functions between different types of operations or relations. So, a first-order formula interpreted in a system E can be understood as a term interpreted in the algebra with types made of both sequences OpE and RelE of structures of all arities. Or, a sub-algebra of it, including arities as large as the number of variables needed in a given context.

Set theory and foundations of mathematics
1. First foundations of mathematics
2. Set theory
3. Algebra 1
4. Arithmetic and first-order foundations
4.1. Algebraic terms
4.2. Quotient systems
4.3. Term algebras
4.4. Integers and recursion
4.5. Presburger Arithmetic
4.6. Finiteness
4.7. Countability and Completeness
4.8. More recursion tools
4.9. Non-standard models of Arithmetic
4.10. Developing theories : definitions
4.11. Constructions
4.A. The Berry paradox
5. Second-order foundations
6. Foundations of Geometry