Гильберт

При этом не обязательно выбирать представителя однозначным способом; наше конкретное правило действует лишь в случае, когда x пробегает множество чисел 0, 1, 2, ... Вместо этого мы будем считать, что квантор ?x обладает универсальной приложимостью и в каждом случае выбирает для нас некоторого представителя. Аксиома выбора Цермело оказывается, таким образом, вплетенной в принцип исключенного третьего. Это смелый шаг, но чем смелее, тем лучше; лишь бы быть уверенным, что мы остаемся в рамках непротиворечивости!

В формализме пропозициональные функции заменяются формулами, обращение с которыми должно быть описано без ссылок на их значение. В общем случае переменные x, y, ... будут встречаться среди символов некоторой формулы A. Мы говорим, что символ ?x связывает переменную x в формуле A, если он предшествует этой формуле 25, и говорим, что x свободна в формуле A, если она не связана квантором с индексом x. При этом x, y, , ?x представляют собой символы, входящие в формулу; готические буквы не применяются для обозначения таких символов, а используются для коммуникации. Нашу основную аксиому (8) более естественно рассматривать как правило для образования аксиом. Она выражает следующее: возьмите любую формулу A, в которой x является единственной свободной переменной, и любую формулу b без свободных переменных и с их помощью образуйте новую формулу