Pull to refresh

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

Reading time2 min
Views5.5K

Введение

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

  1. x + y = y + x

  2. (x + y) + z = x + (y + z)

  3. x \cdot 1 = x

  4. x \cdot y = y \cdot x

  5. (x \cdot y) \cdot z = x \cdot (y \cdot z)

  6. 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

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

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

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

  1. Выбираем канонический вид многочлена.

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

  3. Сравниваем многочлены.

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

  1. x + y = y + x

  2. (x + y) + z = x + (y + z)

  3. x \cdot 1 = x

  4. x \cdot y = y \cdot x

  5. (x \cdot y) \cdot z = x \cdot (y \cdot z)

  6. x \cdot (y + z) = x \cdot y + x \cdot z

  7. 1^{x} = 1

  8. x^{1} = x

  9. x^{y + z} = x^y \cdot x^z

  10. (x \cdot y)^z = x^z \cdot y^z

  11. (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}. Но используя заданную систему аксиом, такое доказательство построить нельзя (подвох здесь в вычитании, которое есть в x^2 - x + 1).

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

В 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.

—-

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

Tags:
Hubs:
Total votes 16: ↑14 and ↓2+18
Comments3

Articles