Студопедия

КАТЕГОРИИ:


Архитектура-(3434)Астрономия-(809)Биология-(7483)Биотехнологии-(1457)Военное дело-(14632)Высокие технологии-(1363)География-(913)Геология-(1438)Государство-(451)Демография-(1065)Дом-(47672)Журналистика и СМИ-(912)Изобретательство-(14524)Иностранные языки-(4268)Информатика-(17799)Искусство-(1338)История-(13644)Компьютеры-(11121)Косметика-(55)Кулинария-(373)Культура-(8427)Лингвистика-(374)Литература-(1642)Маркетинг-(23702)Математика-(16968)Машиностроение-(1700)Медицина-(12668)Менеджмент-(24684)Механика-(15423)Науковедение-(506)Образование-(11852)Охрана труда-(3308)Педагогика-(5571)Полиграфия-(1312)Политика-(7869)Право-(5454)Приборостроение-(1369)Программирование-(2801)Производство-(97182)Промышленность-(8706)Психология-(18388)Религия-(3217)Связь-(10668)Сельское хозяйство-(299)Социология-(6455)Спорт-(42831)Строительство-(4793)Торговля-(5050)Транспорт-(2929)Туризм-(1568)Физика-(3942)Философия-(17015)Финансы-(26596)Химия-(22929)Экология-(12095)Экономика-(9961)Электроника-(8441)Электротехника-(4623)Энергетика-(12629)Юриспруденция-(1492)Ядерная техника-(1748)

Исключающие кванторы




Формализация доказательства.

1) Множество очевидных утверждений.

2) Правила логического вывода (разветвляющие и не разветвляющие)

Сказать про исключающие кванторы.

Задача из «Г следует А?» превращается в «из Г и не А следует тождественная ложь»

 

Пример 1. Выясним, является ли предложение $ z [ S (z) & P (z)] логическим следствием предложений " x [ P (x) → M (x)] и $ y [ S (y) & M (y)]?

 

1 $ y [ S (y) & M (y)] первая посылка

2 " x [ P (x) → M (x)] вторая посылка

3 $ z [ S (z) & P (z)] отрицание заключения

4 [ S (a) & M (a)] из (1)

5 [ P (a) → M (a)] из (2)

6 (" x|a)[ P (x) → M (x)] из (2)

7 " z [ S (z) & P (z)] из (3)

8 S (a) из (4)

9 M (a) из (4)

______↓___________

↓ ↓

10.1 P (a) 10.2 M (a) из (5)

11.1 [ S (a)& P (a)] из (7)

12.1 (" z|a) [ S (z)& P (z)] из (7)

______↓_______________

↓ ↓

12.1.1 S (a) 12.1.2 P (a) из (11.1)

12.1.3 P (a) из (12.1.2)


 

Выражения вида (" x | y 1, y 2,..., yk) и ($ x | y 1, y 2,..., yk) будем называть исключающими кванторами общности и существования соответственно.

Истинностные значения этих формул считаем соответственно равными истинностным значениям формул " x [(xy 1) & (xy 2) &... & (xyk) → A ], $ x [(xy 1) & (xy 2) &... & (xyk) & A ].

Формулу будем называть Γ -формулой, если в списке исключений каждого квантора находятся все свободные переменные, расположенные в его области действия.

Заметим, что любая формула A из Form (σ) логически равносильна некоторой Γ -формуле. Чтобы по формуле A построить логически равносильную ей Γ -формулу достаточно воспользоваться соотношениями x A ≡ (" x | y 1, y 2,..., yk) A & Ax [ yi ], x A ≡ ($ x | y 1, y 2,..., yk) A Ú Ax [ yi ],

где y 1, y 2,..., yk - список переменных, совпадающий со списком свободных переменных формулы A, а Ax [ yi ] - формула, полученная из формулы A заменой свободных вхождений переменной x на yi.

Пример. Формула " x $ y R (x, y), где R - двухместный предикатный символ, логически равносильна Γ -формуле (" x) [($ y | x) R (x, yR (x, x)].

 


 

Ветвь назовем блокированной, если она содержит некоторую формулу B и ее отрицание B.

Определение поискового дерева для утверждения Γ Þ A дадим с помощью правил его построения.

(П1) Дерево, состоящее из одного узла, помеченного формулой A, и всех формул из Г, является поисковым деревом. Все узлы этого дерева считаем неиспользованным.

(П2) Если в дереве есть неиспользованный узел v, которому приписана формула, являющаяся посылкой одного из правил вывода, то с помощью этого правила каждая неблокированная ветвь W, проходящая через узел v, расширяется следующим образом:

· если правило разветвляющее, то из концевого узла ветви W проводятся две дуги, оканчивающиеся новыми вершинами, которым приписываются формулы-заключения данного правила;

· если правило, соответствующее узлу v, - не разветвляющее, то к концевому узлу ветви W присоединяются последовательно один к другому новые узлы, помеченные формулами-заключениями.

Уточнения требуют случаи применения правил (") и ($), поскольку они связаны с выбором параметра a. При использовании правила (") в качестве a выбирается параметр с наименьшим номером, не входящий в список исключений в посылке данного правила. При использовании правила ($) выбирается параметр с наименьшим номером, не встречающийся в расширяемой ветви, в том числе и в списке α. После расширения дерева считаем узел v использованным, а вновь построенные узлы – неиспользованными.

Очевидно, с помощью правил П1-П3 поисковое дерево для утверждения Γ Þ A определяется неоднозначно. Любую последовательность построенных деревьев будем называть поисковой. Если она бесконечна, то также будем называть поисковым деревом.

Лемма (о поисковых последовательностях). Пусть T 1, T 2,... - последовательность поисковых деревьев для утверждения Γ Þ A и Di - множество параметров, используемых в дереве Ti, i = 1, 2,.... Если существует интерпретация I сигнатуры σ на универсуме U, в которой истинны все формулы из множества Γ и формула A, то для каждого i = 1, 2,... существует интерпретация Ii сигнатуры σ È Di, такая, что в Ti есть ветвь, все формулы которой истинны в интерпретации Ii.

[Если из Г не следует А, то на любом шаге алгоритма существует ветвь дерева и интерпритация, в которой истинны все формулы ветви]

Доказательство. Для i = 1 утверждение леммы очевидно. Пусть существует интерпретация Ii -1 сигнатуры σ È Di -1, являющаяся расширением интерпретации I, такая, что в Ti -1 есть ветвь W, все формулы которой истинны в Ii -1, и пусть Ti получено из Ti -1 применением некоторого правила вывода к узлу v.

Если v Ï W, то ветвь W будет искомой ветвью и в дереве Ti. При этом интерпретация символов из множества Di \ Di -1, если такие есть, может быть произвольной.

Пусть теперь v Î W. Если v имеет вид (" x | α) C, и Di = Di -1, то формулы, присоединяемые к концевой вершине ветви в соответствии с правилом вывода, будут истинны в интерпретации Ii = Ii -1. Если же Di получено из Di -1 добавлением нового параметра an, то берем в качестве an ( I ) произвольный элемент из U, тогда присоединяемые к W формулы Cx [ an ] и (" x | α, an) C будут истинными в полученной интерпретации Ii.

Пусть теперь v имеет вид ($ x | α) C и при этом Di получено из Di -1 добавлением параметра an. Поскольку формула ($ x | α) C истинна в интерпретации Ii -1, то существует интерпретация I', совпадающая с Ii -1 всюду, кроме, возможно, переменной x, такая, что C ( I’ ) = 1. Положим an ( I ) = x ( I’ ), и тогда присоединяемая к W формула Cx [ an ] будет истинной в Ii. Рассмотрение остальных способов расширения дерева предоставляем читателю.

Ветвь назовем блокированной, если она содержит некоторую формулу B и ее отрицание B.

Определение поискового дерева для утверждения Γ Þ A дадим с помощью правил его построения.

(П1) Дерево, состоящее из одного узла, помеченного формулой A, и всех формул из Г, является поисковым деревом. Все узлы этого дерева считаем неиспользованным.

(П2) Если в дереве есть неиспользованный узел v, которому приписана формула, являющаяся посылкой одного из правил вывода, то с помощью этого правила каждая неблокированная ветвь W, проходящая через узел v, расширяется следующим образом:

· если правило разветвляющее, то из концевого узла ветви W проводятся две дуги, оканчивающиеся новыми вершинами, которым приписываются формулы-заключения данного правила;

· если правило, соответствующее узлу v, - не разветвляющее, то к концевому узлу ветви W присоединяются последовательно один к другому новые узлы, помеченные формулами-заключениями.

Уточнения требуют случаи применения правил (") и ($), поскольку они связаны с выбором параметра a. При использовании правила (") в качестве a выбирается параметр с наименьшим номером, не входящий в список исключений в посылке данного правила. При использовании правила ($) выбирается параметр с наименьшим номером, не встречающийся в расширяемой ветви, в том числе и в списке α. После расширения дерева считаем узел v использованным, а вновь построенные узлы – неиспользованными.

Очевидно, с помощью правил П1-П3 поисковое дерево для утверждения Γ Þ A определяется неоднозначно. Любую последовательность построенных деревьев будем называть поисковой. Если она бесконечна, то также будем называть поисковым деревом.

Если все ветви поискового дерева, построенного для Γ Þ A, блокированы, то такое дерево называется доказательством (в виде дерева) формулы A из посылок (гипотез) Γ.

Если для утверждения Γ Þ A существует дерево-доказательство, то будем говорить, что формула A выводима из множества гипотез Γ, и обозначать Γ |- A.

Теорема (о корректности дедуктики). Если Γ |- A, то Γ Þ A.

Доказательство. Пусть Γ |- A и T - соответствующее дерево-доказательство. Если бы A логически не следовала из Γ, то существовала бы интерпретация I сигнатуры σ, в которой были бы истинны все формулы из множества Γ и формула A. Но тогда по лемме о поисковой последовательности существовала бы ветвь в дереве T, все формулы которой были бы истинны в некотором расширении интерпретации I, что противоречит тому, что в T все ветви блокированы. Теорема доказана.


 

Ветвь W называется насыщенной относительно множества D' Í D, если:

· вместе с любой посылкой любого разветвляющего правила она содержит хотя бы одну заключительную формулу данного правила,

· вместе с любой посылкой неразветвляющего правила она содержит все заключительные формулы данного правила,

· она содержит каждую формулу из множества Γ.

Уточнения, как и прежде, требуют правила (") и ($). Если формула (" x | α) C принадлежитветви W, то для любого a Î D' формула Cx [ a ] также ей принадлежит; если формула ($x| α) C принадлежит W, то, по крайней мере, для одного a Î D' формула Cx [ a ] принадлежит W.

Поисковое дерево называется полным относительно множества параметров D', если любая его ветвь либо насыщена относительно D', либо блокирована.

Лемма (о существовании полного дерева). Для любого утверждения вида Γ Þ A существует полное поисковое дерево.

Доказательство. Уточним правила построения поисковых деревьев следующим образом. В правиле П2 в качестве v будем выбирать узел минимальной глубины, удовлетворяющий остальным требованиям. Если хотя бы одно из правил П2 и П3 применимо, то обязательно его применяем.

Используя уточненные правила, либо через конечное число шагов получим дерево, в котором каждая ветвь блокирована или насыщена, либо процесс будет продолжаться бесконечно. В последнем случае объединение , где - дерево, полученное на i-ом шаге, будет искомым деревом, в котором каждая бесконечная ветвь будет насыщенной, а каждая конечная будет блокированной или насыщенной.


 

Теорема (о полноте дедуктики). Если Γ Þ A, то Γ |- A.

Доказательство. Пусть формула A не выводима из множества Γ, тогда полное дерево T для утверждения Γ Þ A содержит, по крайней мере, одну неблокированную насыщенную ветвь W. Пусть D' - список параметров, входящих в эту ветвь (он может быть как конечным, так и бесконечным).

Рассмотрим D' в качестве универсума и зададим интерпретацию I сигнатуры σ на D' следующим образом. Для k -местного предикатного символа R Î σ положим

 

R ( I )={(a 1, a 2, …, a k)| «R (a 1, a 2, …, a k)»Î W }.

 

Легко доказать индукцией по построению формулы, учитывая правила построения дерева, что при такой интерпретации все формулы, входящие в ветвь W, будут истинными. В том числе будут истинны все формулы из множества Γ и формула Ø A, следовательно, A логически не следует из Γ.

Объединяя теоремы о корректности и полноте, получим следующую теорему.

Теорема (об адекватности дедуктики). Γ Þ A тогда и только тогда, когда Γ |- A.

Теорема (о компактности). Если Γ Þ A, то существует конечное подмножество Γ' Í Γ такое, что Γ' Þ A.

Действительно, пусть Γ Þ A, тогда по теореме о полноте Γ |- A, следовательно, существует дерево-доказательство, в котором все ветви блокированы и, следовательно, конечны. Следовательно, число гипотез из Γ, содержащихся на этих ветвях, конечно, они и образуют требуемое конечное подмножество гипотез.




Поделиться с друзьями:


Дата добавления: 2015-08-31; Просмотров: 817; Нарушение авторских прав?; Мы поможем в написании вашей работы!


Нам важно ваше мнение! Был ли полезен опубликованный материал? Да | Нет



studopedia.su - Студопедия (2013 - 2024) год. Все материалы представленные на сайте исключительно с целью ознакомления читателями и не преследуют коммерческих целей или нарушение авторских прав! Последнее добавление




Генерация страницы за: 0.038 сек.