замечание. Можно указать на ещё одно философское различие между ситуацией с теоремой Ферма и ситуацией с континуум-гипотезой. Обсуждая вопрос о возможных доказательствах теоремы Ферма или её возможных опровержениях (т. е. доказательствах её отрицания), мы исходили из понятия доказательства в общем, неформальном смысле; об этом понятии – наше шестое размышление. Упоминавшиеся же открытия Гёделя, установившего, что континуум-гипотезу нельзя опровергнуть, и Коэна, установившего, что континуум-гипотезу нельзя доказать, утверждают невозможность формальных доказательств в рамках некоторого ранее известного конкретного представления о формальном доказательстве – более точно, в рамках некоторой конкретной аксиоматики теории множеств, а именно так называемой системы Цермело – Френкеля. Однако считается (мнение это представляет собой не что иное, как акт веры), что система Цермело – Френкеля позволяет формализовать любое неформальное математическое доказательство. Это и даёт право говорить, что континуум-гипотезу нельзя ни доказать, ни опровергнуть какими бы то ни было средствами, допускаемыми современной математикой.

Обсуждаемая тема имеет самое тесное отношение к знаменитой теореме Гёделя о неполноте. Теорема эта утверждает, что, какое бы ни было предложено понятие формального доказательства, имеется такое утверждение о натуральных числах, что ни оно само, ни его отрицание не обладает формальным доказательством в рамках предложенного понятия. Мы исходим из очевидности того, что возможны различные определения формального доказательства. Эти определения отличаются друг от друга набором допускаемых аксиом и правил вывода. Могут быть такие представления о формальном доказательстве, в котором вообще не используются ни аксиомы, ни правила вывода. Короче говоря, подходы к понятию формального доказательства могут быть весьма различны. Но все эти подходы имеют и фундаментальную общность, выражаемую в следующих принципах:

1. Каждое формальное доказательство есть текст, т. е. конечная цепочка знаков, выбранных из некоторого алфавита;

2. Каждый текст, составленный из букв рассматриваемого алфавита, поддается алгоритмической проверке на предмет того, является ли он формальным доказательством или нет, и если да, то какого именно утверждения;