Примеры выводов. 
Дискретный анализ. 
Формальные системы и алгоритмы

Докажем ослабленный «синтаксический» вариант леммы 3.49.

Лемма 3.57. Пусть формула, А имеет единственный параметр х и не содержит вхождений переменной у. Тогда /уА (х:=у) Ь Ух А.

Доказательство. Вот вывод формулы VхА.

Единственный шаг в этом выводе, который нуждается в объяснениях, это шаг 2. Формула А получается из А (х:=у) подстановкой вместо переменной у терма х (состоящего из одной переменной). Так как формула Л (х:—у) получена заменой всех свободных вхождений х на у, терм х свободен для переменной у в формуле А (х:=у). Таким образом, условия утверждения 3.48 выполнены и вторая строка действительно является частным случаем схемы аксиом (А4). ?

Лемма 3.58. Пусть формула, А имеет единственный параметр х. Тогда 1 У х А Ь 3x1 А.

Доказательство. Напомним, что формула 3 х~А — это сокращённая запись формулы 1/т1"|А Докажем вначале, что /хТА ~ /хА:

На втором шаге этого вывода мы применили аксиому (А4) с подстановкой терма х вместо переменной х (такая подстановка всегда корректна).

По слабой теореме дедукции получаем, что формула (VffTlA)—> V#A выводима. Так как в исчислении высказываний выводима формула (А—?В)—?(~В—?~А), то получаем выводимость формулы 1 /хА—>1 VxIlA По правилу modus poiiens из этой формулы и гипотезы 1 /хА выводится формула IV я~П А. ?