полнота исчисления высказываний

полнота исчисления высказываний Полнота и непротиворечивость исчисления высказываний Определение 1.   Абстрактной буквой называется класс символов (конкретных букв),  которые мы считаем одинаковыми. Множество абстрактных букв называется  алфавитом. Конечный ряд букв алфавита называется словом в алфавите. Замечание 1.   Алфавит исчисления высказываний состоит из трех групп символов:  пропозициональные переменные (обозначаются большими буквами); логические  символы  скобки.  и символ следствия  ; вспомогательные символы: запятая и  Определение 2.   Будем говорить, что задано исчисление высказываний  , если задан  алфавит  , множество слов алфавита   ­­ множество выражений исчисления, множество аксиом исчисления  правил вывода исчисления  .  и множество операций на множестве   ­­  Определение 3.   Любое утверждение, имеющее логическую значимость, называется  высказыванием. Определение 4.   Формулой ИВ назовем слово в алфавите, построенное по индукции:  пропозициональная переменная является формулой, и для двух формул    верно   и аналогичные логические конструкции ­­ тоже формулы. Определение 5.   Секвенция ИВ ­­ последовательность формул  четырех типов:  следующих   (из истинности   следует истинность  )  (   противоречивы) 1. 2. 3. 4.Определение 6.   Секвенция   называется доказуемой, если существует  последовательность секвенций ИВ   такая что  . Определение 7.   ИВ называется непротиворечивым, если не все формулы в нем  доказуемы. Теорема 1.   ИВ непротиворечиво. Доказательство. Дадим неформальное доказательство: если множество формул ИВ  непусто, то там найдется формула  формула будет недоказуемой.  . Построим формулу следующего вида  . Эта  Замечание 2.   Пусть пропозициональные переменные принимают булевские  . Тогда каждой формуле можно поставить в соответствие функцию,  значения  которая для каждого набора значений переменных дает 0 или  , т.е. указывает  истинность или ложность формулы на данном наборе. Тогда формулу можно  называть тождественно истинной, если соответствующая ей функция принимает  значение   на всех наборах входящих в формулу переменных. Определение 8.   Множество формул  либо  , либо  .  называется полным, если можно доказать  Полнота и другие свойства формализованного исчисления высказываний Если при изложении материала в предыдущей лекции рассмотрение велось как бы изнутри аксиоматической теории высказываний в процессе Развития темы, то ознакомление с  наукой об аксиоматической теории высказываний строят, опираясь на другой подход.  Установим ряд важных свойств этой теории: полноту, разрешимость,  непротиворечивость. Доказуемость формулы и ее тождественная истинность (синтаксис и семантика)В основе формализованного исчисления высказываний лежат понятия, относящиеся к так  называемой области синтаксиса, т.е. понятия, представляющие собой некие абстрактные,  лишенные смысла знаки и формальные действия с ними: алфавит, формула, аксиома,  правило вывода, доказательство, теорема. Эти понятия принято называть  синтаксическими. В то же время алгебра высказываний, изложенная ранее, пронизана содержательным  смыслом: за каждой пропозициональной переменной стоит конкретное высказывание  нашего языка, каждая формула может превращаться в конкретное составное  высказывание, некоторые формулы могут превращаться только в истинные высказывания  (тавтологии) и т.д. В данной сфере, являющейся областью семантики, каждое понятие  наполнено каким­то внутренним содержанием, смыслом. Понятия истины и лжи,  тождественной истинности и тождественной ложности формул, равносильности и  логического следования формул считают понятиями семантическими. Каково же взаимоотношение между формализованным исчислением высказываний и  алгеброй высказываний, между синтаксисом и семантикой? Перекинуть мостик от одной  области к другой и призвана теорема полноты, о которой пойдет речь в настоящей  лекции. Оказывается, формализованное исчисление высказываний построено так, что  всякая его теорема является тавтологией (тождественно истинной формулой) алгебры  высказываний, и, обратно, для всякой тавтологии алгебры высказываний можно построить ее вывод из аксиом формализованного исчисления высказываний, т. е. доказать, что она  является теоремой исчисления. В этом состоит теорема полноты. Таким образом, теорема полноты как бы свяжет абстрактную аксиоматическую теорию высказываний и  содержательную алгебру высказываний, теорию с практикой, и тем самым  продемонстрирует адекватность отражения абстрактной теорией наших практических  знаний о высказываниях языка. Сформулируем и докажем первую часть теоремы полноты.Теорема 16.1. Всякая доказуемая в формализованном исчислении высказываний  формула является тождественно истинной формулой (или тавтологией) алгебры  высказываний. Символически:  . Доказательство. Пусть формула  высказываний и последовательность  из аксиом. Покажем, что  длине   вывода этой формулы:  доказуема в формализованном исчислении   представляет собой вывод формулы     — тавтология. Доказательство будем вести индукцией по  . Тогда последовательность­вывод состоит из единственной формулы  1)  , которая, следовательно, может быть на основании определения вывода только аксиомой. Все три  аксиомы (А1), (А2) и (A3) являются тавтологиями алгебры высказываний на основании  теорем 3.1 (пункт з), 3.3 (пункт а), 3.3 (пункт л) соответственно; . Предположим теперь, что все формулы, имеющие вывод длины  2)  тавтологиями. Это предположение индукции; , являются  , также   — ее вывод длины   — произвольная формула  . Покажем, что всякая формула, имеющая вывод длины  . На основании предположения   членов данной последовательности — тавтологии. Рассмотрим  3)  является тавтологией. В самом деле, пусть  и  индукции первые  формулу  является тавтологией, как было отмечено в первой части доказательства), либо получена  из двух предыдущих членов этой последовательности    по правилуmodus ponens. Во втором случае тогда  формулы  Итак,  . По определению вывода, она может быть либо аксиомой (и тогда она   и   являются тавтологиями на основании предположения индукции.   и  . Следовательно, по теореме 3.5 (правило заключения)  .  и     и, кроме того, обеИтак, какой бы длины ни имела вывод в формализованном исчислении высказываний  формула, она будет тавтологией алгебры высказываний. Для доказательства второй части теоремы полноты (т. е. теоремы, обратной к только что  доказанной теореме) понадобится одна лемма, которой и посвящается следующий пункт. Лемма о выводимости. Пусть   или 1 (i=1,2,\ldots,n). Из  составленный из нулей и единиц, т.е. каждое  доказательства теоремы 10.3 известно, что всего таких наборов имеется   — упорядоченный набор длины   штук. ,  , для  σ ­Двойником, где   Определение 16.2.  формулы  истинное высказывание  переменных  что  указанной подстановке она превращается в ложное высказывание  Обозначение  Тогда символически данное определение можно записать так: ­двойника для формулы  таких высказываний  , или формула  σ   следующее:   называется или сама эта формула, если она превращается в   при подстановке вместо ее пропозициональных   соответственно,  , если при  .  . Пример 16.3. Найти  σ ­двойники для формул, еслиНаходим сначала значения этих формул при подстановке вместо  переменных   соответственно:  значений  Тогда, по определению  σ ­двойника, имеем Лемма 16.4 (о выводимости). Для всякой формулы  набора  выводимость:  или 1  , где   и всякого  , справедлива следующая  , где  Доказательство. Для доказательства применим индукцию по числу   логических связок,  использованных при построении формулы(в формуле  1)  пропозициональная переменная, например  принимает следующую очевидную форму:  . Тогда  ; , и утверждение леммы   нет логических связок). В этом случае формула FecTb  . Предположим, что утверждение леммы справедливо для всех формул с числом  2)  логических связок  ; . Покажем тогда, что утверждение леммы будет справедливо и для любой  3)  формулы с числом логических связок   — произвольная такая формула. Тогда на основании определения формулы формализованного исчисления высказываний /"имеет один из следующих двух видов:  Рассмотрим последовательно эти две возможности. . Пусть   или  .  Пусть сначала  связок, и для нее, по предположению индукции, будет справедлива выводимость . Тогда формула   содержит   логических   и  , то  , то есть  Покажем, что  таков, что  двойника имеем  принимает следующую очевидную форму:  таков, что  таковы:  форму  15.8, (пункт б) и следствия 15.5 из теоремы о дедукции. , то  . В этом случае требуемая выводимость принимает   и  . Данная выводимость действительно справедлива на основании теоремы   и соответствующие  σ ­двойники   ­σ   . В самом деле, если набор  . Далее, по определению 16.2  . В этом случае требуемая выводимость  . Если же наборИтак,  и  . Тогда, в силу теоремы 15.3, (пункт в) Рассмотрим теперь вторую возможность:  содержит  индукции:    логических связок; для каждой из них будет справедливо предположение  . Снова каждая из формул   и  Покажем, что  во всех случаях, которые могут представиться: , т.е.  . Расшифруем значения  σ ­двойников 1) набор  Тогда  таков, что   и  .  ­двойники имеют вид: σ и  вид:  теоремы 15.8, (пункт в), имеем  дедукции, заключаем, что  получаем  ; . Применив теорему 15.3, (пункт а),   . Требуемая выводимость принимает следующий  . Покажем, что это действительно так. В самом деле, на основании  . Тогда, по следствию 15.5 из теоремы о2) набор  Тогда  таков, что   и  ­двойники имеют в этом случае следующий  σ и  вид:  следующий вид:  доказательства выводимости в предыдущем случае; . Требуемая выводимость принимает  . Ее доказательство ничем не отличается от  3) набор  Тогда  таков, что   и  .  .  σ   ­двойники имеют следующий вид: и  Требуемая выводимость принимает следующий вид:  это действительно так. Ясно, что справедливы выводимости  и  ponons:  получаем  ;    (первая очевидна, а вторая следует на основе правила modus  . Из них, по правилу введения отрицания (теорема 15.9, пункт г),  .  . Покажем, что  4) набор  Тогда  таков, что   и  .σ ­двойники имеют вид: и  принимает следующий вид:    . . Требуемая выводимость . Первую формулу последовательности будем считать  Проверим, что это действительно так. Рассмотрим последовательность  формул  гипотезой. Вторая формула представляет собой аксиому (A1) формализованного  исчисления высказываний, а третья получена из двух предыдущих по правилу modus  ponens. Следовательно, рассматриваемая последовательность есть вывод ее последней  формулы  . Вспоминая теорему 15.3, (пункт а),  заключаем, что   из гипотезы  . Итак,  . Итак, рассмотренные четыре случая приводят к заключению: для любого набора  единиц справедлива выводимость  дает следующую выводимость:  нулей и , которая вместе с выводимостями (1) и (2) Тем самым сделан шаг индукции, и можно заключить, что утверждение леммы  справедливо для любой формулы  . Полнота формализованного исчисления высказыванийВ первом пункте настоящей лекции было сказано, что полнота формализованного  исчисления высказываний состоит в совпадении множества доказуемых формул с  множеством тавтологий. Включение первого множества во второе (первая часть теоремы  полноты) было установлено в теореме 16.1. Теперь нами все подготовлено к тому, чтобы  доказать вторую часть теоремы о полноте формализованного исчисления высказываний. Теорема 16.5. Всякая тождественно истинная формула (или тавтология) алгебры  высказываний доказуема в формализованном исчислении высказываний.  Символически:  . Доказательство. Пусть формула  высказываний. На основании леммы 16.4 о выводимости, имеем  является тавтологией алгебры  для любого набора  формула  высказывание (она — тавтология), то для любого набора  формулы   будет сама эта формула, т.е.   при любой подстановке превращается в истинное  σ   ­двойником  из нулей и единиц. Поскольку   для любого  σ . Тогда В частности, для   имеем (в этом случае  ) (1)а для   имеем (в этом случае  ) (2) Из выводимостей (1) и (2) по правилу удаления дизъюнкции (теорема 15.10, д) получаем Поскольку формула  посылок последней выводимости. Тогда  выводима из аксиом, то ее можно исключить из числа  Далее нужно брать в качестве а наборы следующих видов:  и  , для которых соответственно получим   Отсюда, также по правилу удаления дизъюнкции, получаеми далее . Проделав  в формализованном исчислении высказываний.  раз эту процедуру, придем к заключению, что  , т. е. формула   доказуема  Объединив теоремы 16.1 и 16.5, получим теорему о полноте. Теорема 16.6 (о полноте формализованного исчисления высказываний). Формула  тогда и только тогда доказуема в формализованном исчислении высказываний  (является теоремой исчисления), когда она является тавтологией алгебры  высказываний. Символически:  . Теорема адекватности Теорема адекватности является обобщением предыдущей теоремы о полноте и вытекает  из нее. Теорема 16.7 (адекватности). Формула  высказываний из конечного множества гипотез  является логическим следствием всех формул из этого множества. Символически:  выводима в формализованном исчислении   тогда и только тогда, когда онаДоказательство. Пусть  дедукции, данное утверждение эквивалентно тому, что . Тогда, по следствию 15.6 из теоремы о  Это утверждение, в свою очередь, эквивалентно, на основании теоремы полноты,  следующему: Теперь можно использовать результаты алгебры высказываний. На основании теоремы 4.4, (пункт г) последняя формула равносильна формуле (Точнее, на основании этой теоремы можно утверждать равносильность данных формул  лишь при  , но ясно, что утверждение нетрудно распространить и на произвольное  натуральное число т, например, методом математической индукции). Тогда из  тождественной истинности одной из формул и их равносильности заключаем, что и вторая формула также будет тавтологией (см. замечание 4.7). Итак, Это утверждение на основании теоремы 6.4 эквивалентно следующему:  , что и требовалось доказать.Непротиворечивость формализованного исчисления высказываний Непротиворечивость — важнейшее свойство, которым должна обладать аксиоматическая  теория. Противоречивая теория никакой ценности не имеет. Определение 16.8. Аксиоматическая теория называется непротиворечивой, если ни для  какого утверждения  , сформулированного в терминах этой теории, само утверждение  и его отрицание  некоторого утверждения   теории оба утверждения  аксиоматическая теория называется противоречивой.  не могут быть одновременно теоремами данной теории. Если для   — теоремы этой теории, то   и    Применительно к формализованному исчислению высказываний непротиворечивость  означает, что в нем не существует такой формулы  отрицание  выводимы из аксиом. Следующая теорема утверждает, что это действительно так.  являются теоремами формализованного исчисления высказываний, т.е.  , что сама формула и ее  Теорема 16.9 (о непротиворечивости формализованного исчисления  высказываний). Формализованное исчисление высказываний есть непротиворечивая  аксиоматическая теория. Доказательство. Допустим противное, т.е. предположим, что формализованное  исчисление высказываний противоречиво. Значит, имеется такая формула    являются теоремами формализованного исчисления высказываний. Тогда по теореме 16.1  , что   иявляется тавтологией алгебры высказываний. Но последнее  каждая из формул  невозможно на основании определения тавтологии. Следовательно, формализованное  исчисление высказываний непротиворечиво.  и  Разрешимость формализованного исчисления высказываний Определение 16.10. Аксиоматическая теория называется разрешимой, если существует  алгоритм, позволяющий для любого утверждения, сформулированного в терминах теории, ответить на вопрос, будет или нет это утверждение теоремой данной теории.         ПОЛНОТА ЛОГИЧЕСКИХ ИСЧИСЛЕНИЙ — выводимость в исчислении (логическ ой системе) всехутверждений (предложений, формуЛит.п.), обладающих некоторым подр азумеваемым для этого исчислениясвойством. Напр., П. классического исчисления высказ ываний (в какой­нибудь из возможных формулировок)означает выводимость в нем всех то ждественно истинных формул логики высказываний. Часто под П.исчисления понимают е е адекватность, т.е. не только справедливость П., но и корректность (soundness),непротив оречивость относительно подразумеваемого свойства: все выводимые утверждения облад аютнужным свойством (напр.: все выводимые в классическом исчислении высказываний ф ормулы тождественноистинны).         Семантическая П. — П. относительно свойства истинности в модели или классе мо делей.         Теорема Гёделя о П. утверждает, что всякая теория первого порядка (в том числе и  логика     предикатов,как теория с пустым множеством специальных аксиом) полна: форму   ла этой теории выводима тогда и толькотогда, когда эта формула истинна в любой модел и, в которой истинны аксиомы этой теории. Напр.,множество формул, выводимых в перво порядковой теории групп, совпадает с множеством формул, истинныхво всех группах. Ан алогичные утверждения справедливы и для иных логических языков; напр., для языкатождеств (формул вида t = s, где t и 5 — термы, выражения), квазитождеств (формул вида fj =  Sj &...& tn = sn ­> f J = sn+1) и др. Такого рода теоремы о П. позволяют заменить неэффекти вные понятия истинностипонятиями выводимости, имеющими алгоритмическую природу,  что используется в автоматическомдоказательстве теорем, когда проблема истинности за меняется эквивалентной проблемой выводимости, присоздании логических языков програ ммирования (Пролог и т.п.).         Проблема семантической П. логических систем (исчислений) имеет различные вариан ты: а) поисклогической системы (в частности, обладающей некоторыми требуемыми свойс твами, напр. наличиемконечной аксиоматики), полной относительно данного класса модел ей (относительно данной модели); б)поиск класса моделей (модели), относительно которо го полным является данное исчисление. Приположительном решении этих проблем решае тся и проблема поиска доказательства П. данной логическойсистемы относительно данног о класса моделей. Теорема Гёделя о П. решает один из вариантов последнейпроблемы.         Примеры проблем, а). Множество натуральных чисел N с обычными арифметическим и операциямисложения и умножения, предикатом равенства и константами 0,1 называют с тандартной модельюарифметики. Первая теорема Гёделя о неполноте (в упрощенной фор мулировке) утверждает, что несуществует эффективной, т.е. обладающей разрешимым мн ожеством аксиом и правил вывода, теории(логического исчисления), множество выводим ых утверждений которой совпадает с теорией натуральныхчисел первого порядка. С друг ой стороны, если исключить из рассмотрения умножение, то получившаясятеория, называ емая арифметикой Пресбургера, обладает аксиоматической системой с конечным списко максиом, т.е. существует эффективная логическая система (также называемая арифметик ой Пресбургера),полная относительно модели из натуральных чисел с константами 0,1, фу нкцией (операцией) сложения ипредикатом равенства. Теорема Трахтенброта утверждает,  что не существует эффективного логическогоисчисления, полного относительно класса вс ех конечных моделей (стандартная формулировка —первопорядковая теория конечных м оделей не является рекурсивно перечислимой).         Примеры проблем, б). Парадоксы наивной теории множеств привели к созданию разл ичныхаксиоматических теорий множеств. В отличие от аксиоматической арифметики, н азываемой формальнойарифметикой, теория множеств не обладает стандартной, т.е. всем и принимаемой в качестве стандартной,моделью. Положение усугубляется тем, что имеют ся многочисленные утверждения, такие как континуум­гипотеза, аксиома     выбора, которы е равнонепротиворечивы со своими отрицаниями; напр., мы можем каксиоматической тео рии множеств присоединять континуум­гипотезу (упрощенная формулировка: в каждомбе сконечном множестве действительных чисел элементов либо столько же, сколько натурал ьных чисел,либо столько же, сколько всех действительных чисел) и можем присоединятьее отрицание: если одна изполучившихся теорий непротиворечива, то непротиворечива и  другая. По аналогии с логическимиисчислениями первого порядка строятся исчисления в торого (или даже более высокого) порядка. Доказано,что эти исчисления не обладают сво йством П. относительно класса моделей формул их языка. Однакоудается доказать П. отн осительно видоизмененных моделей (относительно главных интерпретаций).Другими при мерами являются различные неклассические логики. Так, модальные и релевантные исчис лениявозникли изначально как аксиоматические и лишь десятилетия спустя для них были  предложены теориимоделей, относительно которых они полны, и рассматриваемые модел и обладают эвристической ценностью,позволяя учитывать интуицию, подразумевавшуюся  при построении исчислений.         Синтаксическая П. — П. логического исчисления относительно определенного фор мульного свойства.         Так, арифметика Пресбургера обладает кроме семантической также и синтаксическо й П.: для всякогопредложения (замкнутой формулы) А ее языка справедливо, что одна из  формул А или —А выводима варифметике Пресбургера. Из теоремы Гёделя о П. и/или из  ее доказательств следует, что всякаянепротиворечивая теория первого порядка имеет син таксически полное непротиворечивое расширение.Синтаксическая П. иногда полезна для  доказательства разрешимости теории: если теория заданаэффективно (рекурсивно или алг оритмически аксиоматизируема) и синтаксически полна, то она разрешима.Этот вид можн о переформулировать и для случая логических языков, не содержащих отрицания. Близки м кнему видом П. является П. по Посту, применяющаяся чаще всего для пропозициональн ых логик, в которыхдействует правило подстановки формул вместо переменных: логика н азывается полной по Посту, если онанепротиворечива, но всякое ее собственное расширен ие, т.е. содержащее хотя бы одну новую формулу,противоречиво. Так, классическое исчи сление высказываний полно по Посту.         К синтаксической П. относятся и различные свойства эффективности связок. Напр.,  говорят, чтологическое исчисление обладает свойством дизъюнкции (дизъюнктивным сво йством), если из того, что в немвыводима формула AvB, следует, что выводима формула  А или выводима формула В. Свойствомдизъюнкции не обладает классическое исчисление  высказываний (формула р v —,р в нем выводима, но невыводимы нир, ни —р), но обладает  интуиционистское исчисление высказываний. Кванторным вариантомсвойства дизъюнкци и является экзистенциальное свойство: если в данной логической системе выводимопредл ожение З л х р ( х ), то выводимо и предложение вида с р ( £ ), где t — некоторый не содер жащийпеременных терм. Последнее свойство используется в приложениях: если доказано  существованиенекоторого объекта, обладающего требуемым свойством, т.е. и способ пост роения этого объекта.Экзистенциальным свойством обладают многие теории, построенные на интуиционистской (конструктивной)основе. Классическое исчисление высказываний  обладает ослабленным свойством дизъюнкции — П.  (илиразумностью) по Холдену: если выводима AvB, где А и В не имеют общих переменных , то выводима покрайней мере одна из формул А или В. Этим свойством не обладают прак тически все стандартныемодальные логики, но многие из них обладают модальным свойст вом дизъюнкции: если выводима AvB, товыводима, по крайней мере, одна из формул А ил и В.         А.В. Чагров         Лит.: Кпини С.К. Введение в метаматематику. М., 1957; Чёрч А. Введение в математ ическую логику. М.,1960; Булос Дж., Джеффри Р. Вычислимость и логика. М., 1994. Теорема 16.11 (разрешимости формализованного исчисления  высказываний). Формализованное исчисление высказываний есть разрешимая  аксиоматическая теория. Доказательство. Для доказательства теоремы нужно указать алгоритм, позволяющий для  каждой формулы формализованного исчисления высказываний отвечать на вопрос, можно или нельзя вывести ее из аксиом. Такой алгоритм есть. На основании теоремы 16.6 о  полноте формализованного исчисления высказываний доказуемость формулы в  формализованном исчислении высказываний эквивалентна тождественной истинности  данной формулы в алгебре высказываний. Для проверки последнего свойства нужно  составить таблицу истинности формулы. Если последний столбец таблицы будет состоять лишь из единиц, то формула является тавтологией, а следовательно, и теоремой  формализованного исчисления высказываний. Если же там встретятся нули, то формула  — не тавтология, а значит, и не теорема.