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

1 Теорема полноты для исчисления высказываний.

Аксиомы:

1)Ф (ΨФ)

2)[Ф (ΨƟ)] [( ΨY) ( ΨƟ)]

3)[┐Ф Ψ] [( ┐Ф Ψ)Ф]

MP

├ Ф если существует послед-то формул.

И каждая Ψi имеет вид асиомы либо

Ψi =MP(Ф, Ф)где α,K<i

Если Г множество формул Г ˫ Ф если существует последовательность формул Ф1 ,Ф2 , … Фn =Ф

И каждая Фявляется либо доказуемой формулой либо

Фi =MP(Фj, Фk)где j, k<I либо Ψi € Г

˫ АА

Лемма 2

А

A

2 Система аксиом для исчисления предикатов.

Формула А называется следствием множества формул Г и У тогда и только тогда когда существует такая последовательность формул А1 …Аn что Аn есть А и для любого i Аi есть либо аксиома либо элемент Г, либо непосредственное следствие некоторых предыдущих формул по одному из правил вывода. Для сокращения утверждения А есть следсвие Г мы будем упоиреблять запись Г ˫ А. Если множество Г конечно:Г={B1 …Bn}то вместо{B1 …Bn}├А мы будем писать B1 …Bn├А

Приведем несколько простых свойств понятия выводимости из посылок.

1)Если Г⊆∆ и Г ├ А то ∆ ├ А

2)Г├ А тогда и только тогда когда в Г существует конечное подмножество ∆ для которого ∆ ├ А

3)Если ∆ ├ А и Г ├ В для любого В из множества ∆ то

Г ├ А

Мы введем теперь формальную аксиоматическую теорию

L для исчисления высказываний

1)Символами L являются ┐ ﬤ (,)м буквы Аi с целыми положительными числами в качестве индексов:А1 А2 …

2)Все пропозиционные буквы суть формулы

Если А и В-формулы то (┐А)и(А Вﬤ)тоже формулы

3)Каковы ьы ни были формулы А, В и b теории L следующие формулы суть аксиомы L

(А1) (А ⊃(В ⊃А))

(А2) ((А⊃(В⊃b)) ⊃((A⊃B) ⊃(A⊃b)))

(A3) ((┐B⊃┐A) ⊃ ((┐B⊃A) ⊃B))

4)Единсвенным правилом вывода служит правило modus ponens. В есть непосредсвенное следсвие А и А⊃В

Это правило будем сокращенно обозначать через MP

Введем остальные связки для с помощью следующих определений

D1) (A&B)означает ┐(А⊃┐B)

D2) (A˅B)означает (┐А) ⊃В

D3) (A𝞝B) означает (А ⊃В)&(В⊃А)

Лемма:1.7

├L A⊃A для любой формулы А

Доказ. построим вывод формулы A⊃A в L

1)  (A⊃((A⊃A) ⊃A)) ⊃((A⊃(A⊃A)) ⊃(A⊃A))

Подстановка в схему аксиом (А2)

2)  А⊃((А⊃А) ⊃А схема аксиом (А1)

3)  (А⊃(А⊃А)) ⊃(А⊃А) из (1)(2) по MP

4)  А⊃(А⊃А) схема аксиом (А1)

5)  А⊃А из (3) (4) по MP

3 Правила вывода в исчислении предикатов.

Имеется конечное множество R1…Rn отношений между формулами называемых правилами вывода. Для каждого Ri существует целоеположительное j такое что для каждого множества состоящего из j формул и для каждой формулы А эффективно решается вопрос о томнаходится ли данные j формул в отношении Ri с формулой А и если да то А называется непосредсвенным следствием данных jформул

Выводом в Y называется всякая последовательность

A1…An формул такая что для любого i формула Аi есть либо аксиома теории Y либо непосредсвенное следствие каких либо предыдущих формул по одному из правил вывода.

Понятие выводимости из посылок

1)Если Г ⊆∆ и Г├А то ∆├А

2) Г├А тогда и только тогда когда в Г существует конечное подмножество ∆ для которого ∆├А

3)Если ∆├А и Г├В для любого В из множества ∆ то Г├А

Свойсво 1 выражает тот факт что если А выводимо из множества посылок Г то оно остается выводимым если мы добавим к Г новые посылки. Часть “тогда” утверждения (2)вытекает из (1)

4 Равносильность формул. Равносильные формулы в исчислении предикатов

5 Доказательство общезначимости доказуемых формул исчисления высказываний

Формула А называется логически общезначимой если она истинна в каждой интерпритации

Очевидно что формула А логически общезначима тогда и только тогда когда формула ┐А не является выполнимой и формула А выполнима тогда и только тогда когда формула

┐А не является логически общезначимой

Из этих определений непосредсвенно вытекают следующие уиверждения

1)Формула А логически влечет формулу Втогда и только тогда когда А⊃В логическм общезначима

2)Формула А и В логически эквивалентны тогда и только тогда когда формула A𝞝B логически общизначима

3)Если формула А логически влечет формулу В и А истенно в данной интерпритации то в этой же интерпритацииистинно и В

Пример:Всякий часный случай тавтологии логически общезначим

Если А не содержит x свободно то ⩝x(А ⊃В)М(А⊃⩝xВ)логически общизначимо

Если t свободен для x в А то ⩝xА(x) ⊃А(t) логически общизначимо