Создавая теорию доказательств, Гильберт делает ставку на принцип, известный как Tertium non datur («Третьего не дано»), или закон исключенного третьего. Это полезный инструмент для математических доказательств; по сути, он гласит, что для любого математического суждения существует лишь два возможных состояния. Истина или ложь. Включено или выключено. Да или нет. Идти или остаться. Никаких «если», «и» или «но». Черное или белое – и никогда серое.

Но это не совсем точно. Лучше сформулировать Tertium non datur так: «Истинно или неистинно». Такая формулировка точнее, потому что закон исключенного третьего – это не предложение «А или Б», он гласит, что у вас есть либо А, либо не-А. Никакого «отчасти А». Никакого «подобного А». Никакого «вроде А». Никакого «может быть, А».

Tertium non datur – чрезвычайно удобный инструмент для математического доказательства, поскольку он обладает огромным охватом. Он означает, что вы можете установить истинность суждения, показав, что оно не является ложным, – отрицание отрицания равносильно утверждению истины. Это значит, что вам не обязательно доказывать всё исчерпывающим перебором. Достаточно показать, что нечто истинно в одном случае или что противоположное неистинно, – часто путем демонстрации того, что иная возможность (A, или не-А) влечет за собой логическое противоречие.

Вспомним снова игру в шахматы. Кто выиграл последнюю партию? Черные или белые? Теория шахмат Цермело гласит, что при завершении игры либо побеждает одна из сторон, либо партия заканчивается вничью. Допустим, никто не знает, победили ли черные. Используя Tertium non datur, мы рассуждаем так: Выиграли белые? Нет. Была ничья? Нет. Значит, единственный возможный вывод – победили черные.

Это звучит болезненно упрощенно, но это логический подход к рассуждению, идущий еще из Древней Греции. (Аристотель сам первым сформулировал закон исключенного третьего.) Но лишь в конце XIX и начале XX века принцип Tertium non datur начал приобретать еще большую значимость, так как математики обнаружили, что могут использовать его вместе с теорией множеств, чтобы обращаться с бесконечными сущностями при помощи финитных средств. Благодаря закону исключенного третьего вам не нужно строить бесконечное множество, чтобы с ним работать. Вы можете использовать Tertium non datur, например, для построения «чистого доказательства существования» – метода, который так любит Гильберт. «Доказательства существования, проведенные с помощью принципа исключенного третьего, обычно особенно привлекательны своей удивительной краткостью и элегантностью», – говорит он.

Интуиционистский подход и конструктивная математика Брауэра гласят, что вы можете окончательно ответить на тот же вопрос о победе черных в шахматах, только если это можно продемонстрировать (возможно, реконструировав ходы с начала и показав, что на последнем ходу черный конь берет белого короля). Его позиция революционна, пусть и деструктивна. Тысячи лет никто толком не ставил под сомнение принцип исключенного третьего. Но, по мнению Брауэра, все, что не сконструировано, не обязательно имеет силу – включая и сам закон исключенного третьего. Tertium non datur – это не сконструированное утверждение, с точки зрения Брауэра. Он не просто ставит его под сомнение – он отметает его как бессмысленную комбинацию недоказанных слов.