Давид Гильберт, «О бесконечности»· (1925)
Арифметика — это область математики, в которой говорится о свойствах сложения и умножения натуральных чисел: 1, 2, 3, 4, 5, 6, 7,...; она включает в себя такие понятия, как простые, совершенные, треугольные или четные числа. Теория образована всеми утверждениями (также называемыми предложениями, или высказываниями), связанными с этими понятиями, например «1 + 1 = 2», «2 — четное число», «5 — простое число», «любое число, делящееся на 4, четное» или «сумма двух нечетных чисел дает в результате четное число». Аксиомы, которые искал Гильберт, были бы множеством базовых истин, из которых можно вывести, при уже изложенных условиях, все остальные истинные арифметические утверждения, в том числе упомянутые выше.
С другой стороны, что означает алгоритмическая проверка справедливости рассуждений, доказывающих эти истины? Это означает, что по крайней мере в начале должно быть возможным так запрограммировать компьютер, чтобы за конечное количество шагов он мог определить, является ли доказательство справедливым. В соответствии с этой идеей мы вводим доказательство в машину, она обрабатывает его по предварительно написанной программе и через некоторое время (возможно, долгое, но в любом случае конечное) говорит нам, справедливо рассуждение или в нем содержится ошибка.
В целом проверка правильности математического доказательства — непростая работа, иногда даже для специалистов. Например, когда в 1995 году Эндрю Уайлс представил свое доказательство последней теоремы Ферма, которому он посвятил семь лет, специалисты, его проверявшие, нашли логический пробел — шаг, который, насколько они понимали, не был должным образом обоснован. Уайлс, естественно, этой ошибки не заметил, и ему потребовался год на ее исправление. В конце концов в 1996 году он представил полное доказательство.
Продемонстрируем менее сложный пример. Пусть а и b — два числа, которые мы считаем равными и при этом отличными от нуля. На основе того факта, что а = b, мы можем получить «доказательство» того, что 1 = 2 (для большей ясности пронумеруем логические шаги рассуждения).
1. а = b По гипотезе. 2. a · b = b · b Умножили оба члена на Ь. 3. a · b = b² Заменили b · b на b². 4. a · b - a² = b² - a² Вычли а² из обоих частей. 5. a · (b - a) = (b + a) · (b - a) Использовали известные алгебраические равенства. 6. a = b + a Сократили (b - а) в обеих частях. 7. a = a + a Заменили b на а> поскольку числа равны. 8 a = 2 · a Использовали равенство а + а = 2 · а. 9. 1 = 2 Разделили обе части на число а.
Очевидно, что это рассуждение неверно, но где ошибка? Она находится в переходе от шага 5 к шагу 6. В равенстве
а · (b - а) = (b + а) · (b - а)
мы сокращаем скобки (b - а) и делаем вывод, что а = b + а. Это ошибочно, потому что (b - а) равно 0 (поскольку а = b), а 0 нельзя делить. Если представить это в виде чисел и предположить, например, что а и b равны 2, переход от 5 к 6 соответствует тому, чтобы сказать, что из 2 · 0 = 4 · 0 (что истинно) следует 2 = 4.
Но как мы можем научить компьютер обнаруживать ошибки такого типа? Компьютер — это только машина; он не рассуждает, а слепо следует программе, записанной в его памяти. Для того чтобы компьютер мог проверить правильность математического рассуждения, необходимо перевести это рассуждение в последовательность высказываний, каждое из которых либо аксиома, либо выводится из предыдущих высказываний посредством применения точных и заранее установленных логических правил.
Рассмотрим пример математического доказательства, выраженного таким образом. Для начала нам нужны некоторые аксиомы, которые будут служить нам отправной точкой. В 1889 году, задолго до открытия парадокса Рассела, итальянский математик Джузеппе Пеано предложил набор аксиом, которые (как он предполагал) позволяют доказать все арифметические истины. Эти аксиомы основывались на операциях сложения (+), произведения (·), а также понятии последующего элемента (обозначаемого буквой S).
Пеано понимал, что последовательность натуральных чисел получается на основе числа 1 посредством повторного применения функции последующего элемента. Таким образом, 2 определяется как последующий элемент для 1, что обозначается S (1) = 2; 3, по определению, — последующий элемент для 2, то есть S (2) = 3; и так до бесконечности.
Для нашего примера достаточно взять две аксиомы Пеано, относящиеся к сложению.
Аксиома 1: каким бы ни было число х, х + 1 = S(x).
Аксиома 2: какими бы ни были числа х и у, S(x + у) = х + S(у).
В первой аксиоме говорится, что последующий элемент числа х всегда получается прибавлением к нему 1. Вторую аксиому можно воспринимать как (x+y) + 1 = x + (y +1). На основе этих двух аксиом докажем, что 4 = 2 + 2.
Логическая структура доказательства того, что 4*2 + 2. Стрелки показывают применения правил вывода.
Но действительно ли нужно доказывать, что 4 = 2 + 2? Разве это не очевидный факт? Хотя это действительно очевидно, по программе Гильберта любое истинное утверждение, не являющееся аксиомой, должно доказываться на их основе. За исключением высказываний, которые явно указаны как аксиомы, нет других утверждений, которые сами по себе считаются истинными.
Итак, докажем, что 4 = 2 + 2, но запишем рассуждение таким образом, чтобы его мог обработать компьютер. Добавим несколько комментариев, чтобы мы, люди, могли следить за идеей (см. схему).
1. S(x + у) = х + S(y) Аксиома 2.
2. S(2 + 1) = 2 + S(1) Подставили х=2 и у= 1 в аксиому 2.
3. S(2 + 1) = 2 + 2 Заменили S(1) на 2 в предыдущем шаге.
Комментарий: в следующих трех шагах представлено небольшое поддоказательство того, что 2 + 1 = 3; таким образом, в шаге 3 мы можем заменить S(2 + 1) на S(3).
4. х +1 = S(x) Аксиома 1.
5. 2 + 1 = S(2) Подставили = 2 в аксиому 1.
6. 2 + 1 = 3 В предыдущем шаге заменили 5(2) на З.
Комментарий: теперь мы можем заменить 5(2 + 1) на 3 в третьем шаге.
7. S( 3) = 2 + 2
8. 4 = 2 + 2 Заменили S(3) на 4 в предыдущем шаге.
Нужна ли такая точность для доказательства того, что два плюс два равно четыре? Да, это необходимо, если мы хотим, чтобы компьютер был способен проверять правильность рассуждений. Компьютер не думает; следовательно, мы должны вести его за руку, шаг за шагом показывая ему, используя заранее установленные правила, что именно мы сделали на каждом этапе рассуждений.
Действительный мир есть мир, постоянно изменяющийся. [...] Но такие изменения, независимо от их силы, никогда не разрушат истинности отдельного логического или арифметического закона.
Рудольф Карнап. «Философские основания физики»
Что будет делать компьютер, чтобы проверить, правильно ли наше доказательство? Для начала он возьмет первое высказывание и проверит, является ли оно аксиомой. Эта проверка происходит от символа к символу, точно так же как текстовый редактор проверяет орфографию, буква за буквой сверяя слова со словарем, загруженным в память компьютера.
Вспомним, что каждое высказывание должно либо быть аксиомой, либо выводиться из предыдущих высказываний. В нашем примере машина убедилась бы, что первое высказывание — это одна из аксиом в списке (первое высказывание должно быть аксиомой, его нельзя вывести из предыдущих высказываний, просто потому что их нет). Компьютер, конечно же, не понимает значения аксиомы, он только проверяет, что первое высказывание присутствует в списке, предварительно в него загруженном.
После первой проверки машина переходит ко второму высказыванию, S(2 + 1) = 2 + S(1), и проверяет, что это не аксиома (поскольку ее нет в списке). Тогда это второе высказывание должно сводиться к первому с помощью какого-либо логического правила. Чтобы осуществить эту проверку, в память компьютера должен быть загружен список правил логики, то есть правил, которые показывают, какие выводы можно сделать из определенных предпосылок (см. схему).
В случае нашего доказательства правило, позволяющее перейти от шага 1 к шагу 2, заключается в том, что если высказывание начинается с «какими бы ни были числа х и y...», то в следующем выражении буквы х и у могут быть свободно заменены любыми числами. В нашем примере буква х заменена числом 2, а у — числом 1.
