Спирина, М.С. Дискретная математика

Правило подстановки (ms). Если формула В является частным случаем формулы Д, то В непосредственно выводима из А. Другая формулировка правила подстановки имеет вид: если Е — выводи­ мая формула, содержащая символ А (т.е. Е(А)) , то выводима фор­ мула Е(В) , полученная из Е заменой всех вхождений А на произ­ вольную формулу В: т.е. ^ . Ь(В) Правило modus ponens (тр). Если набор формул А , В, С являет­ ся частным случаем набора формул А, А -> В, то формула С явля­ ется непосредственно выводимой из формул А и В. Тогда доказан­ ные правила могут стать новыми правилами вывода. Так, теорему 2 о введении импликации можно сделать новым правилом вывода: А \= В ^ А . Приведем некоторые общие правила. Правило 1. Общие свойства символа |= (|— ). При п > 1 А |, А 2 , ..., Ап }= Д), Д2, *'м Д« Д 2 » ■■■) До Дг> •••5 Д„ [= Д„ — из набора формул непосредственно выводима каждая. Если Дь Д2, ..., Д„ (= С, то Дь Д2, ..., Д„, Ви Вт (= С, т .е . добавление лишних формул при сохранении непротиворечивости не влияет на выводимость. Если при т > 0 и п > ОД,, Д2, ..., Ат |= Ви ..., Д],Д2,...,Д,П \= В„ и Ви В2, ..., Вп (= С, то Д,, ..., Ат \= С — транзитивность непосред­ ственной выводимости. Те же свойства справедливы для выводимости [—. Правило 2. Введение и удаление логических знаков. Пусть А, В, С — произвольные высказывания. Обозначим Ф — конечный список высказываний, быть может пустой. Правила вве­ дения и удаления логических знаков представим в виде табл. 5.2. С помощью этих правил можно доказать другие равносиль­ ности. Т а б л и ц а 5.2 Правила введения и удаления логических знаков Операция Правила введения Правила удаления —> (Ф, А |— В) <=> (Ф |— А —>В) А, А —> В |— В Л А, В |— А л В А л В \— А; А л В |— В V A)—A v В Если Ф, А \— С и Ф, В f - С, то Ф, A v В \— С “1 Если Ф, A В и Ф, Д (— В. то Ф [— А А \ - А ; А [ - А->В (слабое удаление) 3 А = В, В =А \ - А ^ В А =В \ - А-^> В,А = В \ - В^у А 221