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

Докажем, например, справедливость правила противопостав­ ления обратного А - ^ В [ - 2? - » Л и проанализируем доказательство: 1) А -> В, В, А ( - В, 2) А -» В, В, А |— В — удаление 3) А -> В, В \— А введение 4) А -» В |— В -> А, введение Правило 3. Подстановка вместо элементарных высказываний. Пусть В — некоторое составное высказывание, в которое вхо­ дят элементарные высказывания ах, ..., ап\ В' — высказывание, полученное из В одновременной подстановкой составных выска­ зываний Аи А„ вместо ах, а„. Тогда, если |— В, то (— В'. Благодаря этому правилу разрешается осуществлять подстановку в основные равносильности, логические следования и правила доказательства тавтологий. Замена элементарных высказываний на произвольные составные не нарушит строгости рассуждений. Правило 4. О замене. Пусть С 4 — составное высказывание, содержащее в качестве своей части составное высказывание А, а Св — высказывание, полученное из А заменой А на В. Тогда, если ]— , то (— Св. С учетом этих правил, формул и аксиом логика высказываний является полной теорией, так как все логические следствия выво­ димы, а все, что выводится, будет логическим следствием из дан ­ ных посылок. Логическое следование есть конечная алгоритмическая опера­ ция в отличие от логической выводимости. С помощью подстановок в любых формулах А и В заменятся препозиционными переменными либо другими формулами, что не нарушает требований, предъявляемых к теории. При этом ло­ гические операции между формулами и переменными сохраня­ ются. Теоремами теории Т являются тавтологии, т.е. общезначимые формулы, и только они: [— А <=> А — тавтология. Прямым след­ ствием этой теоремы является формальная непротиворечивость и полнота теории Т. Итак, всякая теорема исчисления высказыва­ ний является тождественно-истинным высказыванием, и, наобо­ рот, всякая тождественно-истинная формула является теоремой исчисления высказываний. Исчисление высказываний выполняет задачу порождения общелогических законов как тождественно­ истинных высказываний. В построенной формальной теории Т выводимы многие важ­ ные для практических целей формулы. Они получаются «перефра­ зированием» теорем с добавлением дополнительных связок. Они называются, естественно так же, как и связки булевых перемен­ ных: v — дизъюнкция, а — конъюнкция. Приведем некоторые важные формулы. 222