Хочу, чтобы проверили меня, нельзя ли укоротить что-нибудь или упростить.
Теорема о правиле Modus Ponens. Пусть

и

обе тавтологии. Тогда и

— тавтология.

Допустим,

опровержима. Тогда есть набор значений переменных, при которых она принимает значение

. Тогда на этом наборе значение

(

) тоже

, что невозможно в силу того, что

тавтология и ни на каком наборе значений переменных значения

не принимает. Значит,

всё-таки тавтология.

Более длинную теорему лень переписывать всю (точнее, её длинное доказательство), спрошу только в деталях. Пусть

— правильно построенная формула [ранее её индуктивное определение], не являющаяся пропозиц. переменной. Тогда эта формула может иметь один из видов

,

,

,

, где

,

— п. п. ф.. Правильно я понимаю, что надо доказать именно то, что подформулы

и

— правильно построенные? А то мне эта теорема кажется естественным продолжением индуктивного определения, не понял, что от меня требуется. Могу привести и определение, вдруг они различаются в деталях. (Просто пока лень.)
А ещё, какие есть обозначения для замены

в

на

и подстановки

вместо

в

? У нас они какие-то неудобоваримые. (Странно, как вообще такие выбирают для использования.)