Amigo писал(а):
Это, на мой взгляд, и есть то центральное место теоремы Гёделя, которое нужно всем, кто хочет добиться её понимания - чётко знать.
Можно даже сказать так - "Сказать - "я понимаю т. Гёделя" - равносильно тому, что бы сказать -"я понимаю каким образом доказывается существование предиката, аналогичного по сути выражению в рамке". Всё остальное - ничто.
Я не согласен с этим утверждением. Это то же самое, что сказать "понимать теорию алгоритмов - это понимать, как пишется программа, распечатывающая свой собственный текст". Подход на основе таких вот конструкций, говорящих что-то о самих себе, мне кажется совершенно ненаглядным.
Взамен я приведу пример конструкции, которая в своё время произвела на меня сильное впечатление, и с помощью которой можно доказать вариант теоремы Гёделя, похожий на недоказуемость непротиворечивости, а именно: недоказуемость
-корректности.
-корректность - это следующее свойство:
для любого алгоритма из существования доказательства того, что он останавливатся следует то, что он действительно останавливается. Это есть частный случай корректности, которая утверждает, что из доказуемости следует истинность. Могу сказать, что
-корректность - это более сильное свойство, чем непротиворечивость, но более слабое, чем корректность. И это свойство можно легко формализовать на языке арифметики (для любой формальной теории).
А теперь докажем, что в теории
(на теорию, естественно, нужно наложить ряд требований, например, корректность) нельзя доказать
-корректность
. Для теории построим класс
- множество всех функций
, для которых существует вычисляющий алгоритм и доказательство в теории
, что этот алгоритм останавливается на любом входе.
обычно называют классом доказуемо рекурсивных функций для теории
.
Теперь опишем функцию
- универсальную функцию для
. Пусть в
каким-то образом кодируются пары (алгоритм,доказательство). Тогда
- функция, которую вычисляет алгоритм с номером
.
Заметим, что при любом фиксированном
функция
принадлежит
. Кроме того, любая функция из
имеет номер. И, очевидно, что
вычислима (потому что мы её описали через алгоритм).
Теперь применим Канторовскую диагональ:
, очевидно, не совпадает ни с одной из функций в
, но, тем не менее, вычислима, и вычисляющий её алгоритм останавливается на любом входе. Если нужно доказать просто неполноту теории
, то на этом можно остановиться: мы привели алгоритм, останавливающийся на любом входе, но для которого доказать это в теории
нельзя.
Но мы пойдём дальше и заметим, что если бы в теории
можно было бы доказать её
-корректность, то можно было бы доказать и то, что вычисляющий
алгоритм останавливается на любом входе (технический момент: нужно проделать это нехитрое доказательство в теории
), т.е.
, противоречие.
Примечание 1. Класс
часто используют для характеризации доказательной силы теории
: чем сильнее
, тем больше
. Но даже для самых слабых теорий (типа арифметики Пеано)
содержит практически все встречающиеся в математической практике функции, и привести пример не лежащей в этом классе функции очень трудно. Кроме того, для любой теории
класс
можно описать в терминах вычислительной сложности.
Примечание 2. Если в определении
-корректности заменить "останавливается" на "не останавливается", то получится
-корректность, которая эквивалентна непротиворечивости (т.е. получится более слабое свойство).