Введение
Во время обеда к вам подошёл коллега-программист и заявил, что математика программисту и не нужна вовсе. Вчера он взял учебник 7 класса, раздел «доказательство тождеств в натуральных числах». Вспомнил несколько школьных аксиом:
И написал программу, которая применяет аксиомы, пока тождество не сойдётся. Для примера, доказательство, что :
(аксиома 6)
(аксиома 4)
(аксиома 3)
(аксиома 6)
(аксиома 3)
(аксиома 2)
(аксиома 6)
Подобным образом он решил все примеры из учебника.
Задача Тарского
Заметим коллеге, что алгебра с такими аксиомами порождает только многочлены. Поэтому можно построить даже более эффективный алгоритм доказательства:
Выбираем канонический вид многочлена.
С помощью аксиом приводим левый и правый многочлен к каноническому виду.
Сравниваем многочлены.
Поэтому дадим задачу посложнее: учебник 11 класса, с добавлением операции возведения в степень и аксиом для неё:
Может ли программа по-прежнему доказать любое тождество в натуральных числах, содержащее сложение, умножение и возведение в степень? В подобной постановке эта задача известна как Задача Тарского по школьной алгебре. Кажется, что возведение в степень ничего принципиально не меняет. Однако это не так — существуют тождества, которые из этого набора аксиом не следуют. Впервые это было доказано в 1980 году[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.
—-
Больше интересного — в Телеграм-канале