Tarski's High School Identities (Q5286078)

The question of whether or not the identities (1)--(11): \[ \begin{alignedat}{2} (1)\quad x &+ y=y+ x &\qquad (6) &\quad x\cdot(y+ z)= (x\cdot y)+ (x\cdot z)\\ (2)\quad x &+ (y+ z)= (x+ y)+ z &\qquad (7) &\quad 1^ x= 1\\ (3)\quad x &\cdot 1= x &\qquad (8) &\quad x^ 1= x\\ (4)\quad x &\cdot y= y\cdot x &\qquad (9) &\quad x^{y+z}= x^ y\cdot x^ z\\ (5)\quad x &\cdot(y\cdot z)= (x\cdot y)\cdot z &\qquad (10) &\quad (x\cdot y)^ z= x^ z\cdot y^ z\end{alignedat} \] \[ (11)\quad(x^ y)^ z= x^{y\cdot z} \] provide a basis for all the identities of \({\mathbf N}=(N,+,\cdot,\uparrow,1)\), where \(N\) is the set of positive integers, and \(+\), \(\cdot\), \(\uparrow\) are the familiar operations of addition, multiplication and exponentiation, is called Tarski's High School Problem. The negative solution of this problem was given in 1980 by Wilkie. He showed that some identity \(W(x,y)\) holds in \({\mathbf N}\) and gave a syntactic proof that \(W(x,y)\) cannot be derived from (1)--(11). In this paper the authors give a model (a Gurevic-algebra) of (1)--(11) with 15 elements that does not satisfy Wilkie's identity \(W(x,y)\). At present this is the smallest such model which is known.