Математическая логика и теория алгоритмов. Для изучающих компьютерные науки

Иногда правило вывода modus ponens записывают в виде: ^ ^ ^ В Здесь в числителе перечислены гипотезы (посылки), в знаменателе - следствие из этих посылок, а символ стоящий справа, указывает, что данное правило исключает или вводит этот символ. Тогда рассмотренные правила можно записать следующим образом: теорема дедукции: GA \-В:G =^; А ^В правило перевертывания: GA \- В; G, —iB — i; -А А &В А & В правило удаления &:— — & , —^— &; правило введения &: &; А &В В &А А А правила введения v; v , v ; AwB BvA правило доказательства разбором случаев: А_ 1-Е В \-С, А УВ V ; С правило сведения к нелепости: А \- В, А \-_—В — i . -А Отметим, что перечисленные производные правила вывода позволяют намного упростить выкладки в теории L. Подчеркнем, что в принципе можно и не пользоваться этими производными правилами вывода, а пользоваться только правилом MP. Однако при этом, может быть, придется проводить более громоздкие выкладки. Например, если при выяснении, теорема или нет формула А, пользовались теоремой дедукции, то при отказе от этой теоремы дедукции фактически придется ее доказывать для этого частного случая. В других подобных случаях снова придется ее доказывать. § 11. Свойства исчисления высказываний Непротиворечивость исчисления высказываний . Исчисление высказываний, как и любую формальную аксиоматическую теорию, содержащую символ —1, будем считать непротиворечивой, если ни для какой формулы А не имеет места |-^ и |—А, т.е. не может быть, чтобы одновременно были выводимы А и —А. Для доказательства непротиворечивости исчисления высказываний (теории L) предварительно докажем теорему. Теорема 4.3. Всякая теорема теории L есть тавтология. Доказательство. Легко убедиться, например, с помощью таблиц истинности, что каждая аксиома теории L есть тавтология. Известно, что если А иА^ В тавтологии, то и 5 тавтология (см. теорему 1.1), т.е. правило modus 115