•    Устранение импликаций:

•    Перемещение связоквнутрь выражений. Кроме обычных правил для отрицаемых связок, нам нужны правила для отрицаемых кванторов. Поэтому получаем следующие правила:

Рассматриваемое высказывание проходит через такие преобразования:

Обратите внимание на то, что квантор всеобщностив предпосылке импликации стал квантором существования. Теперь это высказывание приобрело такое прочтение: "Либо существует какое-то животное, которого x не любит, либо (если это утверждение не является истинным) кто-то любит х". Очевидно, что смысл первоначального высказывания был сохранен.

•    Стандартизация переменных. В высказываниях наподобие , в которых дважды используется одно и то же имя переменной, изменим имя одной из переменных. Это позволит в дальнейшем избежать путаницы после того, как будут удалены кванторы. Поэтому получим следующее:

•    Сколемизация. Сколемизация — это процесс устранения кванторов существования путем их удаления. В данном простом случае этот процесс подобен применению правила конкретизации с помощью квантора существования, приведенного в разделе 9.1: преобразовать, где А — новая константа. Однако, если это правило будет непосредственно применено к высказыванию, рассматриваемому в качестве примера, то будет получено следующее высказывание:

которое имеет полностью неправильный смысл: в нем утверждается, что каждый либо не способен любить какое-то конкретное животное А, либо его любит некоторая конкретная сущность В. В действительности первоначальное высказывание позволяет каждому человеку не быть способным любить какое-то другое животное или быть любимым другим человеком. Поэтому желательно, чтобы сущности, определяемые в процессе сколемизации, зависели от х: