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 b ∪ D) is injective
(where b :V → D and Gr b ∩ D
= ∅). This injectivity means that
- D is injective ;
- b is injective, allowing for the simplification V ⊂ D
and b = IdV.
- Im b ∩ Im D = ∅, thus Im b = ∁D
Im D by the hypothesis 〈Im b〉L = D.
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 VD ⊂
D 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 = D∩V and b' = IdVD.
Drafts
Finally, let us formalize an L-draft as an injective L-system (D,
tGr ψD) where:
- Dom ψD = Im D = OD = D\V
is the set of occurrences of symbols from L in D
- VD = ∁D OD = D∩V
is the set of used variables (or occurrences of variables) in D
- 〈VD〉L = D
Let us denote ψD = σ ⊓ l, i.e. ∀x∈OD,
ψD(x) = (σ(x), lx)
∈ LD where σ∈LOD and
lx∈Dnσ(x).
Let R = t∐x∈OD Im lx.
The condition 〈VD〉L = D will be called
well-foundedness, as its equivalent expressions include
∀A⊂D, (VD⊂A ∧ D⋆(LA)
⊂A) ⇒ A = D
∀A⊂D, VD⊂A≠D
⇒ ∃x∈OD\A, Im lx⊂A
∀A⊂OD, A≠∅ ⇒ ∃x∈A, A∩ Im lx = ∅
∀A⊂D, A ⊂
R⋆A ⇒ A = ∅
A ground draft is a draft with no variable, i.e. VD = ∅. Thus,
ψD: D → LD and SubLD = {D}.
Variables in a draft may be reinterpreted as constants: extending ψD
by IdVD : VD → V,
forms a ground (L∪V)-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 A⊂D
will be called a sub-draft of D if, denoting OA =
A∩OD and ψA = ψD|OA
we have Im ψA⊂ LA, i.e.
∀x∈OA, Im lx⊂A.
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:
∀x∈OD, VD ⊂
A={y∈D|x∉Ty} which is a sub-draft
by transitivity of ≤.
x∉A ∴ ∃z∈OD\A,
Im lz⊂A.
A∪{z} is a sub-draft, thus Tz⊂A∪{z}
by definition of Tz.
z∈OD\A ∴
x∈Tz ∴ x = z.
Equivalent values of
x for ≤ give the same A, to which the same z fits.
Thus this equivalence is equality. ∎
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 ∧ ψE ⚬
f|OD = Lf⚬ψD)
where the equality condition can be split as
σE⚬f|OD
= σD
∀x∈OD,
lf(x) = f⚬lx.
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 (L∪V)-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
V∐i∈I Di
= (⋃i∈I VDi) ∪
∐i∈I
ODi
with the structure defined like before.
In the binary case this coproduct between drafts D,E
will be written D ⊔V 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
- For any sub-draft F⊂E, f⋆(F) is co-stable.
- If f[VD] ⊂ VE then Im f is co-stable,
and ∀x∈D,
f[Tx] = T f(x).
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=
φE⚬Lf⚬ψD
∀x∈OD, f(x) =
σ(x)E(f⚬lx)
Theorem. For any L-draft D and any L-algebra E,
∀u∈EV,
∃!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) = {f∈ED |
Gr f ∈ SubL(D×E)}.
As MinL(D×E) is surjective and D is a ground draft, we get
{x∈D | ∃!y∈E,
(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|VD〉L,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
∀u∈EV, 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 v∈EV 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
5. Second-order foundations
6. Foundations of Geometry