4. Arithmétique et fondements du premier ordre

4.1. Termes algébriques

Introduction

Le concept de terme algébrique, à savoir un terme de langage purement algébrique L avec un ensemble V de symboles de variables (pas de prédicats, de symboles logiques ni de symboles liants), fut d'abord intuitivement introduit en 1.5. Nous allons maintenant le formaliser comme une sorte de systèmes dans un cadre ensembliste. Par commodité, supposons un seul type (la généralisation au cas multi-type est facile), et commençons par une classe plus large de systèmes que nous nommerons L-brouillons.
La formalisation de ce concept a plusieurs variantes possibles.

Suivant une première approche, un L-brouillon est un L-système équationnel (D, b) tel que (Gr bD) est injective (où b: VDD and Gr bD = ∅). Cette injectivité signifie que

L'ensemble D désigne l'ensemble des occurrences de symboles, divisé entre l'ensemble Im b d'occurrences de symboles de variables, et l'ensemble Im D d'occurrences de symboles de L. Mais cette définition des brouillons impliquant que chaque variable apparaisse une seule fois, elle ne pourrait pas inclure directement les termes algébriques, où une variable peut avoir plusieurs occurrences ou aucune, comme cas particuliers. La solution est de d'abord remplacer l'utilisation de b par celle de son inverse b', fonction d'un ensemble d'occurrences VDD vers l'ensemble V des variables disponibles, puis d'en retirer l'exigence de bijectivité.
On peut garder l'exigence d'injectivité sur b', à savoir l'unicité d'occurrence de toute variable, car toute multiplicité d'occurrences d'une variable dans un terme peut être remplacée par l'usage d'une seule occurrence multiplement référencée à l'intérieur du terme (ce remplacement donne un « terme » synonyme conçu abstraitement, ignorant tout souci de notations visibles).
Mais lorsque plusieurs variables sont disponibles (∃≥2: V), on doit autoriser les b' non surjectifs (termes laissant certaines variables disponibles inutilisées), en particulier pour autoriser comme brouillon tout terme fait d'un seul symbole de variable.
D'où la pertinence d'une formalisation où VD = DV et b' = IdVD.

Brouillons

Enfin, définissons un L-brouillon comme un L-système injectif (D, tGr ψD) où: Notons ψD = σ ⊓ l, i.e. ∀xOD, ψD(x) = (σ(x), lx) ∈ LD où σ∈LOD et lxDnσ(x).
Le bon fondement a pour formules équivalentes

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

Un brouillon clos est un brouillon sans variable : VD = ∅. Donc, ψD: DLD et SubLD = {D}.
Les variables d'un brouillon peuvent se réinterpréter comme constantes: étendre ψD par IdVD : VDV, forme un (LV)-brouillon clos.

Sous-brouillon et termes

Le bon-fondement rendant inintéressantes les parties stables des brouillons, au profit d'un autre concept de stabilité: une partie AD sera appelée un sous-brouillon de D (ou une partie co-stable de D) si, notant OA = AOD et ψA = ψD|OA, on a (Im ψALA), i.e. ∀xOA, Im lxA.
Tout sous-brouillon A d'un brouillon D est un brouillon, i.e. satisfait les axiomes ci-dessus avec V fixe, où le bon-fondement de A est évidemment déduit de celui de D par sa dernière formulation.

Comme avec les parties stables, toute intersection de sous-brouillons est un sous-brouillon. De plus, toute union de sous-brouillons est aussi un sous-brouillon (contrairement aux sous-algèbres avec une opération d'arité >1, qui avec des arguments dans différentes sous-algèbres peut donner un résultat échappant à leur union).

Le sous-brouillon co-engendré par une partie d'un brouillon, est l'intersection de toutes les sous-brouillons qui l'incluent. Un terme est un brouillon co-engendré par un unique élément qui est sa racine. Tout élément x d'un brouillon D définit un terme Tx de racine x, sous-brouillon de D co-engendré par {x}.
Chaque brouillon D est ordonnée par xyxTy. C'est évidemment un préordre. Son antisymétrie, à savoir l'unicité de la racine de tout terme, peut être prouvée comme suit (une preuve plus élégante à partir de concepts plus généraux est donnée dans l'étude des correspondances de Galois) :

Catégories de brouillons

Comme systèmes relationnels particuliers, les classes de L-brouillons forment des catégories concrètes. Entre deux L-brouillons D,E,

f ∈ MorL(D,E) ⇔ (f[OD]⊂OE ∧ ψEf|OD = Lf⚬ψD)

où la condition d'égalité se divise en

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

Les coproduits y sont donnés par l'union disjointe, comme avec les systèmes relationnels.

Une autre catégorie concrète est celle des brouillons avec morphismes préservant les variables, où V est fixe, et

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

C'est en gros la catégorie des (LV)-brouillons clos (réinterprétant les variables comme des constantes, sauf qu'une variable peut y avoir plusieurs occurrences dans ces derniers, tandis qu'elle ne pouvait en avoir qu'une éventuellement référencée plusieurs fois dans les premiers). La définition des coproduits y est modifiée en

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

avec la structure définie comme avant. Dans le cas binaire ce coproduit entre les brouillons D,E s'écrira DV E.
Les produits dans ces catégories ne peuvent pas être directement constitués des produits des ensembles sous-jacents. La description des produits dans le cas préservant les variables est laissée en exercice une fois compris la condensation des brouillons (4.3).

Images de brouillons

Si D,E sont des L-brouillons et f ∈ MorL(D,E) alors

Inteprétations des brouillons dans les algèbres

Une interprétation d'un L-brouillon D dans une L-algèbre E, est un morphisme f∈MorL(D,E), autrement dit

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

Toute interprétation vEV de variables dans une algèbre E détermine une interprétation de tout brouillon D dans E. Pour simplifier les formulations, restreindre v à VD réduit le problème au cas VD=V.

Théorème. Pour tout L-brouillon D et toute L-algebre E,

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

Preuve. Pour simplifier, soit V = VD par restriction de u.
L'unicité a été vue avec les systèmes équationnels, et servira pour prouver l'existence :Autrement dit, toute L-algèbre E est un module pour tout L-brouillon.

Ceci justifie formellement le concept de symbole d'opération défini par un terme et interprété comme operation dans chaque L-algèbre, par les concepts expliqués en 3.11 : le role de symbole d'opération V-aire joué par tout élément s d'un L-brouillon D (interprété dans chaque L-algèbre E par ∀uEV, sE(u) = h(s) pour l'unique h∈MorL(D,E) tel que h|VD = u|VD), préservée par tous les L-morphismes, est celui du symbole d'opération défini par le L-terme de racine s co-engendré par s dans D.


Théorie des ensembles et fondements des mathématiques
1. Premiers fondements des mathématiques
2. Théorie des ensembles
3. Algèbre
4. Arithmétique et fondements du premier ordre
4.1. Termes algébriques
4.2. Systèmes quotient
4.3. Term algebras
4.4. Integers and recursion
4.5. Presburger Arithmetic
4.6. Finiteness and countability (draft)
4.7. The Completeness Theorem
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

Other languages:
EN : 4.1. Algebraic terms