30.08.2024 14:52
seregablog 3 4900 Источник

Введение

Во время обеда к вам подошёл коллега-программист и заявил, что математика программисту и не нужна вовсе. Вчера он взял учебник 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.

—-

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

Комментарии (3)


  1. MasterMentor
    30.08.2024 16:46
    #27228956
    +5

    Что называется, сыграем в игру "найди отличия":

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

    https://habr.com/ru/articles/839896/

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

    https://ru.wikipedia.org/wiki/Задача_Тарского_по_школьной_алгебре

    PS Я не сказал, что это плохо (в аспекте привлечения интереса к алгербе - это хорошо); я сказал, что отличий нет.


  1. MasterMentor
    30.08.2024 16:46
    #27229092
    +2

    Теперь пару слов по написанному или о математеке.

    Читаем: "Задача Тарского существует ли тождество над целыми положительными (или натуральными) числами" с перечнем аксиом для поля целых чисел (для полноты добавим, правда, что, без нулевого элемента, но сути это не меняет). Читаем далее: "чтобы это доказать, достаточно разделить второй член в обеих частях". Слова "разделить" и "поле целых" - из разных опер вообще (от слова "совсем").

    Вопрос: когда? кто? где? доказал, что можно использовать операцию "деление" в преобразованиях при работе с задачей. Ни в Вики, ни у Вас я об этом ничего не нашёл.

    PS "Аргументы" в форме ссылок вроде тех, что в статье (мол, ищи сам, если тебе это нужно) - не принимаются. Данные ссылки ведут в никуда (я не поленился, загуглил, и не нашёл этих источников).

    Зато нашёл это:

    The equational theory of ⟨N, 0, 1, +, ×, ↑⟩ is decidable, but not finitely axiomatisable Roberto Di Cosmo and Thomas Dufour
    https://www.dicosmo.org/Papers/zeroisnfa.pdf

    Скрытый текст

    В 1969 году Тарский задал вопрос, являются ли арифметические тождества, преподаваемые в средней
    школе, полными, чтобы показать все арифметические уравнения, справедливые для натуральных
    чисел. Мы знаем ответ на этот вопрос для различных подсистем, полученных
    различными способами ограничения языка арифметических выражений, но до сих пор
    мы ничего не знали об оригинальной системе, которую рассматривал Тарский, когда начинал все
    эти исследования, а именно о теории целых чисел в виде суммы, произведения, возведения
    в степень с двумя константами для нуля и единицы.
    Эта статья закрывает эту давнюю открытую проблему, предоставляя элементарное
    доказательство, основанное на предыдущей работе Р. Гуревича, того факта, что исходная
    система Тарского разрешима, но не является конечно приближенной.

    ...

    Мы доказали, что ⟨N, 0, 1, +, ×, ↑⟩ имеет разрешимую, но не
    конечно аксиоматизируемую теорию уравнений, и ясно показали, что единственное различие между ⟨N, 0, 1, +, ×, ↑⟩
    и ⟨N, 1, +, ×, ↑⟩ задается системой Z на рисунке 2.
    Как следствие, семейство равенств Гуревича не разрушается, и мы также
    получаем следующий дополнительный результат
    Теорема 8. Теория изоморфизмов типов в бик-декартовых замкнутых категориях не
    является конечно аксиоматизируемой
    это закрывает давнюю открытую проблему конечной аксиоматизируемости изоморфизмов типов для лямбда-исчисления с суммами и пустыми типами

    В переводе на русский, насколько я понял, что вместо того, чтобы пытаться "доказать" либо "не доказать" тождество, люди снала проверили аксиоматику этой задачи, и установили, что она не полная для ответа на поставленный Тарским вопрос.


  1. Tzimie
    30.08.2024 16:46
    #27229252
    +1

    То есть это аналог теоремы о неполноте, но для алгебры?