Дискретная математика (998286), страница 19
Текст из файла (страница 19)
Таким образом, формальная теория пригодна для описания тех множеств (алгебраических систем), которые являются ее моделями. Модель для формальной теории Т существует тогда и только тогда, когда Т семантически непротиворечива. Формальная теория Т называется (вормально непротиворечивой, если в ней ие являются выводимыми одновременно формулы г и е'. Теория Т формально непротиворечива тогда и только тогда, когда она семантически непротнворечива. ОТСТУПЛЕНИЕ Последние утверждения являются доказуемыми метатеоремами, доказательства которых опускаются из-за технических сложностей. 4.2.5. Полнота, независимость и разрешимость Пусть множество М является моделью формальной теории Х Формальная теория 'Х называется полной (или адекватной), если каждому истинному высказыванию М соответствует теорема теории Т.
Если для множества (алгебраической системы) М существует формальная полная непротиворечивая теория э, то М называется аксиоматизирувмым (или Фор мализуемым). Система аксиом (или аксноматизация) формально непротиворечивой теории з называется независимой, если никакая нз аксиом не выводима из остальных по правилам вывода теории 'Х. 108 Глава 4. Логические исчисления Формальная теория Т называется разрешимой, если существует алгоритм, который для любой формулы теории определяет, является ли эта формула теоремой теории. Формальная теория Т называется полуразрвшимой, если существует алгоритм, который для любой формулы Г теории выдает ответ «ДА», если Р является теоремой теории и, может быть, не выдает никакого ответа, если Р не является теоремой (то есть алгоритм применим не ко всем формулам).
4.3. Исчисление высказываний 4.3.1. Классическое определение исчисления высказываний Исчисление высказываний — это формальная теория С, в которой: 1. Алфавит: и — » — связки; (, ) — служебные символы; а, Ь,..., ам Ьы... — пропозиииональные пврвмвнныв, 1) переменные суть формулы; 2) если А,  — формулы, то (- А) и (А » В) — формулы. А1 .. (А » (В » А)); Аз . ((А -» ( — » С)) -» ((А » В) -+ (А — » С))); Аз: (( В » А) » ((- В » А) -» В)).
А, А-кВ Молив ролелв 2. Формулы; 3. Аксиомы: 4. Правило: Здесь А и  — любые формулы. Таким образом, множество аксиом теории к. бесконечно, хотя задано тремя схемами аксиом. Множество правил вывода также бесконечно, хотя оно задано только одной схемой. ЗАМЕЧАНИЕ Латинское словосочетание вюйар ронелл обычно переводят на русский как правило сиде. При записи формул лишние скобки опускаются, если это не вызывает недоразумений. Другие связки вводятся определениями (а не аксиомами): А4сВ:= (А — к В), АМВ;=.
А-» В. Любая формула, содержащая эти связки, рассматривается как синтаксическое сокращение собственной формулы теории Х. В этом разделе дано описание формальной теории исчисления высказываний. Поскольку исчисление высказываний уже знакомо читателю по материалам разделов 3.1 и 4.1, здесь сделан сильный акцент именно на формальной технике. Знакомство с чисто механическим характером формальных выводов подготавливает рассмотрение методов автоматического доказательства теорем в разделе 4.5. 1О9 4.3. Исчисление высказываний ОТСТУПЛЕНИЕ Классическое задание теории к с помощью схем аксиом цзд любыми формулами вполне соответствуетматематической традиции (мы пишем (а+ Ь) = а +2еЬ+Ь~, подразумевая под а н Ь не только любые числа, но и любые выражения!).
В то же время зто не очень удобно для представления в ЗВМ. В следующих трех рззделзх вводится определение исчисления высказываний, более удобное для реализации на ЭВМ. 4.3.2. Частный случай формулы Если в формулу (исчисления высказываний) А вместо переменных х„...,х„ подставить соответственно формулы Вм..., В„, то получится формула В, кото- рая называется частным случаем формулы А: В: = А(..., х;,... ) (В,//хк),". Каждая формула В; подставляется вместо всех вхождений переменной хь Набор подстановок (Вь//хк),, называется унификатором, Формула С называется совместным частным случаем формул А и В, если С является частным случаем формулы А и одновременно частным случаем форму- лы В при одном и том же наборе подстановок, то есть С = А(...,х;,...) (Х;//х,)," ссС = В(...,х;,...) (Х;//х,),", Формулы, которые имеют совместный частный случай, называются унифииирув- мыми, а набор подстановок (Х,//хк),", с помощью которого получается совмест- ный частный случай унифицируемых формул, называется общим унификатором.
Наименьший возможный унификатор называется наиболее общим уншрикато- ром. Набор формул Вю..., В„называется частным случаем набора формул Аы..., А„, если каждая формула В; является частным случаем формулы А; при одном и том же наборе подстановок.
Набор формул См...,С„называется совместным частным случаем наборов формул Аы, А„и В!,..., В„, если каждая форму- ла С; является частным случаем формул А; и В; при одном и том же наборе подстановок, 4.3.3. Алгоритм унификации Если язык формул удовлетворяет определенным условиям, то можно проверить, являются ли две заданные формулы унифицируемыми, и если это так, то найти наиболее общий унификатор. В частности, это возможно для типичного языка формул, описанного в подразделе 4.3А. В следующем алгоритме предполагается, что функция / осуществляет синтаксический разбор формулы и возвращает знак. главной операции (то есть — к, или признак того, что формула является переменной), а функции ! и г возвращают левый и правый операнды главной операции, то есть подформулы (полагаем, что отрицание имеет толысо правый операнд).
Набор подстановок (унификатор) представлен в виде глобального массива Я, значениями индекса которого являются имена переменных, 11О Глава 4. Логические исчисления а значенийми элементов — формулы, которые подставляются вместо соответ- ствующих переменных, дитпритМ 4.1. АПГОрнты унифИКацИИ вЂ” рЕКурСИВНая фуНКция Онйу Вход: формулы А и В. Выход: (а)зе, если формулы не унифицируемы; сгпе и наиболее общий унификатор Я в противном случае, (г У(А) — переменная Гйеп с:=У(А) ( переменная ) В В[с] = а ГЬЕП 8[с]: = В; гегпгп Ггпе ( то есть добавляем подстановку (В//е) ) е)ве гегпгп (Я[с] ,-Ь В) ( либо эта подстановка уже есть, либо унификация невозможна ) епо К епд 1г 1т /(А) ~ /(В) спев гегпгп (а)ве ( главные операции различны — унификация невозможна епд [г 1г /(А) =' ' тпеп гетпгп \УшГу(г(А), г(В)) ( пытаемся унифицировать операнды отринаний ) епд 11 /(А) = -а спев гетпго 1)п1гу(1(А),1(В)) й 11шГу(г(А), г(В)) ( пытаемся унифицировать операнды импликаций ) епо' и ОБОСНОВАНИЕ Прн любых подстановках формул вместо переменных главная операция (связка) формулы остается неизменной.
Поэтому, если главные операции формул различны, то формулы заведомо не унифицируемы. В противном случае, то есть если главные операции совпадают, формулы унифицируемы тогда и только тогда, когда унифицируемы подформулы, являющиеся операндами главной операции. Этв рекурсия заканчивается, когда сопоставление доходит до переменных. Переменная унифицируется с любой формулой (в частности, с другой переменной) простой подстановкой этой формулы вместо переменной, По подстановки для всех вхождений одной переменной должны совпадать. П 4.3.4. Конструктивное определение исчисления высказываний Алфавит и множество формул — те же (см.
подраздел 4.3.1). Аксиомы — три конкретные формулы: Аг . '(а -+ (Ь -+ а)); Ат . '((а -+ (Ь вЂ” + с)) -+ ((а -ь Ь) -+ (а -+ с))); А1, (( Ь -+ а) -+ (( Ь -+ а) -+ Ь)). 4.3. Исчисление высказываний Правила вывода: 1. Правило подстановки: если формула В является частным случаем формулы А, то В непосредственно выводима из А, 2. Правило Мог(нз ропепз; если набор формул А, В, С является частным случаем набора формул а, а -к Ь, Ь, то формула С является непосредственно выводимой из формул А и В. ЗАМЕЧАНИЕ Здесь а, а -г Ь, Ь вЂ” зго три конкретные формулы, построенные с помощью переменных а,Ь и связки -+, Исчисление высказываний А — это достаточно богатая формальная теория, в которой выводимы многие важные теоремы.
ЗАМЕЧАНИЕ Цыводимость формул в теории Х доказывается путем предъявления конкретного вывода, то есть последовательности формул, удовлетворяющих определению, данному в разделе 4.2.2. Для удобства чтения формулы последовательности вывода выписываются друг под другом в столбик, слева указываются их номера в последовательности, а справа указывается, на каком основании формула включена в вывод (то есть она является гипотезои или получена из схемы аксиом указанной подстановкой, или получена из предшествую щих формул по указанному правилу вывода и т. д.).
ТЕОРЕМА Рг. А -ь А ТЕОРЕМА А ~-с  — г А ДОКАЗАТЕЛЬСТВО 1. А гипотеза 2, А + (В + А) Аг 3.  — ~А МР;1,2 4.3.5. Производные правила вывода ДОКАЗАТЕЛЬСТВО 1, (А -ь ((А — ь А) — г А)) 2. ((А -ь ЯА — г А) — г А)) -+ ((А — г (А -ь А)) -ь (А — г А))) 3. ((А-+ (А-+ А)) -+ (А-+ А)) 4. А-г(А-ьА) 5. А — >А Аг, '(А — г А/В) Аз, (А -+ А/В; А/С) МР; 1,2 Аг, А/В МР; 4,3 П 112 Глава 4. Логические иочиолеиив Всякую доказанную выводимость можно использовать как новое (производное) правило вывода Например, последняя доказанная выводимость называется правилом введения ииаликаиии; А + В -+ А 4.3.6.
Дедукция В теории С импликация очень тесно связана с выводимостью. ТЕОРЕМА (дедукции) Если Г,А)-с В, то Г)-с А -+ В и обратно. доказательство Туда. Пусть Ем..., ń— вывод В из Г, А. Е„= В. Иидукцией по г (1 <'2 <'и) покажем, что Г )-с А -+ Еь Тем самым теорема будет доказана. Ваза: г = 1. Возможны три случая. 1. Пусть Ег — аксиома. Тогда рассмотрим вывод Е,, Ег -к (А -+'Е,), А — > Е,. Имеем )-с А — к Еь 2.
Пусть Ег Е Г. Тогда рассмотрим вывод Ем Ьг -и (А -+ Ег), А -» Е,. Имеем Г Рс А — к Ег. 3. Пусть Е, = А. Тогда по первой теореме предыдущего раздела )-г. Е, -~ Е„ а значит Рс А-+ Е,. В любом случае Г Рс А -+ Еи Таким образом, база индукции доказана. Пусть теперь Г )-с А -+ Е; для всех Т < )г.
Рассмотрим Е». Возможны четыре случая: либо Е» — аксиома, либо Е» е Г, либо Е» = А, либо формула Е» получена по правилу Мог)из ропепз из формул Е; и Еги причем г, г < е и Е, = Е; -+ Еы Для первых трех случаев имеем Г )-с А -+ Е» аналогичным образом, Для четвертого случая по индукционному предположению имеется вывод Г Рс А -+ Е; и вывод Г )-с А -+ (Е; -+ Е»).
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
