Производные правила вывода

Уже довольно глубоко развита аксиоматическая теория высказываний: теорема о дедукции, вскрыв важное свойство выводимости, оказалась мощным средством, облегчающим процесс доказательства того, что та или иная формула является теоремой формализованного исчисления высказываний. Следующим шагом на этом пути служит выявление дальнейших закономерностей процесса выведения одних формул из других и формулировка таких закономерностей в виде правил вывода. Получаемые вторичные правила вывода носят названия производных правил вывода. Разделим их на две группы и сформулируем их в двух теоремах: в одной — производные правила введения логических связок, в другой — производные правила удаления таких связок.

Теорема 14.9 (правила введения логических связок). Справедливы следующие производные правила вывода, называемые правилами введения логических связок (где Г — некоторое, возможно, и пустое множество формул).

Доказательство. а) Данное правило есть не что иное, как теорема о дедукции (теорема 14.4).

б) Обосновать правило предлагается самостоятельно. Напомним только, что запись F G, согласно определению, означает ?(F ?G).