Положим
(modus ponens)
Нет, modus ponens - это вывод
если у нас уже есть
и
(просто определение правила вывода).
Где ошибка?
Ну собственно если для любых
и
, выбираемых независимо,
, то действительно
. Если вы имели в виду что-то другое - попробуйте явно выписать кванторы.
Я специально выписал последовательность переходов со всеми нужными кванторами явно. Какой первый переход вам непонятен?
В 1.13 вводится дополнительное условие для
, используемое при выведении (1.14).
Подстановкой 1.13 в 1.12 мы получаем просто следствие из 1.12. Потом можно подставить что-то другое и получить другое следствие. И этими следствиями можно пользоваться одновременно. Только нужно не забывать, что если в этих следствиях самих остались
- то они верны только для тех
, которые мы подставляли. Но в (1.14)
не осталось, поэтому неважно, что мы туда подставляли.
Попробую привести искусственный пример, больше похожий на происходящее.
Зафиксируем
. Пусть
таково что для любого
выполнено
.
Раз (1) выполнено для любого
, то выполнено и для
. Подставим, получим
. И это уже следствие изначального условия, никак от
не зависящее (
в него вообще не входит).
Теперь подставим
в исходное условие, получим что
выполнено для любого
. Значит в частности выполнено для
. Подставим, получим
.