Про Гёделя и Пенроуза (2)
Второй, но не последний пост на эту тему (чего-то зацепила).
В комментариях к предыдущему посту об этом родилась краткая и более изящная версия доказательства неалгоритмизуемости сознания, основанная на том же принципе, что у Пенроуза.
Из теоремы о неполноте следует, что в любой непротиворечивой системе аксиом существуют алгоритмы, о которых невозможно доказать ни то, что они остановятся, ни то, что они не остановятся [*].
А в сознании Пенроуза таких алгоритмов не существует, т.к. если невозможно доказать, что алгоритм остановится, то это является доказательством того, что он не остановится. Потому что если бы он на каком-то шаге остановился, то пошаговое прохождение до этого шага являлось бы доказательством остановки.
Значит, никакая формальная система (и, соответственно, никакой формальный алгоритм) не может соответствовать сознанию Пенроуза.
Это формулировка без самореференции, парадокса лжеца, диагонального метода и всего прочего. Точнее, всё это тут скрыто за ссылкой на теорему о неполноте.
Поговорю об этом немного подробнее, это интересно.
В реальном мире нет таких объектов, как "число", "точка", "прямая" и прочих математических понятий. Это абстрактные идеи.
Но идеи у каждого свои, и на идеях науку не построить. Один учёный считает, что теорема доказана, другому доказательство не нравится - как узнать, кто прав? Должны быть какие-то формальные критерии проверки. Для физики это эксперимент, а для математики?
Тогда математики придумали, что для этих абстрактных объектов можно сформулировать некоторые базовые свойства, которые ни у кого не вызывают сомнений, назвать их аксиомами, и с помощью формальной логики строить из них всякие следствия-теоремы и решать задачи.
При изучении математики иногда упускается очень важный аспект (я, например, его упустил в своём образовании): математики изучают не следствия из аксиом, а исследуют свойства математических объектов, которые существуют в виде "идей", в неких платоновских мирах, а аксиомы используют лишь для формализации своих рассуждений и доказательств. Примерно как слова используются для передачи идей другим людям, но сами идеи - это не набор слов.
Если какое-то свойство математических объектов не следует из аксиом - это проблема выбранной системы аксиом.
Понятно, почему об этом не говорят прямо: тут отдаёт чем-то ненаучным.
В примитивных случаях возможна формализация доказательства, сведение его к аксиомам и формальная проверка (для чего, собственно, оно и было придумано). В реальных современных математических доказательствах об этом речь не идёт, математики оперируют исключительно абстрактными математическими объектами, представления о которых у них неплохо синхронизированы, и доказательство признаётся корректным, когда оно понятно и принято другими математиками, а не когда оно формально сведено к аксиомам. Никому не приходит в голову автоматическая проверка доказательства, скажем, великой теоремы Ферма или гипотезы Пуанкаре.
Думаю, что это обычно упускается из виду, потому что для одних людей очевидно, что математика оперирует абстрактными объектами, а аксиомы описывают некоторые их свойства, а для других - что математика оперирует формальными утверждениями и строит теоремы на основании аксиом и формальной логики. Каждый из этих подходов оправдан, примерно как материализм и идеализм, но при этом они не противоречат друг другу, и поэтому их редко сравнивают и противопоставляют, а чаще говорят про аксиомы, но подразумевают математические объекты. При изучении математики "понял" - это "увидел" математический объект, который стоит за формальной записью. Например, один ученик заучил определение, что вектор это направленный отрезок (или что это набор чисел), а второй понял, что такое вектор, и ему уже необязательно учить формулу для суммы векторов, он может её сам "придумать".
Теорему Гёделя о неполноте я воспринимал просто как любопытное утверждение о том, что в любой аксиоматической системе (непротиворечивой и включающей аксиомы арифметики) существуют утверждения, которые нельзя ни доказать, ни опровергнуть. То есть, для которых ни само утверждение, ни отрицание утверждения не следуют из аксиом. Факт любопытный, но - ну и что?
На самом деле суть этой теоремы Гёделя в том, что выбранный способ формализации математических сущностей принципиально неполон, всегда найдутся какие-то свойства этих объектов, для которых выбранных аксиом недостаточно. Иными словами, для полного описания математических объектов (например, объекта "число") необходимо бесконечное количество аксиом! Математик, тем не менее, вполне успешно продолжает оперировать этими объектами и изучать их свойства, а вот компьютеру доступны лишь конечные аксиоматические системы, которые могут описывать эти объекты достаточно хорошо, но принципиально не полностью.
Гёдель сказал (доказал!), что машина не может изучать математику наравне с человеком, потому что ей принципиально недоступны платоновские миры, изучением которых занимаются математики, понимаете?
После этого гёделевское доказательство существования бога (онтологический аргумент) уже не выглядит таким уж странным.
Например, для натуральных чисел используется некий набор аксиом, обычно это аксиоматика Пеано. Её достаточно для практически всех утверждений. Тем не менее, существуют утверждения, о которых уже известно (доказано), что в аксиоматике Пеано их доказать невозможно, и опровергнуть тоже невозможно. Это не значит, что можно выбрать произвольный ответ - нет, для абстрактного объекта "число" ответ вполне определённый.
Есть нерешённые задачи - например, гипотеза Гольдбаха (о том, что любое чётное число, больше двух, представляется в виде суммы двух простых). В принципе может оказаться, что ответ на это утверждение не следует из аксиом Пеано (хотя и вряд ли), но если так случится, это не будет значить, что ответа (или решения или доказательства) нет. Напротив - это будет означать, что гипотеза верна, ведь если бы существовало неразложимое число, то оно было бы доказательством неверности этой гипотезы в аксиоматике Пеано. Поэтому конкретный набор аксиом для математиков не очень важен - важнее свойства объектов (в данном случае чисел).
Когда было доказано, что не существует алгоритма для решения диофантовых уравнений (10-я проблема Гильберта) - это не просто означало существование диофантова уравнения, неразрешимого в аксиоматике Пеано. Нет, это означало, что для любой системы аксиом найдётся уравнение, для которого невозможно ни найти решение, ни доказать его отсутствие. Под фразой "не существует алгоритма" скрывается не "не существует способа найти решение", как можно было бы подумать - нет, это значит, что не существует формального решения. Ведь если бы существовало либо решение, либо доказательство его отсутствия, то переборный алгоритм его нашёл бы. Но и сказать "не существует ни решения, ни доказательства его отсутствия" тоже плохо, ведь для математиков невозможность найти решение является доказательством его отсутствия. Является доказательством для математиков, хотя не является формальным доказательством. Не, такого они вслух говорить не будут, поэтому говорят "не существует алгоритма". :)
Что интересно, Пенроуз в своей книге довольно много внимания уделил вопросу о том, придумываем ли мы математику или открываем, т.е. о противопоставлении этих подходов, на чём и основан его аргумент неалгоритмизуемости сознания. Но и он всё-таки не формулирует этого в явном виде, а строит формальное доказательство гёделевским методом.
И ещё интересно, что этот критический для математики факт (по сути - доказательство невозможности строгой формализации математики как науки, т.к. для любой системы аксиом найдутся утверждения, которые осмысленны и определены для математиков, но не определены в аксиоматике) по времени примерно совпал с не менее критическим фактом для физики - обнаружением квантовой неопределённости, которая по сути означает принципиальную невоспроизводимость экспериментов и, соответственно, невозможность предсказания состояния системы с помощью физической теории, а ведь именно это считалось основной задачей физики и критерием научности физических теорий. И то, и другое произошло в начале XX века.
[*] Задача останова говорит о том, что не существует алгоритма, который про произвольный поданный ему на вход алгоритм определял бы, остановится он или нет (это нетрудно доказывается). Значит, алгоритм, который последовательно перебирает все возможные фразы в поисках формального доказательства либо того, что данный ему на вход алгоритм не остановится, либо что он остановится, тоже для каких-то алгоритмов никогда не даст ответ, а значит, для этих алгоритмов не существует ни доказательства того, что они остановятся, ни - того, что они не остановятся.
This entry was originally posted at https://gul-kiev.dreamwidth.org/70091.html.
В комментариях к предыдущему посту об этом родилась краткая и более изящная версия доказательства неалгоритмизуемости сознания, основанная на том же принципе, что у Пенроуза.
Из теоремы о неполноте следует, что в любой непротиворечивой системе аксиом существуют алгоритмы, о которых невозможно доказать ни то, что они остановятся, ни то, что они не остановятся [*].
А в сознании Пенроуза таких алгоритмов не существует, т.к. если невозможно доказать, что алгоритм остановится, то это является доказательством того, что он не остановится. Потому что если бы он на каком-то шаге остановился, то пошаговое прохождение до этого шага являлось бы доказательством остановки.
Значит, никакая формальная система (и, соответственно, никакой формальный алгоритм) не может соответствовать сознанию Пенроуза.
Это формулировка без самореференции, парадокса лжеца, диагонального метода и всего прочего. Точнее, всё это тут скрыто за ссылкой на теорему о неполноте.
Поговорю об этом немного подробнее, это интересно.
В реальном мире нет таких объектов, как "число", "точка", "прямая" и прочих математических понятий. Это абстрактные идеи.
Но идеи у каждого свои, и на идеях науку не построить. Один учёный считает, что теорема доказана, другому доказательство не нравится - как узнать, кто прав? Должны быть какие-то формальные критерии проверки. Для физики это эксперимент, а для математики?
Тогда математики придумали, что для этих абстрактных объектов можно сформулировать некоторые базовые свойства, которые ни у кого не вызывают сомнений, назвать их аксиомами, и с помощью формальной логики строить из них всякие следствия-теоремы и решать задачи.
При изучении математики иногда упускается очень важный аспект (я, например, его упустил в своём образовании): математики изучают не следствия из аксиом, а исследуют свойства математических объектов, которые существуют в виде "идей", в неких платоновских мирах, а аксиомы используют лишь для формализации своих рассуждений и доказательств. Примерно как слова используются для передачи идей другим людям, но сами идеи - это не набор слов.
Если какое-то свойство математических объектов не следует из аксиом - это проблема выбранной системы аксиом.
Понятно, почему об этом не говорят прямо: тут отдаёт чем-то ненаучным.
В примитивных случаях возможна формализация доказательства, сведение его к аксиомам и формальная проверка (для чего, собственно, оно и было придумано). В реальных современных математических доказательствах об этом речь не идёт, математики оперируют исключительно абстрактными математическими объектами, представления о которых у них неплохо синхронизированы, и доказательство признаётся корректным, когда оно понятно и принято другими математиками, а не когда оно формально сведено к аксиомам. Никому не приходит в голову автоматическая проверка доказательства, скажем, великой теоремы Ферма или гипотезы Пуанкаре.
Думаю, что это обычно упускается из виду, потому что для одних людей очевидно, что математика оперирует абстрактными объектами, а аксиомы описывают некоторые их свойства, а для других - что математика оперирует формальными утверждениями и строит теоремы на основании аксиом и формальной логики. Каждый из этих подходов оправдан, примерно как материализм и идеализм, но при этом они не противоречат друг другу, и поэтому их редко сравнивают и противопоставляют, а чаще говорят про аксиомы, но подразумевают математические объекты. При изучении математики "понял" - это "увидел" математический объект, который стоит за формальной записью. Например, один ученик заучил определение, что вектор это направленный отрезок (или что это набор чисел), а второй понял, что такое вектор, и ему уже необязательно учить формулу для суммы векторов, он может её сам "придумать".
Теорему Гёделя о неполноте я воспринимал просто как любопытное утверждение о том, что в любой аксиоматической системе (непротиворечивой и включающей аксиомы арифметики) существуют утверждения, которые нельзя ни доказать, ни опровергнуть. То есть, для которых ни само утверждение, ни отрицание утверждения не следуют из аксиом. Факт любопытный, но - ну и что?
На самом деле суть этой теоремы Гёделя в том, что выбранный способ формализации математических сущностей принципиально неполон, всегда найдутся какие-то свойства этих объектов, для которых выбранных аксиом недостаточно. Иными словами, для полного описания математических объектов (например, объекта "число") необходимо бесконечное количество аксиом! Математик, тем не менее, вполне успешно продолжает оперировать этими объектами и изучать их свойства, а вот компьютеру доступны лишь конечные аксиоматические системы, которые могут описывать эти объекты достаточно хорошо, но принципиально не полностью.
Гёдель сказал (доказал!), что машина не может изучать математику наравне с человеком, потому что ей принципиально недоступны платоновские миры, изучением которых занимаются математики, понимаете?
После этого гёделевское доказательство существования бога (онтологический аргумент) уже не выглядит таким уж странным.
Например, для натуральных чисел используется некий набор аксиом, обычно это аксиоматика Пеано. Её достаточно для практически всех утверждений. Тем не менее, существуют утверждения, о которых уже известно (доказано), что в аксиоматике Пеано их доказать невозможно, и опровергнуть тоже невозможно. Это не значит, что можно выбрать произвольный ответ - нет, для абстрактного объекта "число" ответ вполне определённый.
Есть нерешённые задачи - например, гипотеза Гольдбаха (о том, что любое чётное число, больше двух, представляется в виде суммы двух простых). В принципе может оказаться, что ответ на это утверждение не следует из аксиом Пеано (хотя и вряд ли), но если так случится, это не будет значить, что ответа (или решения или доказательства) нет. Напротив - это будет означать, что гипотеза верна, ведь если бы существовало неразложимое число, то оно было бы доказательством неверности этой гипотезы в аксиоматике Пеано. Поэтому конкретный набор аксиом для математиков не очень важен - важнее свойства объектов (в данном случае чисел).
Когда было доказано, что не существует алгоритма для решения диофантовых уравнений (10-я проблема Гильберта) - это не просто означало существование диофантова уравнения, неразрешимого в аксиоматике Пеано. Нет, это означало, что для любой системы аксиом найдётся уравнение, для которого невозможно ни найти решение, ни доказать его отсутствие. Под фразой "не существует алгоритма" скрывается не "не существует способа найти решение", как можно было бы подумать - нет, это значит, что не существует формального решения. Ведь если бы существовало либо решение, либо доказательство его отсутствия, то переборный алгоритм его нашёл бы. Но и сказать "не существует ни решения, ни доказательства его отсутствия" тоже плохо, ведь для математиков невозможность найти решение является доказательством его отсутствия. Является доказательством для математиков, хотя не является формальным доказательством. Не, такого они вслух говорить не будут, поэтому говорят "не существует алгоритма". :)
Что интересно, Пенроуз в своей книге довольно много внимания уделил вопросу о том, придумываем ли мы математику или открываем, т.е. о противопоставлении этих подходов, на чём и основан его аргумент неалгоритмизуемости сознания. Но и он всё-таки не формулирует этого в явном виде, а строит формальное доказательство гёделевским методом.
И ещё интересно, что этот критический для математики факт (по сути - доказательство невозможности строгой формализации математики как науки, т.к. для любой системы аксиом найдутся утверждения, которые осмысленны и определены для математиков, но не определены в аксиоматике) по времени примерно совпал с не менее критическим фактом для физики - обнаружением квантовой неопределённости, которая по сути означает принципиальную невоспроизводимость экспериментов и, соответственно, невозможность предсказания состояния системы с помощью физической теории, а ведь именно это считалось основной задачей физики и критерием научности физических теорий. И то, и другое произошло в начале XX века.
[*] Задача останова говорит о том, что не существует алгоритма, который про произвольный поданный ему на вход алгоритм определял бы, остановится он или нет (это нетрудно доказывается). Значит, алгоритм, который последовательно перебирает все возможные фразы в поисках формального доказательства либо того, что данный ему на вход алгоритм не остановится, либо что он остановится, тоже для каких-то алгоритмов никогда не даст ответ, а значит, для этих алгоритмов не существует ни доказательства того, что они остановятся, ни - того, что они не остановятся.
This entry was originally posted at https://gul-kiev.dreamwidth.org/70091.html.