По-видимому, стоит кратко объяснить, каким образом формализм Гильберта позволяет восстановить принцип исключенного третьего, служивший главным объектом критики Брауэра. Рассмотрим бесконечную последовательность чисел 0, 1, 2, ... Любое свойство A чисел (например, «быть простым») может быть представлено пропозициональной функцией A(x) («x простое»), из которой подстановкой конкретного числа b вместо переменной x можно получить конкретное утверждение A(b) («b простое»). Согласно принципу, отрицаемому Брауэром и которого хочет придерживаться Гильберт, имеем либо
принцип исключенного третьего
A
A
x
x
b
x
A
b
b
* существует число x, для которого справедливо утверждение A(x),
x
A
x
либо
* A(x) не справедливо ни для какого x.
A
x
x