- •Роджер пенроуз
- •1.2. Спасут ли роботы этот безумный мир?
- •1.3. Вычисление и сознательное мышление
- •1.4. Физикализм и ментализм
- •1.5. Вычисление: нисходящие и восходящие процедуры
- •1.6. Противоречит ли точка зрения в тезису Черча—Тьюринга?
- •1.7. Хаос
- •1.8. Аналоговые вычисления
- •1.9. Невычислительные процессы
- •1.10. Завтрашний день
- •1.11. Обладают ли компьютеры правами и несут ли ответственность?
- •1.12. «Осознание», «понимание», «сознание», «интеллект»
- •1.13. Доказательство Джона Серла
- •1.14. Некоторые проблемы вычислительной модели
- •1.15. Свидетельствуют ли ограниченные возможности сегодняшнего ии в пользу ?
- •1.16. Доказательство на основании теоремы Гёделя
- •1.17. Платонизм или мистицизм?
- •1.18. Почему именно математическое понимание?
- •1.19. Какое отношение имеет теорема Гёделя к «бытовым» действиям?
- •1.20. Мысленная визуализация и виртуальная реальность
- •1.21. Является ли невычислимым математическое воображение?
- •Примечания
- •2 Геделевское доказательство
- •2.1. Теорема Гёделя и машины Тьюринга
- •2.2. Вычисления
- •2.3. Незавершающиеся вычисления
- •2.4. Как убедиться в невозможности завершить вычисление?
- •2.5. Семейства вычислений; следствие Гёделя — Тьюринга
- •2.6. Возможные формальные возражения против
- •2.7. Некоторые более глубокие математические соображения
- •2.8. Условие -непротиворечивости
- •2.9. Формальные системы и алгоритмическое доказательство
- •2.10. Возможные формальные возражения против (продолжение)
- •Примечания
- •Приложение а: геделизирующая машина тьюринга в явном виде
- •3 О невычислимости в математическом мышлении
- •3.1. Гёдель и Тьюринг
- •О психофизи(ологи)ческой проблеме
- •Р.Пенроуз. Тени ума: в поисках потерянной науки о сознании. Penrose r. Shadows of the mind: a search for the missing science of consciousness. - Oxford, 1994. - XVI, 457 p.
2.8. Условие -непротиворечивости
Наиболее известная форма теоремы Гёделя гласит, что формальная система F (достаточно обширная) не может быть одновременно полной и непротиворечивой. Это не совсем та знаменитая «теорема о неполноте», которую Гёдель первоначально представил на конференции в Кенигсберге (см. §§2.1 и 2.7), а ее несколько более сильный вариант, который был позднее получен американским логиком Дж. Баркли Россером(1936). По своей сути, первоначальный вариант теоремы Гёделя оказывается эквивалентен утверждению, что система F не может быть одновременно полной и -непротиворечивой. Условие же -непротиворечивости несколько строже, нежели условие непротиворечивости обыкновенной. Для объяснения его смысла нам потребуется ввести некоторые новые обозначения. В систему обозначений формальной системы F необходимо включить символы некоторых логических операций. Нам, в частности, потребуется символ, выражающий отрицание («не»); можно выбрать для этого символ «~». Таким образом, если Q есть некое высказывание, формулируемое в рамках F, то последовательность символов ~ Q означает «не Q». Нужен также символ, означающий «для всех [натуральных чисел]» и называемый квантор общности', он имеет вид «V». Если Р (п) есть некое высказывание, зависящее от натурального числа п (т. е. Р представляет собой так называемую пропозициональную функцию), то строка символов Vn [Р (п)] означает «для всех натуральных чисел п высказывание Р (п) справедливо». Например, если высказывание Р (п) имеет вид «число п можно выразить в виде суммы квадратов трех чисел», то запись Vn [Р (п)] означает «любое натуральное число является суммой квадратов трех чисел», — что, вообще говоря, ложно (хотя, если мы заменим «трех» на «четырех», то это же утверждение станет истинным). Такие символы можно записывать в самых различных сочетаниях; в частности, строка символов
выражает отрицание того, что высказывание Р (п) справедливо для всех натуральных чисел п.
Условие же -непротиворечивости гласит, что если высказывание можно доказать с помощью методов формальной системы F, то это еще не означает, что в рамках этой самой системы непременно доказуемы все утверждения
Р(0),Р(1),Р(2),Р(3),Р(4), ....
Отсюда следует, что если формальная система F не является -непротиворечивой, мы оказываемся в аномальной ситуации, когда для некоторого Р оказывается доказуемой истинность всех высказываний Р(0), Р(1), Р(2), Р(3), Р(4), ...; и одновременно с этим можно доказать и то, что не все эти высказывания истинны! Безусловно, ни одна заслуживающая доверия формальная система подобного безобразия допустить не может. Поэтому если система F является обоснованной, то она непременно будет и -непротиворечивой.
В дальнейшем утверждения «формальная система F является непротиворечивой» и «формальная система F является -непротиворечивой» я буду обозначать, соответственно, символами «G (F)» и «П (F)». В сущности (если полагать систему F достаточно обширной), сами утверждения (? (F) и П (F) формулируются как операции этой системы. Согласно знаменитой теореме Гёделя о неполноте, утверждение G (F) не является теоремой системы F (т. е. его нельзя доказать с помощью процедур, допустимых в рамках системы F), не является теоремой и утверждение fi (F) — если, разумеется, система F действительно непротиворечива. Несколько более строгий вариант теоремы Гёделя, сформулированный позднее Россером, гласит, что если система F непротиворечива, то утверждение ~ G (F) также не является теоремой этой системы. В оставшейся части этой главы я буду формулировать свои доводы не столько исходя из утверждения fi (F), сколько на основе более привычного нам G (F), хотя для большей части наших рассуждений в равной степени сгодится любое из них. (В некоторых наиболее явных аргументах главы 3 я буду иногда обозначать через «G(F)» конкретное утверждение «вычисление Ck (k) не завершается» (см. §2.5); надеюсь, никто не сочтет это слишком большой вольностью с моей стороны.)
В большей части предлагаемых рассуждений я не стану проводить четкую границу между непротиворечивостью и -непротиворечивостью, однако тот вариант теоремы Гёделя, что представлен в § 2.5, по сути, гласит, что если формальная система F непротиворечива, то она не может быть полной, так как не может включать в себя в качестве теоремы утверждение G(F). Здесь я всего этого демонстрировать не буду (интересующиеся же могут обратиться к [222]). Вообще говоря, для того чтобы эту форму гёделевского доказательства можно было свести к доказательству в моей формулировке, система F должна содержать в себе нечто большее, нежели просто «арифметику и обыкновенную логику». Необходимо, чтобы система F была обширной настолько, чтобы включать в себя действия любой машины Тьюринга. Иначе говоря, среди утверждений, корректно формулируемых с помощью символов системы F, должны присутствовать утверждения типа: «Такая-то машина Тьюринга, оперируя над натуральным числом п, дает на выходе натуральное число р».Более того, имеется теорема (см. [222], главы 11 и 13), согласно которой так оно само собой и получается, если, помимо обычных арифметических операций, система F содержит следующую операцию (так называемую /u-операцию, или операцию минимизации): «найти наименьшее натуральное число, обладающее таким-то арифметическим свойством». Вспомним, что в нашем первом вычислительном примере, (А), предложенная процедура действительно позволяла отыскать наименьшее число, не являющееся суммой трех квадратов. То есть, вообще говоря, право на подобные вещи за вычислительными процедурами следует сохранить. С другой стороны, именно благодаря этой их особенности мы и сталкиваемся с вычислениями, которые принципиально не завершаются, — например, вычисление (В), где мы пытаемся отыскать наименьшее число, не являющееся суммой четырех квадратов, а такого числа в природе не существует.