Непротиворечивость и разрешимость исчисления высказываний
Обновлено: 13.05.2024
Исчисление называется противоречивым, если существует формулатакая, что в этом исчислении доказуемы обе формулыиЕсли такой формулы нет, то исчисление называетсянепротиворечивым. Здесь под доказуемостью формулыпонимается доказуемость секвенцииНиже мы убедимся в том, что построенное нами исчисление высказываний является непротиворечивым. Затем мы обсудим вопросыполнотыиразрешимостиИВ.
Семантика и синтаксис
В формальной математической теории действия, производимые над рассматриваемыми объектами в рамках самой теории, составляют синтаксистеории. Вопросы, выходящие за рамки формальной теории (например,интерпретациярассматриваемых понятий, “придание смысла” некоторым из них и т.д.), составляютсемантикуэтой теории. В частности, формулы, секвенции, правила вывода, формальные доказательства – это синтаксис ИВ. Далее мы рассмотрим ряд семантических понятий.
Интерпретации ив
Пусть – непустое множество,– множество всех его подмножеств. Пусть– множество всех формул ИВ,– множество всех атомарных формул. Рассмотрим произвольное отображениеПродолжим его до отображенияа затем определимдля секвенций. Продолжениес атомарных формул на произвольные построим индуктивно, а именно: еслииуже построены, то полагаем:Итак, каждой формулеисчисления высказываний ставится в соответствие подмножествомножестваСеквенциям ИВ будем ставить в соответствие некоторыеутверждения о подмножествахмножества а именно:
В вышеприведённых определениях принято следующее соглашение: если (т.е.тоОтметим, что так как множествопредполагается непустым, толожно (при любой интерпретации).
Проверим, что аксиомам в данной интерпретации будут поставлены в соответствие истинные утверждения, а применение правил вывода истинность утверждений не нарушает. В самом деле, аксиомы имеют вид поэтомуа это утверждение истинно. Для правил вывода сделаем выборочную проверку. Докажем, что если числителю правила вывода поставлены в соответствие истинные утверждения (о подмножествах множествато знаменателю также будет поставлено в соответствие истинное утверждение. В качестве примера возьмём правила 1 и 6.
Правило 1:
Пусть Еслито мы имеем:иНо тогдаа это означает, чтоистинно.
Правило 6:
Пусть Положим(приввиду наших соглашенийПо условиюиОтсюда получим
Теорема 1. Исчисление высказываний непротиворечиво.
Доказательство. Предположим, что для какой-либо формулыдоказуемы секвенциииРассмотрим какую-либо интерпретациюисчисления высказываний в множествеТак как для аксиомутверждениеистинно и применение правил вывода не нарушает истинность секвенций, то для всех выводимых (т.е. доказуемых) секвенцийутверждениетакже истинно. Значит,ПоэтомуНоследовательно,что неверно. Таким образом, ИВ непротиворечиво.
Рассмотрим теперь главную интерпретацию ИВ. Это будет отображениегде– множество всех формул, а– множество всех секвенций. Для атомарных формулзначениявыберем произвольным образом. На остальные формулы отображениераспространим по обычным правилам:гдеОтображениеможно рассматривать как присвоение значений истинности (“истина” или “ложь”) пропозициональным переменным. После того, как такое присвоение произошло, можно говорить об истинности или ложности других формул. Истинность или ложность секвенций определяется следующим образом:
либо при некоторомлибо
Сформулируем теперь эти определения другими словами. Пусть – формула ИВ, зависящая от пропозициональных переменных (атомарных формул)а– набор из 0 и 1. Будем говорить, чтоформула истинна на наборееслипри. . . ,Пусть дана секвенцияи– пропозициональные переменные, входящие в какие-либо из формулСеквенцияистинна на наборе из 0 и 1, если на этом наборе либо хотя бы одно изложно, либоистинно. Далее, секвенцияистинна на наборе если хотя бы одна из формулна этом наборе ложна. Секвенцияистинна на данном наборе, если на этом набореистинно. Наконец, секвенциясчитаетсяложной на любом наборе.
Отметим, что главная интерпретация является частным случаем интерпретации, рассмотренной ранее. Действительно, пусть состоит из одного элемента. ТогдаСчитаем для формулыеслииеслиНепосредственно проверяется, что получится главная интерпретация.
Формула (соответственно, секвенция) называетсятождественно истинной, если она истинна на любом наборе значений истинности пропозициональных переменных. Нетрудно видеть, что тождественная истинность формулыравносильна тождественной истинности секвенции
Лемма 1. Секвенцияистинна на наборев том итолько в том случае, если секвенция истинна на этом наборе.
Доказательство. Пустьистинна на набореТогда выполняется хотя бы одно из условий: 1) хотя бы одна из формул множестваложна на этом наборе; 2) формулаложна на этом наборе; 3) формулаистинна на этом наборе. Разберём эти случаи отдельно. 1) Если какая-нибудь формула изложна, тоистинна, а значит,истинна. 2) Еслиложна, тоистинна, поэтомуистинна. 3) Еслиистинна, тоистинна, а значит,также истинна. Обратное утверждение доказывается аналогичным образом.
Следствие. Секвенциятождественно истинна в том и только в том случае, если секвенциятождественно истинна.
Лемма 2. Секвенциядоказуема в том и только в том случае, если секвенциядоказуема.
Доказательство. Если секвенцияимеет доказательство, то по правилу 7 это доказательство можно продолжить и получитьНаоборот, если доказана секвенциято из неё по правилу 12 получимУчитывая легко доказываемый фактпо правилу 8 получим
Лемма 3. а) Если секвенциядоказуема, то она тождественно истинна; б) если формуладоказуема, то она тождественно истинна.
Доказательство. Нетрудно проверить, что аксиомы являются тождественно-истинными секвенциями. Также легко проверяется, что применение правил вывода эту тождественную истинность не нарушает. Значит, любая выводимая (доказуемая) секвенция тождественно истинна. Утверждение, касающееся формул, сводится к уже доказанному для секвенций.
Лемма 4. Если формулыиэквивалентны, то булевы функцииисовпадают.
Доказательство. Можно считать, что формулыизависят от одних и тех же пропозициональных переменных(переменные, которые не входят в формулу, считаем входящими фиктивно). По условиюи– доказуемые секвенции. По лемме 3 они тождественно истинны. Если на каком-либо набореформулаистинна, то так как секвенцияистинна, тона этом наборе тоже истинна. Аналогично доказывается, что еслиистинна на наборетотакже истинна на этом наборе. Итак,иистинны на одних и тех же наборах, значит,
Для формулы обозначим черезмножество наборовна которых она истинна.
Замечание. Лемма 4 на самом деле является следствием более общего результата: если для некоторых формулисеквенциядоказуема, то
Теорема 2 (о функциональной полноте ИВ). Пусть в исчислении высказываний бесконечно много атомарных формул. Тогда для любой булевой функциисуществует формулаисчисления высказываний, зависящая от атомарных формултакая, что
Доказательство. Еслитождественно равна 0, то в качестве формулыможно взятьЕсли жето, как известно из курса дискретной математики,представима в совершенной дизъюнктивной нормальной форме:
Следовательно, в качестве формулы исчисления высказываний подойдёт формула
Из леммы 3 мы видели, что доказуемыми могут быть только тождественно истинные формулы или секвенции. Оказывается (и это мы докажем в следующей теореме), что верно и обратное: тождественно истинная формула или секвенция имеет формальное доказательство в ИВ. Этот факт мы будем называть полнотойисчисления высказываний. В конце главы будет рассмотреноинтуиционистское исчисление высказываний, которое не обладает свойством полноты.
Теорема 3(о полноте ИВ).
(а) Формула исчисления высказываний доказуема тогда и только тогда, когда она тождественно истинна.
(б) Секвенция ИВ доказуема тогда и только тогда, когда она тождественно истинна.
Доказательство. Ввиду леммы 2 и следствия из леммы 1 доказуемости (соответственно, тождественные истинности) следующих секвенций эквивалентны:. . . Таким образом можно “перебросить” все формулы, стоящие слева от значкав правую часть и получить секвенцию видадля которой доказуемость (соответственно, тождественная истинность) равносильна доказуемости (соответственно, тождественной истинности) формулы(по определению). Следовательно, нам надо доказать только утверждение (а).
Ввиду леммы 3 нам следует доказать лишь достаточность: если формула тождественно истинна, то она доказуема. Пусть– тождественно истинная формула. По теореме 2 предыдущего раздела существует формулатакая, что
Положим . . . ,Так както по лемме 4тождественно истинна. Но это означает, что формулытождественно истинны. Рассмотрим какую-нибудь одну из них, например,Если всеразличны, тоне будет тождественно истинной, так как обращается в 0 на таком наборе, гдеЗначит, вкакая-либо пропозициональная переменная (скажем,встречается вместе со своим отрицанием. Следовательно,можно преобразовать:Секвенция доказуема по лемме 4 § 1.1. По правилу вывода 4 получим, что секвенциядоказуема. Значит, формуладоказуема. Аналогично получим, что формулыдоказуемы. По правилу 1 получим, что формуладоказуема. Следовательно, формулаа значит, и формуладоказуема.
Докажем теперь разрешимость исчисления высказываний. Под разрешимостью мы понимаем существование алгоритма, который по данной формуле (или секвенцииопределяет, доказуема эта формула (или секвенция) или нет. Такой алгоритм действительно существует.
Теорема 4. Исчисление высказываний разрешимо.
Доказательство. По теореме 3 проверка доказуемости формулы или секвенции сводится к проверке её тождественной истинности. Алгоритм такой проверки очевиден: надо придавать пропозициональным переменнымвходящим в рассматриваемые формулы, всевозможные значения(из множестваи определять по таблицам истинности значение формулы(соответственно, секвенцииЕсли на любом наборе будем иметь(соответственно,то(соответственно,тождественно истинна, а значит, доказуема, в противном случае(илинедоказуема.
Замечание. Пусть формула тождественно истинна, в чём мы убедились, применив алгоритм, изложенный в теореме 4. Тогдаимеет доказательство. На самом делеможно построить алгоритм, выписывающий это доказательство (т.е. доказательство секвенции Алгоритм достаточно громоздкий, так как включает в себя (в качестве “подпрограмм”) доказательства утвержденийи многих других, ведь мы приводим формулук видудоказываем формулузатем продолжаем доказательство, пока не будет доказана формула
Читайте также: