|
|
en.wikipedia.org/wiki/Tarski's_high_school_algebra_problem
在数理逻辑中，Tarski的高中代数问题是Alfred Tarski提出的一个问题。
如下 11 个恒等式称为“高中代数的公理”
\begin{align} &x + y = y + x\\ &(x + y) + z = x + (y + z)\\ &x · 1 = x\\ &x · y = y · x\\ &(x · y) · z = x · (y · z)\\ &x · (y + z) = x · y + x ·z\\ &1^{x} = 1\\ &x^{1} = x\\ &x^{y + z} = x^{y} · x^{z}\\ &(x · y)^{z} = x^{z} · y^{z}\\ &(x^{y})^{z} = x^{y · z}.\\\end{align}Tarski 的问题：是否存在只涉及加法、乘法和取幂的恒等式，对所有正整数都成立，但不能仅用公理 1-11 证明？
这个问题在 1980 年由 Alex Wilkie 解决，他构造了一个无法仅用公理 1-11 证明的恒等式。通过引入对应于将正数映射到正数的多项式的新函数符号，他证明了这一恒等式，并表明这些函数连同上述 11 个公理对于证明这一点是充分且必要的。 这个恒等式是\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*}这个恒等式通常表示为 $W(x, y)$ 并且对于所有正整数 $x$ 和 $y$ 都为真，如通过因式分解 $(1-x+x^2)^{xy}$ 可以看出每边的第二个因式； 然而，使用公理 1-11 无法证明它是正确的。
直观地说，之所以不能证明这个恒等式，是因为不能仅用公理 1-11 讨论多项式$1-x+x^2$。 关于包含负系数的多项式的推理需要“加法逆”或减法的概念，而这些在公理 1-11 中不存在。 Wilkie 的论文结果用更正式的语言表明，公理 1-11 中的“唯一缺陷”是无法操纵包含负系数的多项式。 |
|
