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

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

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

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

1. [math]\displaystyle{ x+y=y+x }[/math]
2. [math]\displaystyle{ (x+y)+z=x+(y+z) }[/math]
3. [math]\displaystyle{ x\cdot1=x }[/math]
4. [math]\displaystyle{ x\cdot y=y\cdot x }[/math]
5. [math]\displaystyle{ (x\cdot y)\cdot z=x\cdot (y\cdot z) }[/math]
6. [math]\displaystyle{ x\cdot(y+z)=x\cdot y+x\cdot z }[/math]
7. [math]\displaystyle{ 1^x=1 }[/math]
8. [math]\displaystyle{ x^1=x }[/math]
9. [math]\displaystyle{ x^{y+z}=x^y\cdot x^z }[/math]
10. [math]\displaystyle{ (x\cdot y)^z=x^z\cdot y^z }[/math]
11. [math]\displaystyle{ (x^y)^z=x^{y\cdot z} }[/math]

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

История

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

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

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

[math]\displaystyle{ \begin{align}&\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{align} }[/math]

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