ГЕДЕЛЬ, ЭШЕР, БАХ: эта бесконечная гирлянда.

Квантор существования.

Два предыдущих правила объяснили нам, как можно убрать квантор общности и вернуть его на место; следующие два правила покажут, как обращаться с кванторами существования.

ПРАВИЛО ОБМЕНА: Представьте, что u — переменная. Тогда строчки Au:~ и ~Eu: взаимозаменимы везде внутри системы.

Давайте, например, применим это правило к аксиоме 1:

Aa:~Sa=0  аксиома 1.

~Ea:Sa=0  обмен.

Кстати, вы можете заметить, что обе эти строчки — естественный перифраз в ТТЧ высказывания «Нуль не следует ни за одним из натуральных чисел.» Следовательно, хорошо, что они могут быть с легкостью превращены одна в другую.

Следующее правило еще более интуитивно. Оно соответствует весьма простому типу рассуждений, который мы употребляем, переходя от утверждения «2 — простое число» к утверждению «существует простое число.» Название этого правила говорит само за себя:

ПРАВИЛО СУЩЕСТВОВАНИЯ: Предположим, что некий терм (могущий содержать свободные переменные), появляется один или много раз в теореме. Тогда каждый (или несколько, или все) из этих термов может быть заменен на переменную, которая больше нигде в теореме не встречается, и предварен соответствующим квантором существования.

Давайте применим, как обычно, это правило к аксиоме 1:

Aa:~Sa=0  аксиома 1.

Eb:Aa:~Sa=b  существование.

Вы можете поиграть с символами и при помощи данных правил получить теорему: ~Ab:Ea:Sa=b.