Ты право, пьяное чудовище

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

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

Пенроуз пишет, что задача найти нечетное число, которое можно представить в виде суммы двух четных, приводит к перманентному «зависанию» машины Тьюринга, хотя даже первоклассник разбирается с ней мгновенно. Но я что-то не могу поверить, что компьютер нельзя запрограммировать так, чтобы он сразу же сообщал, что такого числа не может быть, потому что не может быть никогда?

Сэр Роджер Пенроуз о платоническом мире математических объектов

Спасибо уважаемой yoginka, чей интерес к теме сподвигнул меня на чтение второй книжки Пенроуза.