4 - Исчисление предикатов. Построение теории P. Правила естественного вывода. Глобальные свойства теории P (Конспект лекций), страница 4

Значит, метод, которым разворачивалась невыводимая””формула может быть использован (с некоторыми модификациями) для анализа формулы наистинность. Поясним сказанное. Ставим задачу убедиться в общезначимости некоей формулыX или опровергнуть это. Последнее означает построение интерпретации, в которой эта формула ложна.

Чтобы работать только с замкнутыми формулами, можем эту формулу замкнутькванторами всеобщности. Что значит ложность X? Допустим X = X1 ∨ X2 . Тогда ложностьX равносильна ложности и X1 , и X2 . Допустим X = X1 → X2 . Тогда ложность X равносильнаистинности X1 и ложности X2 . Эти рассуждения показывают, что исходная формула разворачивается в два множества L и R более простых формул, причем все формулы в L должны бытьистинны, а все формулы в L2 ложны. Разворачивание сопровождается уменьшением логическойсложности формул, и в конце концов дело дойдет до элементарных формул. Однако при этомвозникает несколько вариантов (например, истинность U ∨ W обеспечивается истинностью Uили истинностью W ; какой из этих вариантов возможен, на этапе анализа формулы не известно; надо иметь в виду все варианты) Если при этом множества L и R будут пересекаться, томы приходим к невозможности обеспечить главное требование: истинность формул из L и ложность формул из R.

Это означает, что интерпретаций, в которых исходная формула истинна,нет. Если же пересечений нет, то можно так устроить интерпретацию предикатных символов,что основное требование будет выполняться.ÔÍ-12J Пусть общезначимая формула A не выводима в теории P . Мы можем считать, что этаформула замкнута, добавляя к ней в случае необходимости кванторные приставки. Замкнутаяформула ¬A, не являясь общезначимой, тоже не выводима в теории P . Рассмотрим формальную теорию T , которая получается из P добавлением нелогической гипотезы ¬A. Эта теориянепротиворечива, так как иначе в ней выводилась бы любая формула, в том числе и A. Другими словами, в исчислении предикатов имела бы место выводимость ¬A ` A.

Но это возможнотолько в случае, когда A — выводимая формула. Но если T — непротиворечивая теория, то онаимеет модель, т.е. такую реализацию, в которой формула ¬A истинна. В этой же реализацииформула A ложна. Следовательно, она не является общезначимой. Полученное противоречиедоказывает, что предположение о невыводимости A неверно. IÌÃÒÓÌÃÒÓТеорема 4.3. В исчислении предикатов выводима любая тавтология.ÌÃÒÓÌÃÒÓÌÃÒÓ51R. Получится следующее:> ∃x(p → q(x)) → (p → ∀xq(x))∃x(p → q(x)) > p → ∀xq(x)∃x(p → q(x)), p > ∀xq(x)p → q(a0 ), p > ∀xq(x)p → q(a0 ), p > q(a1 )p > p, q(a1 )q(a0 ), p > q(a1 )Разобранный пример можно истолковать как алгоритм проверки формулы на истинность.Это верно, но этот алгоритм не всегда приводит к ответу за конечное число шагов.ÔÍ-12ÔÍ-12Пример 4.4.

Рассмотрим формулу ¬∀x∃yp(x, y). Для нее дерево разбора имеет следующийвид:> ¬∀x∃yp(x, y)ÌÃÒÓМы видим, что в левой ветке формула p встречается и слева, и справа, и в этом случаеобеспечить истинность формул левее > и ложность правее нельзя. В то же время правая веткаобеспечивает нужную интерпретацию: предикатный символ p нулевой арности полагаем равным 1, а для q полагаем q(a0 ) = 1, q(a1 ) = 0. Таким образом, если носитель интерпретациисодержит два элемента, а предикатные символы имеют заданный смысл, формула будет ложной. Впрочем, если носитель интерпретации имеет всего лишь один элемент (а почему бы инет?), то нужное условие не удается обеспечить и в правой ветви.

Что это значит? В любоймомент в левом и правом списках формул есть формулы эквивалентные. Если две такие формулы истинны, то дизъюнкция всех правых формул истинна, т.е. истинна исходная формула.Если же обе формулы ложны, то конъюнкция левых формул ложна, откуда следует истинностьисходной формулы. Вывод: анализируемая формула истинна при любой интерпретации.ÔÍ-12ÔÍ-12ÔÍ-12ÌÃÒÓÌÃÒÓÌÃÒÓÔÍ-12ÔÍ-12ÌÃÒÓÔÍ-124. ИСЧИСЛЕНИЕ ПРЕДИКАТОВ∀x∃yp(x, y) >∃yp(c0 , y), ∀x∃yp(x, y) >p(c0 , c1 ), ∀x∃yp(x, y) >......................При разборке квантора всеобщности мы выбираем первую не реализованную для этого квантора константу, а при разборке квантора существования — первую свободную константу.

Дляпостроения контрпримера есть два варианта. Можно в очередной момент вместо свободнойконстанты использовать прежнюю (считать, что новых констант уже нет), например, считать,что c2 = c1 . Тогда истинность формул p(c0 , c1 ) и p(c1 , c1 ) в интерпретации с двумя элементамиc1 и c2 будет означать и истинность формулы ∀x∃yp(x, y). Мы получаем контрпример, т.е.интерпретацию, в которой анализируемая формула ¬∀x∃yp(x, y) является ложной. Возможен идругой вариант — счетный набор констант.

Мы получаем набор формул p(ck , ck+1 ), которыеобъявляем истинными. Считая, что других констант нет, делаем заключение об истинностиформулы ∀x∃yp(x, y) и ложности формулы ¬∀x∃yp(x, y). Мы снова получили контрпример, ноуже со счетным носителем интерпретации.ÔÍ-12ÌÃÒÓÔÍ-12ÌÃÒÓÔÍ-12ÔÍ-12p(c0 , c1 ), p(c1 , c2 ), ∀x∃yp(x, y) >ÌÃÒÓÌÃÒÓp(c0 , c1 ), ∃yp(c1 , y), ∀x∃yp(x, y) >ÌÃÒÓÔÍ-12ÌÃÒÓ52Однако, если бы проверяемая формула была тавтологией, мы должны были бы рассмотретьоба этих варианта, за конечное число шагов установить истинность формулы нам бы не удалось.ÔÍ-12ÔÍ-12ÌÃÒÓÌÃÒÓÔÍ-12ÔÍ-12ÌÃÒÓÌÃÒÓÔÍ-12Процесс расшифровки“, предпринятый в разобранном примере очень похож на построение”вывода в рамках правил естественного вывода, но с одним уточнением.

В секвенциях исчисления предикатов справа могла быть только одна формула, в то время как в разобранном примереи слева, и справа находятся списки формул.Приведенное построение, а также теория N , в которой дело свелось к манипуляциям ссеквенциями, приводит к идее построить совсем другое исчисление, основанное на понятиисеквенции. Такое исчисление называют исчислением генценовского типа в противовесисчислениям N и P , которые относят к исчислениям гильбертовского типа.ÌÃÒÓÌÃÒÓÌÃÒÓÔÍ-12ÔÍ-12ÌÃÒÓÔÍ-124.

ИСЧИСЛЕНИЕ ПРЕДИКАТОВÔÍ-12ÌÃÒÓÔÍ-12ÌÃÒÓÔÍ-12ÌÃÒÓÌÃÒÓ141416213. Алгебра предикатов3.1. Предикаты и кванторы . . . . . . . . . . .3.2. Логико-математические языки . . . . . . .3.3. Переименования и подстановки . . . . . .3.4. Семантика логико-математического языка3.5. Логические законы . . .

. . . . . . . . . .3.6. Замены . . . . . . . . . . . . . . . . . . . .3.7. Упрощение формул . . . . . . . . . . . . ........26262730333538404. Исчисление предикатов4.1. Построение теории P . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

. . . . . .4.2. Правила естественного вывода . . . . . . . . . . . . . . . . . . . . . . . . . . . . .4.3. Глобальные свойства теории P . . . . . . . . . . . . . . . . . . . . . . . . . . . . .434344465. Генценовские формальные системы5.1. Исчисление GV . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

.5.2. Исчисление GP . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .5454586. Примеры формальных теорий6.1. Теория групп . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .6.2. Формальная арифметика . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

.6161637. Метод резолюций7.1. Скулемовские функции . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .7.2. Метод резолюций для исчисления высказываний . . . . . . . . . . . . . . . . . . .7.3. Метод резолюций для исчисления предикатов . . . . .

. . . . . . . . . . . . . . . .68687073......................................................................................................................................................................................................................................................ÌÃÒÓ2. Исчисление высказываний2.1. Основные положения теории N . . .

. . . . . . . . . . . . . . . . . . . . . . . . . .2.2. Правила естественного вывода . . . . . . . . . . . . . . . . . . . . . . . . . . . . .2.3. Глобальные свойства теории N . . . . . . . . . . . . . . . . . . . . . . . . . . . . .....ÔÍ-12....11359ÔÍ-12ÔÍ-121. Алгебра высказываний1.1. Введение . .

. . . . . . . . . . . . . . .1.2. Алгебра логики . . . . . . . . . . . . .1.3. Тавтологии и эквивалентность формул1.4. Функции алгебры логики . . . . . . . .ÔÍ-1253ÌÃÒÓÔÍ-12ОГЛАВЛЕНИЕÌÃÒÓÌÃÒÓÌÃÒÓÔÍ-12ÔÍ-12ÔÍ-12ÌÃÒÓÌÃÒÓÌÃÒÓÔÍ-12ÔÍ-12ÔÍ-12ÌÃÒÓÌÃÒÓÔÍ-12ÌÃÒÓ.