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

Введение

Во время обеда к вам подошёл коллега-программист и заявил, что математика программисту и не нужна вовсе. Вчера он взял учебник 7 класса, раздел «доказательство тождеств в натуральных числах». Вспомнил несколько школьных аксиом:

$x \cdot 1 = x$
$x \cdot y = y \cdot x$
$(x \cdot y) \cdot z = x \cdot (y \cdot z)$
$x \cdot (y + z) = x \cdot y + x \cdot z$

И написал программу, которая применяет аксиомы, пока тождество не сойдётся. Для примера, доказательство, что $(x + 1)(x + 1) = x \cdot x + 2x + 1$ :

$(x + 1)(x + 1) = (x + 1) \cdot x + (x + 1) \cdot 1$ (аксиома 6)
$= x \cdot (x + 1) + (x + 1) \cdot 1$ (аксиома 4)
$= x \cdot (x + 1) + (x + 1)$ (аксиома 3)
$= x \cdot x + x \cdot 1 + (x + 1)$ (аксиома 6)
$= x \cdot x + x + (x + 1)$ (аксиома 3)
$= x \cdot x + (x + x) + 1$ (аксиома 2)
$= x \cdot x + x \cdot (1 + 1) + 1$ (аксиома 6)
$= x \cdot x + 2x + 1$

Подобным образом он решил все примеры из учебника.

Задача Тарского

Заметим коллеге, что алгебра с такими аксиомами порождает только многочлены. Поэтому можно построить даже более эффективный алгоритм доказательства:

Выбираем канонический вид многочлена.
С помощью аксиом приводим левый и правый многочлен к каноническому виду.
Сравниваем многочлены.

Поэтому дадим задачу посложнее: учебник 11 класса, с добавлением операции возведения в степень и аксиом для неё:

$x \cdot 1 = x$
$x \cdot y = y \cdot x$
$(x \cdot y) \cdot z = x \cdot (y \cdot z)$
$x \cdot (y + z) = x \cdot y + x \cdot z$
$1^{x} = x$
$x^{1} = x$
$x^{y + z} = x^y \cdot x^z$
$(x \cdot y)^z = x^z \cdot y^z$
$(x^{y})^{z}= x^{y \cdot z}$

Может ли программа по-прежнему доказать любое тождество в натуральных числах, содержащее сложение, умножение и возведение в степень? В подобной постановке эта задача известна как Задача Тарского по школьной алгебре. Кажется, что возведение в степень ничего принципиально не меняет. Однако это не так — существуют тождества, которые из этого набора аксиом не следуют. Впервые это было доказано в 1980 году[1]. Вот пример подобного тождества:

$((1 + x)^{y} + (1 + x + x^{2})^{y})^{x} \cdot ((1 + x^{3})^{x} + (1 + x^{2} + x^{4})^{x})^{y}\\=((1 + x)^{x} + (1 + x + x^{2})^{x})^{y} \cdot ((1 + x^{3})^{y} + (1 + x^{2} + x^{4})^{y})^{x}$

Данное тождество верно, чтобы это доказать, достаточно разделить второй член в обеих частях на $(x^2 - x + 1)^{xy}$ . Но используя заданную систему аксиом, такое доказательство построить нельзя (подвох здесь в вычитании, которое есть в ).

Возникает новый вопрос: насколько много таких тождеств? Что если коллега просто добавит это тождество к аксиомам в свою программу?

В 1990 было показано[2], что нельзя ввести конечный набор аксиом так, чтобы из них выводились все тождества в натуральных числах со сложением, умножением и возведением в степень. Сколько бы аксиом коллега ни добавлял, всегда найдётся такое тождество, которое его программа доказать не сможет.

Ссылки

[1]. A.J. Wilkie, On exponentiation — a solution to Tarski’s high school algebra problem, Connections between model theory and algebraic and analytic geometry, Quad. Mat., 6, Dept. Math., Seconda Univ. Napoli, Caserta, (2000), pp. 107–129.
[2]. R. Gurevič, Equational theory of positive numbers with exponentiation is not finitely axiomatizable, Annals of Pure and Applied Logic, 49:1–30, 1990.

—-

Больше интересного — в Телеграм-канале