Intel_Nils (526801), страница 37
Текст из файла (страница 37)
Итак, каждая п. п. формула в нашем множестве будет предложением. Наша п.п. формула теперь представлена в виде следующих предложений: Р(х) ~/ Р(у) ~/ Р(7(х, у)), Р (х) ~г Я (х, д (х)), Р(х) 1/ Р(д(х)). Заметим, что в литералах предложения могут содержаться переменные, которые всегда следует считать относящимися 'к кванторам всеобщности. Если вместо переменных литерала ') См. примечание на стр.
181. — Прим. перев. б.7, Уныоерсум Эрбрана 188 подставляются выражения, не содержащие переменных, то мы получаем так называемый константный частный случай этого литерала. Так, Я(а, ~(й(Ь)) ) — константный частный случай п. и. формулы Я(х, у). Наш процесс, предназначенный для демонстрации того, что некоторое множество 5 п.
п. формул неудовлетворимо (невыполнимо), начинается с превращения каждой п. п. формулы нз 5 в предложения. В результате возникает некоторое множество 5 предложений. Можно показать, что если множество 5 неудовлетворимо, то неудовлетворимо и множество 5', и обратно, нз неудовлетворимости 5' вытекает неудовлетворимость 5. В оставшейся части этой главы мы изложим методы, позволяющие показать, что некоторое неудовлетворимое множество предложений действительно неудовлетворимо. Эти методы носят вполне общий характер, поскольку любое множество правильно построенных формул можно представить в виде предложений.
8.7. УНИВЕРСУМ ЭРБРАНА Рассмотрим неудовлетворимое конечное множество 5 предложений. Для того чтобы убедиться в неудовлетворимости 5, нужно показать, что не существует интерпретации, которая ему удовлетворяет. Задавая для 5 интерпретацию, следует прежде определить область В, а затем связать с каждым константным символом в 5 некоторый элемент из 0 и с каждым функциональным символом в 5 некоторую функцию на 11 и т. д. Очевидно, что для демонстрации того, что каждая получающаяся в результате интерпретация не удовлетворяет 5, мы не в состоянии перечислять всевозможные области и такие связи. Но можно указать такой адекватный список имен для элементов области, что если не существует удовлетворяющей интерпретации в областях, элементы которых могут быть названы именами нз нашего списка, то не существует удовлетворяющей интерпретации вообше.
Одним из таких списков имен, адекватным множеству предложений 5, является универсум Эрбрана для 5. Универсум Эрбрана Н(5) для множества предложений 5 определяетси рекурсивно следующим образом: 1. Множество всех константных букв ~)ч), упомянутых в 5, принадлежит Н(5). Если Я) пусто, то Н(5) содержит некоторую произвольную константную букву, скажем а. 2.
Если термы Гь ..., 1„принадлежат Н(5), то Н(5) принадлежит также н 7,"(гн Г,, ...„г„), где )," — любаЯ фУнкциональная буква, упомянутая в 5. 3. Никаких других термов в Н(5) нет. !86 Гм 6. Т(окаввтельство теорем в исчислении иредикатов Должно быть ясно, что независимо от выбора интерпретации при приписывании значений Т и Р литералам из 5 никаких других имен для элементов области никогда не потребуется. В этом смысле Н(5) — наиболее общая область; если мы покажем, что множество 5 неудовлетворимо в области Н(5), то можно бцть уверенным, что оно неудовлетворимо в любой области.
Универсум Эрбрана, вообще говоря, бесконечен, но счетен, так что его члены всегда можно тем или иным образом упорядочить. Например, рассмотрим множество предложений 5: (Р(х) 1I ()(а) ~Т Р(г'(х)), чс(Ь) ~/ Р(йс(х, у))). Здесь константные термы — (а, Ь), а функции — Д,д). Таким образом, Н(5) представляет собой (счетное) бесконечное множество (а, Ь, г'(а), г (Ь), д(а, а), я (а, Ь), й(Ь, а), й (Ь, Ь), г'()(а)), г'(7(Ь)), йс(а, г'(а)), ...). 6.8. ЗтБРАНОВСКАЯ БАЗА Когда мы задаем интерпретацию (на Н(5)) для предложения в 5, его атомным формулам приписываются значения (Т или Р).
Предположим, что Р есть и-местная предикатная буква в 5, Означивание атомной формулы Р(хь х,, ..., х ) производится приписыванием значений Т и Р независимо для всех ее константных частных случаев„, получающихся в результате подстановки элементов из Н(5) вместо переменных хь хм ..., х . Разумеется, число константных частных случаев для каждой атомной формулы в 5 может оказаться бесконечно большим„ так что таким способом можно бесконечно долго решать задачу означивания. Но замечательно, что, прежде чем будет закончено означивание каждой атомной формулы в 5, станет совершенно очевидным, что никакая интерпретация не может удовлетворить 5, и это будет несмотря на то, что даже еще не всем константным частным случаям приписаны значения истинности! Эрбрановской базой для 5 называется множество всех константных частных случаев для всех атомных формул в 5 при условии, что для наименования элементов области использован универсум Эрбрана.
Элементы эрбрановской базы называются' атомами. Очевидно, что задание интерпретации на Н(5) закаичивается для всех предложений из 5 только тогда, когда каждому атому эрбрановской базы приписано значение истинности. Эрбрановская база также является счетной, и, следовательно, ее элементы можно тем или иным образом упорядочить. Пусть упорядоченная эрбрановская база для 5 записана в виде последовательности (рь ре, рв,...).
6.9. Построение семантического дерева 69. ПОСТРОЕНИЕ СЕМАНТИЧЕСКОГО ДЕРЕВА Семантическое дерево представляет собой бинарное дерево'), простирающееся вниз от корневой вершины. В соответствии со способом, который мы выбрали для приписывания значений истинности атомам р; зрбрановской базы, мы будем спускаться по .этому дереву по определенному пути. Если мы присвоим атому рг значение Т, то окажемся непосредственно под корневой вершиной слева, а если Р, то справа. Далее, независимо от того, в какой из двух вершин, расположенных непосредственно под корневой вершиной, мы оказались, если мы присвоим атому рх значение Т, то пойдем из нее по левой ветви, а если Р, то по правой.
Этот процесс продолжается до тех пор, пока каждому элементу эрбрановской базы не будет присвоено значение истинности. Очевидно, что в случае бесконечной эрбрановской базы любой полной интерпретации будет соответствовать бесконечный путь вниз по вершинам этого дерева. Полное дерево, содержащее все возможные пути, представляет все возможные интерпретации предложений из 5; отсюда и название: семантическое дерево. В качестве примера рассмотрим неудовлетворимое множество 5 предложений Р(х) '1/ Я(у), Р (а), Я (Ь). Универсумом Эрбрана будет здесь конечное множество гу (5) = (а, Ь). Эрбрановская база также конечна. Ее можно упорядочить так1 (Р(и), 1ч (и), Р(Ь), Я (Ь)).
Семантическое дерево для этого множества предложений конечно, оно показано на рис. 6.1. Каждое ребро, соединяющее вершину с одной из ее дочерних вершин, представляет решение, принятое относительно значения истинности одного из атомов эрбрановской базы. Условились записывать рядом с ребром, где атому присваивается значение Т, сам этот атом, а рядом с ребром, где атому присваивается значение Є— его отрицание.
Каждый из путей, ведущих от корневой вершины к концевой вершине этого дерева (а именно к вершине, расположенной внизу этого дерева), дает одну нз интерпретаций для множества 5. Эту интерпретацию можно однозначно представить в ') Каждая вершина бинарного дерева имеет ровно две дочерние вершины, если таковые у нее вообще имештси. Можно обобщить определение семантаческого дерева так, чтобы допускалось более двух таких вершин. 1 88 Г*. 6. доказательство теорем в исчислении предикатов 1 2 Р и с.
8.!. Семантическое дерево для множества нредложени А (Р(х) Ч 1С(у), Р(а), Я (Ь). виде множества атомов, встречавшихся на этом пути. Так, интерпретация, . уч , пол ающаяся при прослеживании пути от корне- а ис. 6.1 и вой вершины к концевой вершине, отмеченной на рис.. цифрой 1, задается множеством М,=(Р(а), Я(а), -Р(Ь), Я(Ь)). був. Неблагоприятные вершины !вэ Такое множество называют моделью для данного множества предложений. Говорят, что модель не удовлетворяет предложению, если существует константный частный случай этого предложения (построенный на термах универсума Эрбрана), имеющий значение Р при означиваниях, определяемых этой моделью.
Так, М, не удовлетворяет ни одному из предложений Р(а) и ° Я(Ь).Аналогично Мя = ( Р(а), 1,!(а), Р(Ь), !!(Ь)) не удовлетворяет предложению Р(х)'I 1,1(у), так как константный частный случай Р(а) ~l 11(Ь) имеет значение Р. Если в 5 есть предложение, не удовлетворшощееся интерпретацией, или моделью, то эта модель не может удовлетворить 5. Так, М, и Мя не удовлетворяют множеству 5 нашего примера, более того, можно исключить по очереди каждую из 16 возможных интерпретаций и сделать вывод, что множество5 нашего примера неудовлетворимо. 8.!О.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
