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