Всё ниже насчёт a):
Установите сначала, что если
и
, то
(используя 4.1.5, 4.1(j), D3 и ещё что-то).
Будем и дальше пользоваться теоремой о дедукции 4.1.5 и выводимостями 4.1(…) и вообще иметь в виду то, что если
, …,
и
, то
.
Имеем следующие вещи:
•
,
•
,
Тут приходится прерваться, потому что у вас удаление
не предоставили. Неудобно. Попробуйте доказать сами, что
, больно полезная штука. Полезно также, и нам тоже потребуется, введение
:
. Продолжим:
•
, отсюда
•
•
•
• но мы также имеем
• так что, раз
и
, выходит
• так что
В обратную сторону проще: контрапозицией 4.1(e, e′) мы получим
и
, что в соединении с 4.1(j) даёт нам вывести нужное
.
Список производных выводимостей в вашем курсе какой-то не систематичный, и хотя дана метатеорема о дедукции, не дана метатеорема про выводимость, которую я привёл — потому остаётся гадать, насколько можно оторваться, а насколько вам придётся восполнять такие непростительные пробелы (так как задания на блуждание в тёмном лесу на ручное составление вывода на низком уровне — это довольно бессмысленная штука; нам же формализация логики не для того нужна).
Если пока можно только предъявлять составленный руками вывод, придётся разворачивать все применения метатеорем… мда.