Задача Тарского по школьной алгебре

Задача Тарского по школьной алгебре спрашивает, существует ли тождество над целыми положительными числами с использованием сложения, умножения и возведения в степень, которое не следует из набора тождеств, преподаваемых в школе. Решена в 1980 году Алексом Вилки, нашедшем пример тождества, которое не выводится из школьных аксиом.

Формулировка

Верно ли, что из следующих одиннадцати аксиом, которые мы будем называть школьными аксиомами:

1. $x+y=y+x$
2. $(x+y)+z=x+(y+z)$
3. $x\cdot 1=x$
4. $x\cdot y=y\cdot x$
5. $(x\cdot y)\cdot z=x\cdot (y\cdot z)$
6. $x\cdot (y+z)=x\cdot y+x\cdot z$
7. $1^{x}=1$
8. $x^{1}=x$
9. $x^{y+z}=x^{y}\cdot x^{z}$
10. $(x\cdot y)^{z}=x^{z}\cdot y^{z}$
11. $(x^{y})^{z}=x^{y\cdot z}$

следует любое тождество над целыми положительными числами с использованием сложения, умножения и возведения в степень?

История

Этот список из одиннадцати аксиом был выписан Рихардом Дедекиндом, хотя все эти тождества были известны задолго до этого.

Задача о выводимости всех тождеств была сформулирована Альфредом Тарским в 1960-х. Точная формулировка использует теорию моделей. В 1980-х она стала известна как задача Тарского по школьной алгебре.

В 1980 году Алекс Вилки доказал, что тождество

${\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}}$

не выводится из набора школьных аксиом.