Статья 484

Общность не нарушится, если при применении слабых правил мы будем использовать только термы, входящие в формулы нижней секвенции или первую свободную переменную, если ни один терм не входит в формулы нижней секвенции.
Продемонстрируем для примера поиск доказательства секвенции.
Формула нижней секвенции не содержит свободных переменных. Единственная возможность - применить слабое правило для квантора существования.
Теперь применяем правило для введения импликации справа в силу сформулированных выше предпочтений.
Затем применяем сильное правило для введения квантора существования влево.
На следующем шаге применяем слабое правило для квантора существования. Какой терм мы должны использовать. Использование ничего нового не дает, поэтому используем.
Заметим, чтобы ликвидировать неопределенность в выборе искомого терма, мы, не нарушая общности, могли бы переформулировать слабые правила для кванторов следующим образом, где все термы свободны.