Дениэль Деннет "Опасная идея Дарвина"

[sergey zhukov]

В книжке Деннета есть такой абзац:

Цитата:

Итак, вот что говорит нам Гёдель, которого Тьюринг приковал к миру компьютеров: у каждого компьютера, являющегося внутренне непротиворечивым механизмом доказательства арифметических истин, есть ахиллесова пята, истина, которую он никогда не сможет доказать, даже если будет работать до Судного дня. Ну и что с того?

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

Почему Гёдель так считал? Разве какие-то математики могут непосредственно видеть истинность недоказуемых высказываний? Были такие примеры? И как они вообще могут быть сконструированы, эти примеры? Недостаточно же просто сказать "Я думаю, это истинно"?

[Mikhail_K]

sergey zhukov в сообщении #1714338 писал(а):

Разве какие-то математики могут непосредственно видеть истинность недоказуемых высказываний? Были такие примеры? И как они вообще могут быть сконструированы, эти примеры? Недостаточно же просто сказать "Я думаю, это истинно"?

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

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

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

[sergey zhukov]

Mikhail_K
Получается, что мы можем сконструировать пример истинного и недоказуемого (внутри данной системы аксиом) утверждения. Это, видимо, не так уж и сложно. Ок.

Но мы не можем про любое данное произвольное утверждение сказать, какое оно? Часто можно услышать про какую-нибудь сложную математическую задачу "А не пример ли это того самого утверждения, которое недоказуемо?". И здесь никакого преимущества людей перед компьютером не видно. Люди тоже могут до Судного дня ковырять какую-нибудь гипотезу Коллатца так и не узнав, что она недоказуема (например). Или нет?

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

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

[mihaild]

Mikhail_K в сообщении #1714340 писал(а):

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

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

sergey zhukov в сообщении #1714342 писал(а):

Получается, что мы можем сконструировать пример истинного и недоказуемого (внутри данной системы аксиом) утверждения

Мы можем сконструировать пример утверждения, недоказуемого и неопровержимого в данной теории. Соответственно в некоторых моделях теории оно истинно, а в некоторых ложно. Говорить, что оно просто "истинно" нельзя (потому что его отрицание точно так же недоказуемо и неопровержимо, и как-то странно говорить, что одновременно истинно и утверждение, и его отрицание).

sergey zhukov в сообщении #1714342 писал(а):

Люди тоже могут до Судного дня ковырять какую-нибудь гипотезу Коллатца так и не узнав, что она недоказуема (например). Или нет?

Да, вполне может оказаться, что это так.

sergey zhukov в сообщении #1714342 писал(а):

Т.е. можно сказать, что Гёдель видел преимущество человека

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

[Mikhail_K]

sergey zhukov в сообщении #1714342 писал(а):

Но мы не можем про любое данное произвольное утверждение сказать, какое оно?

sergey zhukov в сообщении #1714342 писал(а):

Люди тоже могут до Судного дня ковырять какую-нибудь гипотезу Коллатца так и не узнав, что она недоказуема (например).

Разумеется.

sergey zhukov в сообщении #1714342 писал(а):

Т.е. можно сказать, что Гёдель видел преимущество человека в том, что он может в принципе понять неполноту, и ограниченность теории (и даже доказать эту неполноту и ограниченность) и подняться до метатеории?

Что-то вроде того. Такие мысли ещё Пенроуз активно продвигал. Но убедительности тут не хватает.
Гёдель, к слову, ещё автор одного из "доказательств" бытия Божия.

mihaild в сообщении #1714344 писал(а):

Мы можем сконструировать пример утверждения, недоказуемого и неопровержимого в данной теории. Соответственно в некоторых моделях теории оно истинно, а в некоторых ложно. Говорить, что оно просто "истинно" нельзя

В некотором определённом смысле так говорить всё-таки можно. Например, если мы верим в истинность аксиом ZFC, то должны бы верить и в ConZFC и всё, что выводится из ZFC+ConZFC - несмотря на то, что получаемые утверждения в некоторых моделях ZFC будут ложными.

[mihaild]

Mikhail_K в сообщении #1714345 писал(а):

Например, если мы верим в истинность аксиом ZFC, то должны бы верить и в ConZFC

А чем тут ConZFC лучше $\neg \text{ConZFC}$? Почему бы не поверить во второе вместо первого?
Множества странные, мало ли что они там вместо строк закодировать могут...

[Anton_Peplov]

sergey zhukov
Я не знаю, что считал Гедель, и буду говорить на современном языке, а не на том, на котором Гедель доказал свою теорему о неполноте. Не знаю, насколько Вы в теме, поэтому извините, если проговариваю банальности.

Теорема Геделя о неполноте применима только к формальным теориям. Что это такое? Формальная теория строится в четыре шага.

1. Определяем алфавит (обычно в него входят латинские буквы, цифры, скобки, логические символы и т.д.). Просто перечисляем символы. Их конечное и обычно небольшое число.
2. Определяем, какие наборы символов являются высказываниями (например, $\forall x \ x > 5 \Rightarrow x > 2$ является высказыванием, а $((8+$ - нет).
Пункты 1-2 называются "определим язык".
3. Определяем, какие высказывания мы принимаем за аксиомы.
4. Определяем, какие конечные цепочки высказываний являются доказательством последнего высказывания в цепочке.
Пункт 4 называется "определяем правила вывода".

Пункты 1-4 вместе называются "определяем формальную теорию". Важно, что пп. 1-4 формулируются предельно конкретно, формально, механически. Так, чтобы не оставалось никакой двусмысленности и свободы толкования. Так, чтобы можно было буквально компьютерной программой, написанной школьником, проверить, является ли данный набор символов высказыванием, данное высказывание аксиомой и данная цепочка высказываний - доказательством.

Теорема Геделя о неполноте утверждает, что в любой непротиворечивой теории с достаточно богатым языком (уже язык арифметики Пеано достаточно богат) найдутся высказывания, для которых в этой теории не будет ни доказательств, ни опровержений (доказательств их отрицания). То есть сказать на языке теории мы можем больше, чем доказать или опровергнуть по ее правилам вывода. Пример: в арифметике Пеано недоказуема и неопровержима теорема Гудстейна.
Можно взять другую теорию, в которой теорема Гудстейна доказуема. Но, согласно теореме Геделя, в этой теории найдутся собственные недоказуемые и неопровержимые утверждения.

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

Поэтому неудивительно, что человек может доказывать теоремы, недоказуемые и неопровержимые, например, в арифметике Пеано. В этом смысле человек может быть "умнее" какой-то конкретной формальной теории.

С другой стороны, нельзя сказать, что он "умнее" всех формальных теорий вообще. Чтобы объяснить, почему так, нам понадобится понятие "алгоритм". Алгоритм - это компьютерная программа для компьютера с неограниченной (в общем случае) памятью. Есть несколько равносильных формализмов, позволяющих в принципе записать любой алгоритм. Наиболее известный из них - машина Тьюринга.

Какая связь с формальными теориями? Тривиально строится алгоритм, который для любого высказывания $X$ ищет его доказательство или же опровержение. Просто перебирает все возможные цепочки высказываний в алфавитном порядке, пока не наткнется либо на доказательство утверждения $X$, либо на доказательство утверждения $\neg X$. Ясно, что если в данной теории вообще существует доказательство высказывания $X$ или же его отрицания, то алгоритм рано или поздно их найдёт и остановится. Правда, при попытке сделать это на реальном, а не воображаемом, компьютере ему может понадобиться столько времени, что звезды погаснут. Полный перебор такой полный. Поэтому с практической точки зрения такой алгоритм интереса не представляет. Но с принципиальной точки зрения важно, что он есть.

В обратную сторону это тоже работает. Если (как гласит авторитетная гипотеза) мышление вообще и поиск любого математического доказательства в частности представляет собой выполнение алгоритма, то этот алгоритм можно представить в виде некоторой формальной теории. И к ней, естественно, применима теорема Геделя о неполноте. Хотя, конечно, мы никогда не сможем в явном виде выписать ее язык, аксиомы и правила вывода. У нас буквально не хватит на это мозгов. У эволюции не было задачи создать мозг таким, чтобы он мог понять алгоритм собственного мышления.

Гипотеза о том, что мышление не вполне алгоритмируемо, скажем так, менее авторитетна. Хотя ее любит Пенроуз и некоторые философы и философствующие.

Кстати, даже сама теорема Геделя о неполноте сегодня доказывается на языке теории алгоритмов. И критерий "достаточно богатого языка" формулируется в ней же.

(Как?)

Anton_Peplov в сообщении #1297668 писал(а):

В максимальной (видимо) общности теорема Гёделя о неполноте сформулирована Клини в 1943 г.

Если на языке формальной системы для любого натурального числа $n$ можно выразить утверждение "универсальный алгоритм остановится, получив на вход число $n$", то такая система либо противоречива, либо неполна. Поскольку, будь она полна, алгоритм, для каждого $n$ перебирающий все доказательства подряд, пока одно из них не окажется доказательством утверждения "универсальный алгоритм остановится, получив на вход число $n$" или его отрицания, всегда останавливался бы, и тем самым, если система непротиворечива, решал проблему останова. Но известно, что проблема останова алгоритмически неразрешима.

Я набросал все очень кратко и схематично. С деталями можно ознакомиться по учебникам математической логики и теории алгоритмов. Например, по учебнику Клини или Верещагина, Шеня.

(Оффтоп)

Да что ж такое, опять пришел в "Свободный полет". Обещал же не ходить. Надеюсь, хотя бы не без пользы.

[sergey zhukov]

Anton_Peplov в сообщении #1714348 писал(а):

У эволюции не было задачи создать мозг таким, чтобы он мог понять алгоритм собственного мышления.

Я думаю, что иногда для людей невозможность представить что-то является "доказательством" несуществования этого.

Скажем, я думаю, что одной из главных причин веры в бессмертие души является просто то, что мы не можем представить себе, что значит "для меня все закончится". Аналогично, невозможность представить себе какие-то границы в нашем мышлении наталкивают на мысль, что их не должно быть (в отличии от компьютерных алгоритмов, для каждого конкретного вида которых мы такие ограничения представить можем).

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

Само это убеждение сильнее любых теорем. Оно и есть, видимо, причина, по которой, например, Пенроуз, утверждает, что математик может видеть то, что машине недоступно. Если под этим понимать это самое иррациональное чувство уверенности в чем-либо (которое у людей точно есть), то он может и прав: у компьютера этого нет. Но является ли это преимуществом людей?

[Anton_Peplov]

sergey zhukov в сообщении #1714350 писал(а):

Аналогично, невозможность представить себе какие-то границы в нашем мышлении наталкивают на мысль, что их не должно быть (в отличии от компьютерных алгоритмов, для каждого конкретного вида которых мы такие ограничения представить можем).

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

sergey zhukov в сообщении #1714350 писал(а):

это данная теорема скорее появилась в попытке доказать это наше иррациональное убеждение

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

В начале XX века разгорелась жаркая дискуссия об основаниях математики, о строгости рассуждений, о допустимых методах доказательства и опасности незамеченных противоречий. В ней приняли участие многие выдающиеся математики. Конструктивизм, интуиционизм и прочие измы - это оттуда. Наиболее продуктивным оказался подход Гильберта, придумавшего те самые формальные теории. Программа Гильберта заключалась в том, чтобы изложить все разделы математики в виде формальных систем, а затем доказать их полноту и непротиворечивость. (Полнота означает, что всякое утверждение, которое можно записать на языке теории, либо доказуемо, либо опровержимо в этой теории). Достаточно быстро была доказана полнота и непротиворечивость исчисления высказываний. Полноту исчисления предикатов доказал тот же Гедель в 1930 г. В том же году он доказал и неполноту формальной арифметики. А позже другие математики (в частности, Клини) обобщили теорему о неполноте до современного вида.

Но, еще раз, это предположение. Никаких писем, дневников или мемуаров по этому поводу я не читал.

Что до алгоритмов, то в 1930 г., когда Гедель доказал свою теорему о неполноте, это понятие еще только зарождалось. Идеи о "чисто механических процедурах" бродили в умах, свидетельством чему те самые формальные системы Гильберта. Но ни машина Тьюринга, ни другой общеизвестных формализм для алгоритмов еще не были придуманы. А уж о мыслящих машинах рассуждали только самые смелые мечтатели. Первый работающий программируемый компьютер был построен только в 1938 г. (Конрадом Цузе).

[talash]

Меня мучает один вопрос про формализацию. Гильберт издал труд по формализации геометрии. По идее с появлением компьютеров должны были появиться и программы, умеющие доказывать или опровергать любые геометрические утверждения. Но что-то я про такое не слышал, как человеки решали геометрические задачки, так и решают. Современные ИИ не в счёт. Почему так получилось? Что-то не доформализовал Гильберт?

[Anton_Peplov]

talash в сообщении #1714392 писал(а):

По идее с появлением компьютеров должны были появиться и программы, умеющие доказывать или опровергать любые геометрические утверждения.

Нет, не должны были. Формализация гарантирует существование алгоритма, который для любого доказуемого утверждения $X$ найдет его доказательство, но не гарантирует, что хотя бы один из таких алгоритмов выполнится на реальном компьютере за разумное время. Я уже писал выше:

Anton_Peplov в сообщении #1714348 писал(а):

Тривиально строится алгоритм, который для любого высказывания $X$ ищет его доказательство или же опровержение. Просто перебирает все возможные цепочки высказываний в алфавитном порядке, пока не наткнется либо на доказательство утверждения $X$, либо на доказательство утверждения $\neg X$. Ясно, что если в данной теории вообще существует доказательство высказывания $X$ или же его отрицания, то алгоритм рано или поздно их найдёт и остановится. Правда, при попытке сделать это на реальном, а не воображаемом, компьютере ему может понадобиться столько времени, что звезды погаснут. Полный перебор такой полный. Поэтому с практической точки зрения такой алгоритм интереса не представляет.

Поэтому формализацию обычно используют не для поиска доказательств, а для их проверки (для этого нужно перевести готовое доказательство с человеческого на формальный).

Кроме того, для формальной евклидовой геометрии справедлива теорема Геделя о неполноте. Так что в ней найдутся недоказуемые и неопровержимые утверждения, на которых алгоритм зациклится.

[mihaild]

talash в сообщении #1714392 писал(а):

Почему так получилось?

Потому что задача проверки истинности геометрических утверждений EXPTIME-трудна. Т.е. не существует алгоритма, который по геометрическому утверждению длины $x$ говорит, доказуемо ли оно, и работает, например, не больше чем $2^{\sqrt x}$ шагов.
Более того, хотя трудность доказана только в EXPTIME, лучший из известных алгоритмов требует $2^{2^x}$ шагов. Что становится неподъемным уже для очень коротких утверждений.

talash в сообщении #1714392 писал(а):

Но что-то я про такое не слышал, как человеки решали геометрические задачки, так и решают

Это, впрочем, не совсем правда. Есть куча эвристических систем, и они в общем-то справляются довольно неплохо.

[epros]

sergey zhukov в сообщении #1714350 писал(а):

Я думаю, что иногда для людей невозможность представить что-то является "доказательством" несуществования этого.

А "невозможность представить" доказана? Если да, то это и есть формальное доказательство несуществования - посредством приведения к противоречию предположения о существовании. Причём это верно даже в том случае, если "невозможность представить" просто принята за аксиому.

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

sergey zhukov в сообщении #1714350 писал(а):

Само это убеждение сильнее любых теорем. Оно и есть, видимо, причина, по которой, например, Пенроуз, утверждает, что математик может видеть то, что машине недоступно. Если под этим понимать это самое иррациональное чувство уверенности в чем-либо (которое у людей точно есть), то он может и прав: у компьютера этого нет. Но является ли это преимуществом людей?

Убеждения можно считать за принятую аксиоматику. Так что их существование никоим образом не отменяет формализацию знания и возможность алгоритмического поиска доказательств. Если Пенроуз имел честь не признавать тезис Чёрча, то это могло сколько угодно приводить его к уверенности в преимуществе людей перед машинами, при этом ни в малейшей степени не давая им реальных преимуществ.

[sergey zhukov]

epros
Вот уверенность в чем-то в отсутствии реальных доказательств этого - это и есть то, что недоступно компьютеру, видимо. Сам этот факт, кажется, оспаривать не приходится (все мы знаем, что такое иррациональная уверенность). Пенроуз может быть считает, что это видение истинности без формальных доказательств ("Я просто знаю, что это так"), а кто-то считает, что это просто заблуждение ("Я уверен, что знаю, что это так").

Но кажется, что уверенность иногда стоит даже больше истины или что первая может как-то изменить вторую (и что вообще, именно уверенность то нам и нужна в первую очередь). Поскольку абсолютная истина все равно нам недоступна (а все доступное - это по большей части произвольные соглашения), а увереность - это что-то большее, чем простое "примем, что это так".

(Оффтоп)

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

-- 12.01.2026, 13:28 --

epros в сообщении #1714502 писал(а):

Ну вот, например, некоторые считают, что "невозможно представить" квадратный круг.

Понятно, что "невозможно представить" - это что-то неясное. Наличие такого ощущения вообще ничего не доказывает. Но кажется, что доказывает. Даже больше того: сама эта "невозможность" аргументом не выставляется, она как бы за скобками, но она является основной.

[mihaild]

sergey zhukov в сообщении #1714506 писал(а):

Вот уверенность в чем-то в отсутствии реальных доказательств этого - это и есть то, что недоступно компьютеру, видимо

Используется синтаксис Python

 while True:
  input()
  print("Не хочу читать, что ты там написал, но гомеопатия работает")