Вы в одном месте правильно указали требуемые пропозициональные тавтологии, в другом - преобразовали свой вывод на вывод после применения теоремы о дедукции. В одном месте говорите, что он поможет всё решить, в другом - что не можете обработать даже простые входные данные задания 4 (предварительно потребовав их от меня). Странно всё это.
Тут всё просто: те выводы, которые нужны, конструируются как-то не очень прозрачно — а вот эквивалентные им по т. о д. идут как по маслу. После чего применяем к такому прозрачному выводу прозрачную процедуру из теоремы — да, в результате получится монстр о десятках формул — но проверять корректность-то не человеку. Если мы напишем неправильный вывод, программа первой же скажет, что это не работает, так что сделать что-то неправильно таким способом нельзя. (А можно возложить весь вывод на программу, см. ниже.)
P.S. Я догадываюсь, что вы изобрели какой-то "универсальный метод" и тщетно пытаетесь мне растолковать его применение для первого правила Бернайса.
Вряд ли даже переизобрёл — просто сложил два и два. Уверен, через какое-то время и вам это станет более-менее очевидно.
Но это снова наталкивается на необходимость выводов, которые ничуть не проще, и даже может быть сложнее тех, которые в книге:
В общем случае нет. В книге кусок вывода, соответствующий применению эквивалентности пропозициональных формул, опущен только из-за доказанной раньше теоремы о
для исчисления высказываний, и конструирование вывода возложено на неё (и с ним справится в данном случае программа при любом корректном входе).