Почему алгоритм не может понять неполноту?

Я слышал, как многие говорят, что доказательство Гёделя показывает, что человеческий интеллект каким-то образом превосходит возможности компьютера. Только мне это когда-то очень плохо артикулировали, хотя и не из-за того, что я не пытался. Я согласен с этим выводом по другим причинам, но я просто не понимаю, каким должен быть аргумент, относящийся к доказательству Гёделя.

  • Аргумент не может заключаться в том, что Гёдель был способен фактически выполнить мельчайшие детали доказательства, в то время как компьютер не может, потому что это было доказано алгоритмически несколько раз за последние 30 лет.
  • Аргумент не может заключаться в том, что из доказательства вытекают утверждения, которые компьютер не сможет также доказать, потому что любые утверждения, вытекающие из доказательства Гёделя, будут выведены компьютерами.
  • Аргумент не может заключаться в том, что мы можем спонтанно использовать новые истинные, но недоказуемые утверждения в качестве аксиом, потому что также ничто не мешает нам принять любой набор аксиом, который нам нравится, независимо от того, истинны они или доказуемы в любой данной системе. Способность к спонтанности, хотя и интересная и, без сомнения, важная для различения человека и машины, кажется вовсе не характерной для доказательства Гёделя.
  • Аргумент не может заключаться в том, что алгоритм не мог придумать идею для попытки доказательства, потому что это также не относится к доказательству Гёделя.

Так что же это должно быть?

Редактировать: Другой способ спросить об этом может быть: каково конкретное качество очень сложного доказательства Гёделя, которое важно для понимания познания и которое нельзя продемонстрировать другим, более простым способом. Ответ может заключаться в том, что ничего нет, но так много людей настаивают на том, что в доказательстве Гёделя есть что-то особенное, имеющее отношение к познанию, что я чувствую необходимость задать этот вопрос.

Ответы (3)

Что касается теоремы Гёделя о неполноте, нам нужно сначала понять с разумной точностью, что она утверждает; см. Torkel Franzén, теорема Гёделя. Неполное руководство по ее использованию и злоупотреблению (2005):

Первая теорема о неполноте (Гёделя-Россера) . Всякая непротиворечивая формальная система S, в рамках которой может быть осуществлено некоторое количество элементарной арифметики, неполна по отношению к утверждениям элементарной арифметики: есть такие утверждения, которые нельзя ни доказать, ни опровергнуть в S.

Ключевые понятия: формальная система , непротиворечивость и «некоторое количество элементарной арифметики».

О первом:

В популярных формулировках теоремы Гёделя условие такого рода (применительно к аксиомам) [о «механизируемости рассуждений в формальной системе] иногда включается в виде оговорки о том, что аксиомы формальной системы конечное число. Это означает, что аксиому можно ("в принципе") распознать как таковую, просматривая конечную таблицу. Но это условие на самом деле не выполняется многими формальными системами, изучаемыми в логике, такими как PA и ZF Эти системы имеют бесконечное число аксиом, но проверка того, является ли конкретное предложение аксиомой, по-прежнему является механическим делом.

Насчет «некоторого количества элементарной арифметики» эту мысль можно уточнить; грубо :

Любая система, язык которой включает в себя язык элементарной арифметики, а теоремы включают некоторые основные факты о натуральных числах, несомненно, удовлетворяет условию.

Теорема доказывает, что при сделанных предположениях мы можем «эффективно» построить формулу G на языке формальной системы S (т. е. формулу, «состоящую» из чисел и операций над ними, т. е. + и х), такую что ни приведенная выше формула не доказуема в системе (т. е. не выводима с помощью обычных правил вывода из аксиом системы), ни ее отрицание не-G.

Эта «странная» формула изготовлена ​​таким образом, что ее «интерпретация» является истинным утверждением, потому что формула «говорит о себе», что она недоказуема, и она действительно недоказуема; таким образом, если система работает так, как мы хотим, формула должна быть верной.

И что ? Гёдель не «вычислил», что наши алгоритмы не в состоянии выполнить. Он сделал математическое доказательство с помощью обычной математической техники: проницательности и рассуждений.

Из его теоремы следует, что касается темы, которую мы обсуждаем, заключается в том, что способность математической логики «воспроизводить» в единую формальную систему S, работающую алгоритмически, обычные рассуждения, которые математический (т. «в единую формальную систему.

Чтобы формализовать построение доказательства Гёделя в формальную систему, мы должны построить новую (более мощную) систему S'; но тогда мы можем воспроизвести построение приведенной выше формулы, получив новую формулу G' для S', и так далее.

Можем ли мы сделать вывод о неисчерпаемости наших математических знаний? Кажется, да [см. Franzén, стр. 56].

Хорошее простое объяснение после «Ну и что?» здесь. Кажется, вокруг теорем о неполноте ходит много диких разговоров, например, о том, в чем скептически настроен Лукас, или о том, как Гёдель приведет к «постньютоновским» взглядам и тому подобному. Все, что я вижу, — это любопытство логики, которое выглядит относящимся к математике, информатике, лингвистике и т. д., но само по себе «достаточно справедливо». Да: люди должны использовать S', чтобы разобрать любопытное предложение G, и сделать. И искусственный интеллект должен быть таким же, и они делают, если вы строите их для этого? Есть ли что-то еще?
@Diploria - я полностью с вами согласен; вообще, это «опасная» задача — пытаться извлечь философские уроки из научно-технических результатов; часто мы получаем «дикие» идеи, которые являются только предположениями без научной поддержки.
Эта книга существует! Потрясающий заголовок. Я думаю, что после (Ну и что?) вам удалось сформулировать самое сильное из возможных обоснованных утверждений, которые теорема Геделя делает о человеческом интеллекте. Не думаю, что мне следует ожидать чего-то большего. Я действительно думаю, что некоторые люди хотят сказать что-то еще более сильное, но я понимаю (оглядываясь назад), что если действительно недопустимо говорить что-то более сильное, у меня мало шансов, что это будет конкретно выражено в качестве ответа.
@ Лукас - я согласен с вами: для меня книга Франзена - лучшая книга по этой теме. Является «обобщающим», стараясь быть как можно менее техническим, но в то же время полным, избегающим ошибок и упрощений.

Теорема Гёделя о неполноте часто грубо неверно истолковывается, когда обсуждаются вопросы интеллекта и искусственного интеллекта.

Его теорема утверждает, что существуют математические утверждения, которые нельзя ни доказать, ни опровергнуть. Компьютер, ищущий доказательство, не сможет его найти. Компьютер, ищущий доказательство и не сдающийся, застрянет. Но блестящий математик, ищущий доказательство, также не найдет его. И если этот математик не сдастся, он или она тоже застрянут навсегда.

Он обнаружил, что это проблемы, которые не может решить ни один компьютер. Однако эти же проблемы не под силу решить и человеку. Некоторые люди, кажется, думают, что неразрешимая проблема создаст проблемы для искусственного интеллекта. Но, конечно же, любой искусственный интеллект, достойный этого имени, был бы способен понять, что проблема сложна, слишком сложна для ее решения, и тогда, как это сделали бы люди, единственный выход — сдаться.

Вы правы, это не лучшее выражение результата Геделя. Его результат состоит в том, что не существует конечно аксиоматизируемой теории арифметики. Чтобы раскрыть некоторые (но не все, потому что распаковка всего этого заставит нас задержаться здесь на некоторое время, а у меня нет Сникерса), «теория арифметики» — это любой набор предложений, вытекающих из языка первого порядка, вместе с набор нелогических аксиом, из которых следуют в точности истинные арифметические равенства. «Конечно аксиоматизируемая» теория арифметики — это любая теория арифметики, для которой набор нелогических аксиом конечен по размеру.

Если бы мне пришлось изложить это в моем собственном выражении, максимально приближенном к естественному языку, я бы сказал: «Если бы компьютеру была дана программа, предназначенная для получения всех и только истинных арифметических равенств, всегда будет какое-то истинное равенство, которого он будет систематически упускать».

Мне нравится ваше выражение теоремы о неполноте, и я думаю, что оно правильное. Однако я пытался найти кого-нибудь, кто дал бы мне хорошую версию аргумента о том, что люди не ограничены таким образом. В такой формулировке кажется, что высказывание «если бы я написал алгоритм для перечисления всех натуральных чисел, он никогда не дал бы мне отрицательного числа» имеет точно такой же смысл.
О, этот аргумент сложнее. Но идея такова: если вы проводите доказательство, вы на самом деле строите предложение, которое не доказуемо в теории. И когда вы, как человек, посмотрите на это предложение, вы увидите, что оно верно. Как? Можете ли вы распознать (в принципе) истинность любого гёдель-предложения? Они могут быть очень длинными и сложными, если вы начнете искать другие в цепочке, но все они работают на одном и том же трюке «это предложение не доказуемо на этом языке», так что кажется, что мы можем. Если это так, то похоже, что люди не запрограммированы каким-то конечно-аксиоматизированным способом.
Но и компьютер может сделать доказательство. Хотя я мог бы посмотреть на (конструкцию) числа Гёделя и сказать: «Это выглядит правдой», это не доказывает этого. Если опыт правдивости — способность думать, что что-то истинно, не доказывая этого — это все, о чем идет речь, тогда вам не нужна теорема Геделя, это просто очевидный факт, который вы можете продемонстрировать многими другими простыми способами.
Что ж, я полагаю, суть вопроса зависит от того, согласитесь ли вы с тем, что высшим испытанием «понимания» компьютера является печать утверждений, в то время как высшим испытанием человеческого понимания является демонстрация некоторой убежденности и способности объяснять. Вы можете подумать, что это глупый набор стандартов, что это почти вызывает вопросы, но это аргумент, как я его понимаю. (Не одобряя.)
Я думаю, вы можете быть правы в том, что это аргумент. Поместите так, как вы это сделали, это почти не вызывает вопросов.