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

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

ФормулировкаПравить

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

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

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

ИсторияПравить

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

Задача о выводимости всех тождеств была сформулирована Альфредом Тарским. Точная формулировка использует теорию моделей. В 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}}$ 

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