В 1931 году 25-летний Курт Гёдель написал доказательство, которое перевернуло мир математики с ног на голову. Выводы были настолько поразительными, а само доказательство настолько изящным, что это было… как-то даже забавно. Я хотел поделиться с вами его открытием.
Объединение
На протяжении последних 300 лет математики и ученые делали поразительные открытия, которые привели к появлению одной великой закономерности. Эта закономерность заключалась в объединении: идеи, которые раньше считались разрозненными и непохожими, неизменно оказывались одним и тем же!
Ньютон положил начало этому процессу в физике, когда обнаружил, что то, что удерживает нас на Земле, — это то же самое, что заставляет Землю вращаться вокруг Солнца. Люди думали, что тепло — это особый вид энергии, но оказалось, что его можно объяснить с помощью механики. Люди думали, что электричество, магнетизм и свет — это разные вещи, но Максвелл обнаружил, что их можно объяснить с помощью электромагнитного поля.
Дарвин сделал то же самое для биологов. Оказалось, что наши подбородки, красивые перья птиц, рога оленей, разные цветы, мужской и женский пол, причина, по которой вам так нравится сахар, причина, по которой киты плавают по-разному, все это можно объяснить естественным отбором.
Математики вели аналогичную борьбу за объединение. Они хотели найти «основные» принципы математики, из которых можно было бы вывести все истинные теории. Это объединило бы логику, арифметику и так далее под одной простой крышей. Чтобы понять, о чем идет речь, задайте себе следующий вопрос: откуда мы знаем, что 3 меньше 5? Или что 1 идет перед 2? Является ли это «основным» принципом, который мы принимаем на веру (официальное название этого — «аксиома»), или его можно вывести из какого-то еще более основного принципа? Являются ли числа фундаментальными понятиями, или их можно вывести из чего-то еще более фундаментального?
Кризис
Математики добились больших успехов в этой борьбе за основные принципы. Например, некий господин по имени Фреге обнаружил, что может создать теорию множеств, способную описывать практически всё. Что касается чисел, например, он мог поступить примерно так:
Здесь он обозначил 0 как пустое множество, 1 — как множество, содержащее множество для 0, а 2 — как множество, содержащее множества для 1 и 0. На этом основании он смог сформулировать принцип получения «следующего» числа: просто объединить все предыдущие числа в одно множество. Довольно круто! Фреге смог использовать это и доказать арифметические правила, такие как «1 + 1», «числа бесконечны» и т. д.
Это выглядело впечатляюще и круто, но появился Бертран Рассел и одним махом разрушил эту теорию.
Он использовал правила, сформулированные Фреге, чтобы сделать верное, но бессмысленное утверждение. Он доказал нечто аналогичное 1 + 1 = 3. Это звучит безобидно; в конце концов, это было всего лишь одно утверждение. Но тем не менее это было катастрофой для фундаментальной теории математики. Если можно доказать, что 1 + 1 = 3, то нельзя доверять ни одному истинному утверждению, вытекающему из этого фундамента.
Это привело математиков в замешательство. Они даже назвали этот период «фундаментальным кризисом математики».
Программа Гильберта
Стремясь решить эту проблему, математик по имени Гильберт сформулировал ряд требований к тому, как должна выглядеть фундаментальная теория математики [2]. Он заявил, что эта теория должна представлять собой новый язык с набором правил, удовлетворяющих двум основным условиям:
Теория должна была быть способна доказать любое истинное математическое утверждение. Например, представьте себе утверждение 1 + 1 = 2. Если этот язык не может доказать это утверждение, то он, безусловно, не может доказать всю математику. Гильберт назвал это свойство полнотой. Язык должен был быть полным.
Второе строгое требование, как мы обсуждали ранее, заключалось в том, что он не мог доказать ложное математическое утверждение. Если бы мы могли доказать, что 1 + 1 = 3, то все было бы напрасно. Гильберт назвал это «согласованностью». Язык должен быть согласованным.
Рассел и Уайтхед
Бертран Рассел, тот самый джентльмен, который опроверг теорию Фреге, совместно с Альфредом Нортом Уайтхедом разработал собственную теорию. Они трудились годами, чтобы создать огромный труд под названием «Principia Mathematica».
Они начали с создания нового языка (назовем его PM) с несколькими простыми правилами. Взяв эти правила, они приступили к доказательству целого ряда вещей. Рассел и Уайтхед почти ничему не верили на слово. Например, давайте посмотрим на это почти нечитаемое доказательство (не волнуйтесь, вам не нужно понимать синтаксис для этого эссе):
Это доказательство показало, что «1 + 1» действительно равно «2». Чтобы прийти к этому, потребовалось два тома.
Их язык был плотным, а работа — кропотливой, но они продолжали доказывать целую кучу различных истин в математике, и, насколько можно было судить в то время, противоречий не было. Предполагалось, что, по крайней мере теоретически, можно взять эту основу и в конечном итоге расширить ее за пределы математики: можно ли закодировать в чистой логике, как ведет себя собака или как думают люди?
Появление Гёделя
Казалось, что «Principia Mathematica» вполне может служить основополагающей теорией математики. До тех пор, пока не появился Гёдель.
Он доказал, что в «Principia Mathematica» действительно содержатся истинные математические утверждения, которые невозможно доказать с помощью этого языка. «Principia Mathematica» оказалась неполной.
Это было поразительно, но его доказательство шло ещё дальше. Он показал, что вся затея, лежащая в основе Программы Гильберта — найти формальное основание для математики — никогда не могла сработать.
Трудно поверить, что человек действительно мог доказать, что что-то «никогда» не может произойти. И все же вот он, Гёдель… 25-летний молодой человек, который доказал вне всякого сомнения, что эта затея была невозможна. Он сделал это, показав, что если язык может представлять числа, то неизбежно появятся недоказуемые утверждения.
Давайте на секунду задумаемся об этом: числа кажутся такими простыми и легко доказуемыми — просто «1», «2», «3»… и так далее. Люди думали, что в конечном итоге мы сможем записать, как думают люди — представьте, как они должны были быть шокированы, увидев, что мы не можем доказать все истины о… числах.
Давайте посмотрим, как Гёдель это сделал.
Язык Рассела и Уайтхеда был сложен для чтения. Нет ничего плохого в том, чтобы немного изменить некоторые из их символов. Давайте преобразуем их язык в нечто более понятное для программистов.
Можно представить, что Рассел и Уайтхед придумали язык, похожий на Lisp. Вот как выглядел их синтаксис:
Во-первых, у них было несколько символов для арифметических операций.
Символ | Значение | Пример |
|---|---|---|
0 | zero |
|
next | the next successor |
|
+ | plus |
|
* | times |
|
= | equals |
|
Используя только эти символы, они могли бы обозначить все натуральные числа. Если бы они доказали, что символ 0 работает как 0, а символ next — как функция преемника, то (next 0) мог бы обозначать 1, (next (next 0)) — 2 и так далее.
Вот как они могли бы записать выражение 1 + 1 = 2:
(= (+ (next 0) (next 0))
(next (next 0)))
Теперь, я добавлю одно правило. Если вы когда-нибудь увидите, что я использую в PM-Lisp натуральное число, отличное от 0 (например, «15»), можете считать, что это сокращённая запись выражения (next (next (next …)))) столько раз. В данном случае «15» означает, что функция next применяется к 0 15 раз
Символ | Значение | Пример |
|---|---|---|
|
|
означает |
(Далее (каламбур)), они придумали несколько символов для обозначения логических операций:
Символ | Значение | Пример |
|---|---|---|
not | not |
|
or | or |
|
when | when ... then .. |
Когда 0, то существует либо 0, либо 1. |
there-is | there is ... such that ... |
|
Эти символы тесно связаны с логическими выражениями, к которым мы привыкли в программировании. Самым необычным из них является «there-is». Рассмотрим один из таких примеров:
(there-is x (= 4 (* x 2)))
Здесь утверждается, что существует некоторое число x, такое, что (* x 2) равно 4. Да, это действительно так: x = 2. Это довольно круто — мы только что сформулировали общее арифметическое утверждение.
Но откуда взялось это x? Нам нужно учесть это в нашем языке:
Символ | Значение |
|---|---|
a...z, A...Z | variable(переменная) |
Чтобы выразить общие истины, Рассел и Уайтхед ввели переменные. Вот как они могли бы, например, вывести значение «and»:
(not (or (not A) (not B)))
Если это утверждение верно, то и A, и B должны быть верны!
Очень круто. Еще один трюк для нашего эссе. Чтобы текст читался легче, я иногда буду вводить новые символы. Они не будут частью языка, но могут стать удобной сокращенной записью для нас.
Символ | Значение | Пример |
|---|---|---|
| определить |
то же самое, что и |
Теперь мы можем написать (and 1 2)
Аксиомы PM-Lisp
Все, что мы видели выше, — это символы. Они пока не имели никакого значения.
Расселу и Уайтхеду нужно было доказать, что это 0работает как ноль, а это =работает как равенство . Чтобы вдохнуть жизнь в эти символы, они начали с нескольких основных принципов — аксиом.
Вот что они выбрали:
Аксиома | Пример |
|---|---|
| если либо яблоки, либо яблоки, то яблоки |
| если яблоки, то либо яблоки, либо бананы |
| если яблоки или бананы, то бананы или яблоки |
| если яблоки, бананы или груши, то бананы, яблоки или груши |
| если яблоки — это фрукты, то выражение «бананы или яблоки» означает «бананы или фрукты» |
Вот и всё. Этого было достаточно, чтобы принять их на веру. Они взяли эти правила и кропотливо соединили их сложными способами, чтобы вывести из них всё остальное.
Например, вот как они вывели = :
(def = (and (when A B) (when B A)))
Если из A следует B, а из B следует A, то они должны быть равны! Представьте себе, что это повторяется на сотнях и сотнях страниц.
Обратите внимание на один важный момент: их правила настолько точны, что не оставляют места для человеческого суждения; их может выполнять компьютер. Это стало ключевым компонентом фундаментальной теории математики: если правила настолько просты, что их можно реализовать в виде алгоритма, то мы сможем избежать ошибок, связанных с человеческим суждением.
Первая идея Гёделя
Итак, Гёдель хотел изучить язык Рассела и Уайтхеда. Но изучать символы довольно сложно. Как рассуждать об отношениях между ними?
Ну, есть одна вещь, которую можно изучать очень хорошо… числа! И тогда ему пришла в голову идея: а что, если бы он смог выразить весь язык PM-Lisp с помощью чисел*?*
Вот что он сделал:
Символы
Сначала он взял все символы и присвоил им номера:
Символ | Число Гёделя |
|---|---|
( | 1 |
) | 3 |
0 | 5 |
next | 7 |
+ | 9 |
* | 11 |
= | 13 |
not | 15 |
or | 17 |
when | 19 |
there-is | 21 |
a | 2 |
b | 4 |
c | 6 |
Предположим, он захотел бы указать время. Он мог бы просто написать «19». Это неплохо, но не решает всех задач: как же ему обозначить формулы?
Формулы Он придумал решение и для формул. Он установил правило:
Возьмите любую формулу, например такую:
(there-is a (= (next 0) a))
и преобразовать каждый символ в соответствующее число Гёделя:
token | ( | there-is | a | ( | = | ( | next | 0 | ) | a | ) | ) |
|---|---|---|---|---|---|---|---|---|---|---|---|---|
Число Гёделя | 1 | 21 | 2 | 1 | 13 | 1 | 7 | 5 | 3 | 2 | 3 | 3 |
Затем возьмите список простых чисел, упорядоченных по возрастанию, и возведите каждое из них в степень, равную числу Гёделя:
простое Число Гёделя | 2¹ | 3²¹ | 5² | 7¹ | 11¹³ | 13¹ | 17⁷ | 19⁵ | 23³ | 29² | 31³ | 37³ |
|---|
Умножьте их все вместе, и вы получите вот такое огромное число:
25777622821258399946386094792423028037950734506637287219050
В этом числе есть одна очень интересная особенность. Поскольку оно состоит исключительно из возрастающих простых чисел, его уникальность гарантирована! Это означает, что каждую формулу PM-Lisp можно представить с помощью уникального числа Гёделя!
Доказательства
Формулы — это замечательно, но они составляют не всё в PM-Lisp. Нам также хотелось бы поддерживать доказательства. В доказательстве у нас будет «последовательность» формул:
(there-is a (= (next 0) a))
(there-is a (= a (next 0)))
Он снова применил тот же трюк, но на этот раз к каждой формуле по отдельности:
Формула Гёделя |
|
|
|---|---|---|
Число Гёделя | 25777622821258399946386094792423028037950734506637287219050 | 76887114166817775146256448336954145299389470803180389491850 |
Простое число Гёделя | 225777622821258399946386094792423028037950734506637287219050 | 376887114166817775146256448336954145299389470803180389491850 |
А теперь, если мы возьмем
2^25777622821258399946386094792423028037950734506637287219050 * 3^76887114166817775146256448336954145299389470803180389491850
Мы получили бы одно гигантское число. Только первый член этого выражения имеет 7 октодециллионов цифр! (Один октодециллион сам по себе состоит из 58 цифр.) Но это ещё не всё. Это гигантское число однозначно представляет доказательство, которое мы только что написали!
Внезапно Гедель смог однозначно представлять символы, формулы и даже доказательства с помощью чисел Геделя!
PM-Lisp на PM-Lisp
Теперь мы можем использовать математику для изучения отношений между числами: например, «как связаны четные числа и простые числа?», «бесконечны ли простые числа?» и так далее. Точно так же, как мы могли использовать математику для изучения простых чисел, Гёдель понял, что он может использовать математику для изучения «всех чисел, представляющих доказательства PM-Lisp»!
Теперь, какой язык он мог бы использовать для изучения этих отношений? Ну, Рассел и Уайтхед позаботились о том, чтобы сам PM-Lisp отлично подходил для изучения чисел… и он, безусловно, хорошо работал для изучения простых чисел… так почему бы не использовать PM-Lisp для изучения «всех чисел, представляющих доказательства PM-Lisp»?
И это именно то, что сделал Гёдель: он использовал PM-Lisp, для изучения PM-Lisp!
Конечно, это не то, что задумывали Рассел и Уайтхед, но тем не менее это было возможно. Давайте посмотрим на несколько примеров, чтобы понять, о чем мы говорим.
Описание формул
Предположим, у вас есть такая формула:
(there-is a (= (next 0) a))
А что, если бы мы захотели доказать утверждение «Второй символ в этой формуле — это ‘there-is’»?
Ну, если бы у нас было число Гёделя для этого:
25777622821258399946386094792423028037950734506637287219050
Нам нужно всего лишь написать в PM-Lisp:
«Наибольший делитель этого числа Гёделя, кратный 3, равен 321».
Если бы мы сказали это… это было бы равносильно утверждению, что второй символ (простое число 3) «существует» (число Гёделя 21)! Очень круто.
Что ж, эту зависимость очень просто выразить в PM-Lisp. Начнём с написания формулы, проверяющей, является ли одно число делителем другого:
(there-is x (= (* x 5) 30))
В этом утверждении говорится, что существует такое x, при котором (* x 5) должно равняться 30. Если x = 6, то это сходится, а значит, утверждение верно. Ну, это соответствует идее, что 5 — делитель числа 30! Итак, давайте сделаем это «сокращением» для факторизации:
(def factor? (there-is x (= (* x y) z)))
Тогда в нашем утверждении можно использовать фактор?
(and
(factor? x 3^21 25777622821258399946386094792423028037950734506637287219050)
(not (factor? x 3^22 25777622821258399946386094792423028037950734506637287219050)))
В этом утверждении говорится, что 321 является делителем нашего числа, а 322 — нет. Если это верно, значит, 321 — это наибольший делитель 25777622821258399946386094792423028037950734506637287219050, кратный 3. И если это верно, то PM-Lisp только что сказал что-то об этой формуле: он сказал, что второй символ должен быть there-is!
Построение формул
Мы можем пойти дальше. Мы можем даже строить формулы PM-Lisp в PM-Lisp! Представьте, что у нас есть набор вспомогательных операторов для простых чисел и экспонент:
(def prime? ...) ; (prime? 5) ; true
(def largest-prime ...) ; (largest-prime 21) ; 7
(def next-prime ...) ; (next-prime 7) ; 11
(def expt ...) ; (expt 10 3) ; 1000
Поскольку PM-Lisp полностью посвящён математике, можно представить, что Рассел и Уайтхед глубоко изучили простые числа и предложили нам эти удобные утверждения. Теперь мы могли бы написать формулу, которая «добавляет» символ ' ) ', например:
(* n (expt (next-prime (largest-prime n)) 3))
Допустим, n — это число Гёделя для выражения (there-is a (= (next 0) a)).
Вот что означает это утверждение:
Найдите наибольшее простое число для n: 37 Найдите следующее простое число после него: 41 Умножьте n на 41^3 Умножение n на 41^3 будет эквивалентно добавлению лишней скобки )! Просто головоломка.
И вот Гёдель задался вопросом: какие ещё виды утверждений мы могли бы сформулировать? Могли бы мы сформулировать такое утверждение:
(successor? a b)
Это можно было бы сформулировать так: «Формула с номером Гёделя a вытекает из формулы с номером Гёделя b».
Оказывается… это верное и доказуемое утверждение в PM-Lisp! Математическое доказательство немного сложно для понимания, но интуитивное мы можем хорошо уловить.
Учтите, что в PM-Lisp, чтобы перейти от одного утверждения к следующему, необходимо свести все к одной из аксиом, сформулированных Расселом и Уайтхедом!
Например, из предложения p мы можем применить аксиому (when p (or p q)), так что одним из допустимых следующих утверждений может быть (or p q). Оттуда мы можем использовать другие аксиомы: (when (or p q) (or q p) поможет нам преобразовать это в (or q p). И так далее.
Мы уже видели, что можем использовать PM-Lisp для «изменения» формул (например, как мы добавили дополнительную скобку в конце). Можем ли мы написать более сложные утверждения, которые могут «генерировать» следующие возможные последователи из утверждения и этих аксиом?
Например, чтобы перейти от p к (or p q), нам просто понадобится математическая функция, которая принимает число Гёделя для p и выполняет эквивалентные умножения, которые добавляют (or в начало и q в конец).
Оказывается, это можно сделать с помощью серьезной математики, связанной с простыми числами! Ну, если это возможно, то мы могли бы проверить, является ли следующее утверждение в последовательности действительным:
(def successor? (one-of b (possible-successors a)))
Это утверждение гласит: «Один из возможных последующих чисел Гёделя, вытекающих из формулы с числом Гёделя a, равен формуле с числом Гёделя b». Если это верно, то b действительно должен быть последующим числом Гёделя по отношению к a.
Отлично! PM-Lisp может утверждать, что одна формула вытекает из другой.
(proves a b)
Если мы можем доказать, что формула является последующей, можно ли сказать что-то большее?
Как насчет утверждения (доказывает a b)? Оно будет означать: «последовательность формул с числом Гёделя, a доказывает формулу с числом Гёделя b».
Что ж, давайте подумаем об этом. Получить «список» формул с числами Гёделя из a довольно просто: достаточно извлечь показатели степени из простых чисел. PM-Lisp, безусловно, может это сделать.
Ну, у нас уже есть функция successor? Мы могли бы просто применить ее к каждому утверждению, чтобы убедиться, что оно является действительным преемником!
(and
(every-pair sucessor? (extract-sequence a))
(successor? (last-formula a) b))
Там есть много абстракций, о которых я не говорил — every-pair, extract-sequence и т. д. — но можно почувствовать, что каждая из них, безусловно, является математической операцией: от извлечения экспонент до проверки того, что число Гёделя является прямым преемником.
Вышеуказанное утверждение фактически означало бы:
«Каждая формула в последовательности с числом Гёделя a является прямым преемником и подразумевает число Гёделя b».
Гёдель приложил немало усилий, чтобы доказать это в своей статье. Для нас, думаю, достаточно интуиции. Используя PM-Lisp, мы теперь можем высказать некоторые глубокие истины о PM-Lisp, такие как «это доказательство подразумевает это утверждение» — безумие!
(subst a b c) Есть еще одно последнее утверждение, которое он доказал. Представьте, что у нас есть такая формула
(there-is b (= b (next a)))
Число Гёделя будет равно 26699108848097731568417316859014651425159900891216992323750
Это означает: «Существует число b, которое на единицу больше a».
А что, если мы захотим заменить символ a на 0?
Ну, это будет сложная, но понятная задача: нам просто нужно заменить все экспоненты, равные 2 в этом числе (помните, что 2 — это число Гёделя для символа a), на 5 (число Гёделя для 0).
(replace-exponent
26699108848097731568417316859014651425159900891216992323750
2
5)
Опять же, это выглядит как довольно простой математический расчёт, и можно предположить, что PM-Lisp способен его выполнить. Это потребует немало математических операций — извлечения экспонент, умножения — но всё это останется в разумных логических пределах.
Гёдель доказал, что эта функция также является доказуемым утверждением в PM-Lisp. Например, приведённое выше выражение даст число Гёделя, представляющее эту формулу:
(there-is b (= b (next 0)))
Невероятно! a заменяется на 0. Теперь PM-Lisp может производить подстановки в формулах PM-Lisp. Могу себе представить, что, увидев это, Рассел и Уайтхед почувствовали легкое недомогание.
Подозрительное использование subst
Если они еще не почувствовали недомогания, то это, безусловно, заставило бы их почувствовать его:
(subst
26699108848097731568417316859014651425159900891216992323750
2
26699108848097731568417316859014651425159900891216992323750)
Здесь a заменяется на число Гёделя самой формулы!
В этом случае формула будет выглядеть следующим образом:
(there-is b (= b (next 25777622821258399946386094792423028037950734506637287219050)))
Странно использовать номер Гёделя самой формулы внутри формулы, но в конце концов это всего лишь число, так что всё вполне допустимо и логично.
Очень круто: теперь PM-Lisp может определить, является ли то или иное доказательство верным, и даже заменять переменные внутри формул!
Гёдель объединил эти формулы в потрясающую симфонию. Давайте проследим за этим:
Он начинает с этого:
(proves a b)
Пока что это означает: «последовательность с номером Гёделя a доказывает формулу с номером Гёделя b»
Далее он ввёл оператор «there-is»
(there-is a (proves a b))
До сих пор речь шла о том, что «существует некоторая последовательность с номером Гёделя a, которая доказывает формулу с номером Гёделя b».
Теперь он вставил примечание not :
(not (there-is a (proves a b)))
Это означало бы:
«Не существует последовательности, доказывающей верность формулы с числом Гёделя b»
Затем он вставил subst :
(not (there-is a (proves a (subst b 4 b))))
Ого, что за… Ладно, здесь говорится:
«Не существует последовательности, которая бы доказывала формулу, получаемую, если взять число Гёделя для b и заменить 4 (число Гёделя для символа «b») самим числом Гёделя b!
Пока всё понятно. Но что такое b в данный момент? Это может быть что угодно. Давайте определим конкретное значение:
А что, если взять число Гёделя
(not (there-is a (proves a (subst b 4 b))))
Это будет невероятно большое число. Давайте назовём его...G
А что, если мы заменим bна G?
(not (there-is a (proves a (subst G 4 G))))
Интересно... что это значит?
Формула Гёделя
Давайте посмотрим на это еще раз:
(not (there-is a (proves a (subst G 4 G))))
Это означает: «Нет доказательства формулы, получаемой при принятии „формулы с числом Гёделя G“» — напомним, что G — это число Гёделя для:
(not (there-is a (proves a (subst b 4 b))))
«И заменить b на G»… в результате чего для формулы получится число Гёделя:
(not (there-is a (proves a (subst G 4 G))))
Постойте-ка! Это же та формула, с которой мы только что начали.
А это значит, что
(not (there-is a (proves a (subst G 4 G))))
Это означает: «Меня невозможно доказать в PM-Lisp».
Во что верить
Это интересное утверждение, но правда ли это? Давайте на мгновение задумаемся:
«Эту формулу невозможно доказать на языке PM-Lisp».
Если бы это было правдой:
Это означало бы, что PM-Lisp является неполным : не все истинные математические утверждения могут быть доказаны в PM-Lisp. Это предложение было бы примером утверждения, которое нельзя доказать.
Но если это не так:
Тогда это означало бы, что PM-Lisp мог бы доказать утверждение «Эта формула недоказуема в PM-Lisp». Но если бы он мог доказать это утверждение, то оно было бы ложным! Эта формула доказуема, верно? Так как же мы можем доказать, что она недоказуема? Это сделало бы наш язык непоследовательным — это просто доказало бы ложность утверждения, аналогично утверждению 1 + 1 = 3!
Таким образом, Гёдель пришёл к поразительному выводу: если PM-Lisp непротиворечив , то он должен быть неполным. Если же он полон, то он должен быть противоречивым.
Сила чисел
Это был удар для Рассела и Уайтхеда, но как насчет Гильберта? Могли бы мы просто придумать какой-нибудь новый язык, который позволил бы этого избежать?
Как только язык сможет представлять целые числа, он попадёт в ту же ловушку: Гёдель сможет просто сопоставить язык с числами, создать допустимую successor?функцию и получить эквивалентное утверждение «Я недоказуем в X».
Это противоречило мечтам многих математиков: даже арифметика обладала качеством, которое нельзя было свести к аксиомам.
В программировании это означает: существуют истины, которые невозможно записать в виде алгоритма. В этом суть открытия Гёделя.
Он продолжил доказывать ещё несколько удивительных вещей. Оказалось, что он мог написать похожее, корректное предложение, которое гласило: «Я не могу доказать, что я последователен». Это означало, что ни одна формальная система не могла бы самостоятельно доказать, что она способна выдавать только истинные утверждения.
Однако это не означает, что все усилия напрасны. Например, это может означать, что мы не сможем написать алгоритм, способный мыслить как собака... но, возможно, нам это и не нужно. Подобно тому, как нейроны не осознают любовь собаки к игрушкам, нашим алгоритмам тоже не нужно будет этого осознавать: возможно, сознание возникнет как эпифеномен таким же образом. Идея «мыслить как собака» просто не будет конкретно зафиксирована.
Мы не можем доказать непротиворечивость одной системы, но мы могли бы доказать это, используя другую систему. Но, конечно, возникает вопрос: как мы могли бы доказать непротиворечивость другой системы ? И так далее!
Я воспринимаю идею Гёделя как руководство: она показывает нам пределы того, что мы можем сделать с помощью предписывающих алгоритмов. И то, что он сделал, мне кажется чертовски забавным. Рассел и Уайтхед приложили немало усилий, чтобы избежать самореференции в своей работе. В некотором смысле Гёдель обошел это, создав первый «метациклический оценщик» — язык, который интерпретировал сам себя, — и в результате пришел к некоторым неожиданным выводам.
Если вы хотите поэкспериментировать с созданием собственных чисел Гёделя, вот небольшой скрипт на Clojure .
Оплата зарубежных сервисов в рублях — по ссылке. (Visa/Mastercard с Apple Pay) Для ПК —ссылка.
