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

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

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

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

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

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

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

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

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