Problème d'algèbre de lycée de Tarski

Tarski considère les 11 axiomes suivants sur l'addition ('+'), la multiplication ('·') et l'exponentiation comme des axiomes standards connus au lycée :

1. x + y = y + x
2. (x + y) + z = x + (y + z)
3. x · 1 = x
4. x · y = y · x
5. (x · y) · z = x · (y · z)
6. x · (y + z) = x · y + x ·z
7. 1^x = 1
8. x¹ = x
9. x^y + z = x^y · x^z
10. (x · y)^z = x^z · y^z
11. (x^y)^z = x^y · z.

Ces 11 axiomes, parfois appelées les « identités lycéennes »^[1] sont liés aux axiomes des anneaux exponentiels^[2]. Le problème de Tarski devient alors : existe-t-il des identités n'impliquant que l'addition, la multiplication et l'exponentiation, qui sont vraies pour tout entier positif, mais ne pouvant être démontrées en utilisant uniquement les 11 axiomes ?

Comme les axiomes semblent montrer toutes les propriétés usuelles des opérations algébriques, il n'est pas évident de voir qu'un énoncé utilisant les trois opérations ne puisse pas être démontré. Toutefois, démontrer certaines propriétés simples peuvent parfois nécessiter de longs calculs si on ne doit utiliser que les 11 axiomes. Considérons la démonstration de (x + 1)² = x² + 2 · x + 1 :

(x + 1)²

= (x + 1)^1 + 1

= (x + 1)¹ · (x + 1)¹  par 9.

= (x + 1) · (x + 1)  par 8.

= (x + 1) · x + (x + 1) · 1  par 6.

= x · (x + 1) + x + 1  par 4. et 3.

= x · x + x · 1 + x · 1 + 1  par 6. et 3.

= x¹ · x¹ + x · (1 + 1) + 1  par 8. et 6.

= x^1 + 1 + x · 2 + 1  par 9.

= x² + 2 · x + 1  par 4.

Les parenthèses ne sont pas nécessaires par l'axiome 2. qui donne l'associativité de l'addition.

La longueur des preuves n'est pas un problème ; les calculs montrant des égalités comme le développement de (x + y)¹⁰⁰ seraient longs mais l'idée directrice des calculs resterait la même que pour la preuve donnée en exemple.

La liste des onze axiomes peut être trouvée explicitement dans les travaux de Richard Dedekind^[3], bien qu'ils fussent clairement connus et utilisés par de nombreux mathématiciens l'ayant précédé. Dedekind fut le premier toutefois à se demander si ces axiomes étaient en un sens suffisants pour donner tout ce qu'on pourrait chercher à savoir sur les entiers. La question est devenue, grâce à Alfred Tarski, un problème sérieux de logique et de théorie des modèles au cours des années 1960^[1],[4], et a pris son nom actuel de « Problème d'algèbre de lycée de Tarski » dans les années 1980.

En 1980, Alex Wilkie a démontré que toutes les identités usuelles ne pouvaient être dérivées à partir des 11 axiomes seuls^[5], en donnant explicitement une telle identité. En introduisant de nouveaux symboles fonctionnels correspondant aux polynômes qui envoient les nombres positifs vers des nombres positifs, il montra la validité de cette identité, puis qu'il était nécessaire et suffisant d'avoir ces fonctions associés aux 11 axiomes pour la démontrer. L'égalité en question est : ${\displaystyle {\begin{aligned}&\left((1+x)^{y}+(1+x+x^{2})^{y}\right)^{x}\cdot \left((1+x^{3})^{x}+(1+x^{2}+x^{4})^{x}\right)^{y}\\={}&\left((1+x)^{x}+(1+x+x^{2})^{x}\right)^{y}\cdot \left((1+x^{3})^{y}+(1+x^{2}+x^{4})^{y}\right)^{x}.\end{aligned}}}$

Cette fonctionnelle est souvent notée W(x,y) et est satisfaite pour tous les entiers positifs x et y, ce qu'on peut voir en factorisant (1-x+x²)^xy après simplification ; cependant, les 11 axiomes seuls ne permettent pas de la démontrer.

Intuitivement, on peut voir que l'identité ne peut être démontrée car les axiomes sont insuffisants pour traiter le cas du polynôme 1-x+x². L'étude de ce polynôme et du terme -x requiert la définition de la négativité ou de la soustraction, absentes des axiomes. Cette lacune rend impossible la manipulation de ce polynôme par les axiomes et les calculs complets à partir de celui-ci. Les résultats de Wilkie montrent, dans un langage plus formel, que le « seul handicap » des axiomes « lycéens » est l'impossibilité de manipuler des polynômes à coefficients négatifs.