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

Задача Тарского по школьной алгебре спрашивает, существует ли тождество над целыми положительными числами с использованием сложения, умножения и возведения в степень, которое не следует из набора тождеств, преподаваемых в школе. Решена в 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{array}{cc}& {((1+x{)}^y+(1+x+x^2{)}^y)}^x\cdot {((1+x^3{)}^x+(1+x^2+x^4{)}^x)}^y=\\ =& {((1+x{)}^x+(1+x+x^2{)}^x)}^y\cdot {((1+x^3{)}^y+(1+x^2+x^4{)}^y)}^x\end{array}$

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