Каковы философские следствия первой теоремы Гёделя о неполноте?
Первая теорема Гёделя о неполноте утверждает
Любая эффективно порожденная теория, способная выражать элементарную арифметику, не может быть одновременно непротиворечивой и полной. В частности, для любой непротиворечивой, эффективно порожденной формальной теории, которая доказывает некоторые основные арифметические истины, существует арифметическое утверждение, которое является истинным, но недоказуемым в теории (Клин, 1967, стр. 250).
Каковы философские следствия этой теоремы? В частности, существуют ли более общие аналоги этой теоремы — обязательно «недоказуемые истины» в других видах формальных систем?
Любая эффективно аксиоматизированная формальная система, расширяющая базовую теорию формальной арифметики, называемую арифметикой Робинсона (Q), будет содержать неразрешимое предложение. В общем случае синтаксическую версию первой теоремы о неполноте можно сформулировать следующим образом:
(G1T) Для любой эффективно аксиоматизированной теории T, которая расширяет Q, существует T-предложение G такое, что: (i) Если T непротиворечиво, то T не может доказать G (ii) Если T омега-непротиворечиво, то T не может доказать ¬G.
Это самое общее утверждение теоремы, которое вы можете получить. Обратите внимание, что Клини в вашей цитате говорит о семантической версии теоремы. Однако то, что первоначально доказал Гёдель, не включало семантических понятий, таких как истина, арифметическая истина и т. д. Можете ли вы увидеть/признать/признать G как истинное или нет, зависит от семантического/интенсионального понимания G — это распространенное заблуждение, которое Гедель хотел доказать. ограничения арифметической истины. Фоном, против которого он работал, был гильбертовский формализм, поэтому его главной задачей было продемонстрировать чисто синтаксические ограничения формальных систем. Таким образом, в полной синтаксической общности (G1T) говорит (неформально), что никакие соответствующие манипуляции с символами в любой формальной системе, достаточно сложной, чтобы содержать некоторую арифметику, не приведут к G.
Итак, вы видите, что (G1T) применимо к огромному количеству формальных систем. Решите ли вы рассматривать полученное G как «недоказуемую истину », зависит от вашей семантики/от того, имеет ли ваше T предполагаемую интерпретацию и так далее. Но в большинстве случаев такой вывод считается оправданным. Но это возникает только из-за вспомогательного синтаксического сбоя, который обеспечивает (G1T).
Теперь, что касается философских выводов, литература огромна. Упомяну некоторые актуальные вопросы:
Наконец, я хотел бы сказать, что бесчисленное множество философски настроенных авторов/мыслителей/хакеров присвоили теорему Геделя, чтобы попытаться сделать выводы о самореференции/петлях/Боге/метафизике/осведомленности об окружающей среде и бог знает о чем еще. Три вывода, которые я привел, могут показаться сухими и академичными, но они также точны, хорошо изучены и лишены преувеличений. Нет сомнений в том, что теоремы Гёделя продвинули вперед наше понимание формальных систем, а вместе с ним и наше понимание философских сил и слабостей формальных рассуждений.
Я хотел бы здесь остановиться, чтобы сначала точно сформулировать и должным образом доказать теорему Гёделя. Первоначальная презентация была создана до изобретения компьютера и была сложной. Но мы живем 80 лет спустя, где знакомы компьютеры.
Во-первых, в теореме Геделя вы всегда говорите об аксиоматической системе S. Это логическая система, в которой вы можете доказывать теоремы с помощью компьютерной программы, вы должны думать об арифметике Пеано, или ZFC, или любой другой теории первого порядка с вычислимая схема аксиом (аксиомы, которые могут быть перечислены фиксированной компьютерной программой).
Предполагается, что такая система аксиом может описывать компьютер в любое конечное время. Содержимое памяти компьютера представляет собой строку битов, большое целое число M, а манипуляции с памятью от выполнения одного шага представляют собой очень простую функцию, которая что-то делает из набора инструкций и изменяет память. Если вы сделаете это конечное число раз, вы получите новое состояние памяти M'. Основное предположение о S таково:
S может следовать компьютерной программе: для фиксированного универсального компьютера с начальной памятью M он докажет, что память в момент времени t равна M' для любого конечного времени t.
В арифметике Пеано это тривиально, потому что вы можете кодировать память компьютера очень простыми способами, а аксиомы без индукции, просто аксиомы для вычислений, говорят вам, каков результат конечного вычисления. Так что это верно в арифметике Пеано без индукции и без кванторов. Очень просто спросить у системы аксиом, что она может проследить за вычислением и доказать, что результат за конечное время верен.
Затем мы предполагаем, что S может заявлять такие вещи, как «Программа P не останавливается». Это требует квантификатора
Я предполагаю, что S непротиворечиво. Утверждение «S непротиворечиво» означает, что если S доказывает, что «P не останавливается», то P на самом деле не останавливается. Поскольку, если P остановится, S будет следовать за ним до тех пор, пока он не остановится, а затем докажите и это. Обратите внимание, что S может доказать, что «P останавливается» без фактической остановки P, он просто не может доказать, что «P не останавливается», если это ложь.
Теорема. Рассмотрим такую систему аксиом S. Существует программа P, которая не останавливается, для которой S не может доказать, что «P не останавливается»:
Доказательство: Напишите компьютерную программу SPITE, которая делает следующее:
Если вы подумаете об этом на полсекунды, в тот момент, когда S докажет, что «ЗЛОП не останавливается», ЗЛОП останавливается (по построению) и делает S лжецом. Ссылка на самого себя находится в первой строке --- вывод вашего собственного кода в переменную, и то, что это возможно, является упражнением для программистов бакалавриата.
Это полная конструкция и полное доказательство.
Гёдель 2: S не может доказать свою непротиворечивость
Доказательство таково: если S непротиворечиво, SPITE не может остановиться, потому что мы видим, что это подразумевает, что S непротиворечиво. Таким образом, если S может формализовать этот аргумент и доказать свою непротиворечивость, это доказывает, что SPITE не останавливается (что невозможно).
Это полное доказательство. Требуется знакомство с логикой, чтобы увидеть, что для подходящего S неформальный вывод «S последовательно подразумевает, что SPITE не останавливается» может быть формализован в S, но если бы было невозможно формализовать интуитивные логические выводы, подобные этому, мы бы не не используйте S в первую очередь.
Россер: Проблема с Гёделем1 и Гёделем2 (которые, по сути, являются одной и той же теоремой с точностью до тривиального выбора канонического примера) заключается в том, что S может быть полным, но неверным . Другими словами, доказательство Гёделя не показало, что существует программа P, остановка которой вообще не предсказуема. Может быть, S решает, что все программы либо останавливаются, либо не останавливаются, но это неправильно: он говорит вам, что некоторые не останавливающиеся программы останавливаются. Если бы он сказал вам, что останавливающаяся программа не остановилась, это было бы противоречием в S (после достаточного времени), но он может сказать вам, что неостанавливающаяся программа останавливается без противоречия (это очевидно, но тонко).
Так пиши РОССЕР:
Теперь S не может доказать ни «РОССЕР печатает», ни отрицание «РОССЕР не печатает». Таким образом, если вторая программа следует за Россером и останавливается, когда ROSSER печатает, то эта программа не доказана ни останавливающейся, ни не останавливающейся.
Главный философский вывод — самый важный в истории философии (это не преувеличение):
Существует универсальное понятие вычисления, которое не зависит от системы аксиом.
Это главный результат работы Геделя, хотя он не был полностью понят до версии Тьюринга несколько лет спустя. Но Гёдель нащупывал это, так как очень быстро понял, что это правда, после доказательства теоремы, и признал, что объяснение дал Тьюринг, и отказался от своего собственного подхода к вычислениям в пользу тьюринговского. Причина, по которой мне может сойти с рук подобное доказательство, состоит в том, что все мы знакомы с понятиями «компьютер» и «компьютерная программа», и все мы знаем, что любой точный алгоритм может быть запрограммирован на компьютере, и что один компьютер так же хорош, как и другой.
Непосредственные философские выводы:
Существует общепринятое представление о том, что значит иметь точно определенный набор правил.
На самом деле вы можете построить машину, которая может имитировать любой другой точно определенный набор правил.
Любые две такие машины эквивалентны: A может имитировать B, а B может имитировать A.
Если физика существует (если есть точный набор правил, пусть даже вероятностных, для моделирования природы), универсальная машина (оснащенная генератором случайных чисел) может моделировать все, что угодно в природе.
Отсюда следует, что:
Полное поведение человека может быть смоделировано универсальным компьютером.
С правдоподобным логическим позитивистским предположением это означает, что
Компьютер — это машина, способная мыслить.
Это понимание принадлежит Тьюрингу. У фон Неймана есть следующее понимание:
Компьютер — это машина, способная моделировать поведение биологических систем. Теорема Геделя аналогична самовоспроизведению.
Это бесспорно самые важные философские открытия всех времен. Предшественником этого являются попытки Либница создать философскую машину, которая могла бы рассуждать механически. Лейбниц понимал некоторые последствия использования компьютера.
Теорема Геделя показала, что если принять философскую позицию, согласно которой утверждение «программа P не останавливается» абсолютно осмысленно, то не существует фиксированной аксиоматической системы, способной доказать все эти осмысленные истины. Это вроде как очевидно — программа, выводящая из аксиом, не может слишком много доказать о себе без противоречия.
Но что более важно, он показывает вам, как создавать более сильные системы — присоединяя аксиому «S непротиворечиво», вы получаете новую систему, которая делает систему сильнее. Это означает, что у любой системы аксиом есть более сильная система — гёделевское отражение.
S + «S непротиворечиво»
строго сильнее S.
Вы можете повторять эту процедуру, повторяя отражение Гёделя. На бесконечности барьера нет --- можно рассматривать систему, являющуюся бесконечным геделевским отражением, как объединение всех теорем, доказанных на n-м этапе (есть специальная программа, которая распечатает выводы--- вам не нужна теория множеств, чтобы сделать итерацию точной, по крайней мере, не для достаточно малых бесконечных порядковых номеров). Процесс итерации гёделевского отражения воспроизводит канторовские ординалы.
Это отвечает на вопрос математической философии
Зачем нужны ординалы?
Это полностью оправдывает теорию множеств Кантора. Теория множеств Кантора требуется, чтобы дать Гёделю размышления о теориях, прошедших омегу. Однако это не оправдывает всю метафизику, а только порядковые числа после целых чисел.
По мере того как вы поднимаетесь вверх по списку порядковых номеров, порядковые номера становятся все более сложными компьютерными программами (каждый порядковый номер — это «процесс», по словам Пола Коэна). Традиционно вы можете определить предел всех ординалов, которые могут быть представлены на компьютере в рамках теории множеств, и это называется порядковым номером Чача-Клине. Вы можете приблизиться только к порядковому номеру Черча-Клин по сложности.
Вслед за Гёделем Генцен доказал непротиворечивость арифметики Пеано в рамках очень ограниченной аксиоматической системы (PRA --- слабый фрагмент PA) с дополнительным предположением
Порядковое эпсилон-ноль хорошо обосновано
С этого момента стало ясно, что доказательства непротиворечивости сложных теорий могут быть получены из простых теорий при единственном сложном допущении обоснованности некоторого счетно-вычислимого ординала. Для PA порядковый номер был не так уж и сложен, так что есть вопросы (например, проблема Пэрис-Харрингтона, или проблема гидры, или теорема Гудштейна), которые эквивалентны обоснованности эпсилон-ноль, и, таким образом, не могут быть доказаны в рамках PA, но которые эквивалентны непротиворечивости PA, поэтому они доказуемы в любой теории, которая может доказать непротиворечивость PA.
Предмет теории порядкового доказательства пытается сопоставить порядковый номер, как можно более точно описываемый, с каждой математической теорией. Эта программа имеет успех с некоторыми теориями множеств, и нет никаких препятствий для доказательства непротиворечивости любой теории, какой бы бесконечной она ни была. Итак, еще один смысл
Можно завершить программу Гильберта и доказать непротиворечивость несчетно бесконечных математических систем, только используя счетные вычислимые ординалы, которые могут быть представлены на компьютере.
Эта программа действует и сегодня, но она еще не доказала состоятельность ZF. Отчасти это потому, что многие люди продолжают говорить, что это невозможно сделать из-за теоремы Геделя.
Основное предположение в этих идеях состоит в том, что процесс создания ординалов, приближающихся к порядковому номеру Черча Клини, можно каким-то образом понять, хотя его нельзя формализовать в виде компьютерной программы. Этот процесс усложняется по аналогии с биологической эволюцией, и непонятно, как далеко мы можем зайти в рамках наших человеческих ограничений.
Есть много ложных следствий теоремы Геделя.
Мы больше, чем компьютеры
Эта интерпретация исходит из того факта, что мы можем понять, что программа P не останавливается (а именно SPITE для данной формальной системы), даже если формальная система не может. Чтобы увидеть, что это ложный вывод, вам просто нужно посмотреть, что делает SPITE: он моделирует систему, ищет предсказание и назло ему! Нет причин, по которым вы не можете сделать это с человеком:
Если вы можете симулировать человека, вы можете предсказать его выбор и вопреки его решению --- так что вы сможете положить миллион долларов в коробку А только в том случае, если человек выберет коробку Б.
Это точный аналог теоремы Геделя в человеческом мире, и это известная философская проблема. Есть также заявления
Джон Серл не может последовательно верить этому утверждению.
которые в точности аналогичны, и Джон Серл не может поверить, хотя это правда. Хотя, чтобы сделать это логическим утверждением первого порядка об арифметике, вы должны дать вычислительную модель убеждений Серла, что может быть невозможно из-за случайности. Но идея та же самая: то, что система аксиом не может знать, но мы можем знать, относится к самой системе.
Есть и другие конструкции, принадлежащие Чайтину, которые перефразируют теорему о неполноте следующим образом.
Никакая программа не может доказать, что колмогоровская сложность любой строки больше, чем длина программы плюс фиксированная константа.
Но с вычислительной точки зрения это просто означает, что ни один человек не может доказать, что колмогоровская сложность строки больше, чем сложность программы, моделирующей этого человека. Поскольку у нас такое тяжелое время даже с небольшой колмогоровской сложностью, это безопасный прогноз.
Таким образом, из теоремы Геделя нет никаких следствий, которые подразумевают, что вычислительная теория разума ложна. Есть другие идеи
Теорема Геделя говорит, что семантика не формализуема
Это тоже не совсем верно — теорема Геделя утверждает, что семантика остановки компьютерных программ только приблизительно аксиоматизируется усилением систем, а процесс усиления неалгоритмичен на верхнем уровне. Но точная природа неалгоритмичности может заключаться в простом названии все более крупных вычислимых счетных ординалов, которые приближаются к порядковому номеру Черча Клини, и это может быть разумным образом возможно с точки зрения эволюции.
Теорема Годе убивает программу Гильберта
поскольку программа Гильберта разработала порядковый анализ в ответ на теорему Геделя, это неверно. Это делает наивную реализацию программы Гильберта невозможной, но точка зрения порядкового анализа вовсе не наивна, и это именно те основания, которые можно ожидать от математики, которая бесконечно богата и бесконечно сложна.
Я думаю, что это также имеет некоторые последствия для философии математики, в частности, для радикального формалистического взгляда, который рассматривает математику как простую формальную игру без какого-либо реального смысла. У этой точки зрения есть проблема с результатом Геделя: теорема действительно показывает, что мы можем делать математические выводы вне любых возможных фиксированных (и достаточно строгих) формальных условий, поэтому, если математика просто «играет с формальными правилами», неясно, как идентифицировать эти правила любым разумным способом, поскольку любой возможный набор правил, который вы можете предоставить, оказывается необоснованно слабым по результату Гёделя.
Никакое измерение изнутри наблюдаемой системы не может быть информационно полным.
пользователь 21820