Алфавит, формулы, система аксиом схем и правило вывода исчисления высказываний.

ИСЧИСЛЕНИЕ ВЫСКАЗЫВАНИЙ

Алфавит, формулы, система аксиом схем и правило вывода исчисления высказываний.

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

Алфавит и определение формулы – те же что и в алгебре высказываний. Но буквам алфавита не приписывается никакой смысл, - это просто символы, которые можно распознавать и различать.

В алгебре высказываний мы описали класс общезначимые формул, выражающих законы логики на основе понятия истинностного значения. Здесь же законы логики – множество доказуемых формул – они описываются по-другому. Некоторые формулы принимаются в качестве “аксиом”, а для получения новых формул вводится некоторое “правило вывода”. Позже рассмотрим, что обе формулировки логики высказываний – алгебра высказываний и теория L – дают эквивалентные результаты.

Определение 1.14

Аксиомами теории L называются веские формулы, которые порождают нижеследующие формульные схемы при любом выборе формул A,B,C:

1.

2.

3.

4.

5.

6.

7.

8.

9.

10.

11.

12.

13.

Каждая из схем (1)-(13) порождает счетное множество аксиом, если символы A, B, C заменять конкретными формулами. Поэтому записи (1)-(13) будем называть аксиомными схемами (AC).

Схемы (1)-(13) совпадают с первыми тринадцать формульными схемами предложения 1.6.

Определение 1.15

Правила вывода теории L называют процедуру перехода от двух формул вида A и к одной формуле вида B для любых A и B. Это правило называется modus pondus, MP. Правило MP называют также правилом удаления импликант и обозначают УИ. Формулы A и называют посылками, а B – заключением правила MP.

Формальное доказательство и формальный вывод.

Определение 1.16

Формальным доказательством (в теории L) называется конечная последовательность формул , причем каждая формула этой последовательности либо аксиома, либо получена по правилу MP из каких-либо двух предшествующих формул этой последовательности. Формальное доказательство является доказательством своей последней формулы . Формула B называется формально доказуемой, или формальной (теории L), если она имеет формальное доказательство.

Утверждение “Формула B формально доказуема в теории L” обозначается .

Введем соглашения:

a) Индекс L опускать;

b) Говорить «формальное доказательство», «формально доказуема», «формальная теорема» - доказательство «доказуема», «теорема».

Пример 1

Установить, что

1. 1. AC2 C=A,

2. 2. AC1

3. 3. MP(2, 1)

4. 4. AC1

5. 5.MP(4, 3)

Пояснение AC2 A, , B, C означает, что записано AC2, в которой формула С заменила формулой А, а формула В – формулой , пояснение MP(2, 1) означает, что формула получена в результате применения правила MP к формулам с номерами 2 и 1.

Следует заметить, что в проверенном доказательстве каждая из пяти формул. Является теоремой, в том числе и выписывание первые две аксиомы: доказательство любой аксиомы состоит из этой аксиомы.

Определение 1.17

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

1. или одна из посылок ;

2. или аксиома;

3. или формула, полученная из некоторых двух предшествующих формул этой последовательности по правилу MP.

Если формальный вывод B из формул , то формула B называется формально выводимой из формул и обозначается: , или , где .

Очевидно, что доказательство – частный случай формального вывода из пустого множества посылок.

Введем соглашение: вместо «формальный вывод», «формально-выводима» будем говорить «вывод», «выводима».

В определениях 1.16 и 1.17 употребляемые термины «формальное доказательство», «формально доказуема», «формальный вывод», «формально-выводима» для явного указания на то, что эти доказательства и выводы строятся в предметной языки. Используемые слева от доказательства или вывода нумерация и справа от доказательства или вывода пояснения уже относится к метаязыку.

Пример 2

Установить, что , .

1. 1. Посылка

2. 2. Посылка

3. 3. AC4

4. 4.MP (2, 3)

5. 5. AC5

6. 6. MP (2, 5)

7. 7. MP (4, 1)

8. 8. MP (6, 7)

9. , 9. ОФВ- определение формального вывода (1-8)

Запись 9 подытоживает формальный вывод формулы С из формул , . Запись 9 сделана на метаязыке.

Метатеорема 1(МТ1).

a) .

b) Если и , то

Доказательство

a) Для построения вывода формула из формул достаточно записать последовательно все формулы (в произвольном порядке), поместив последней формулу .

b) Заменив в данном выводе формулы С из формул формулы их данными выводами из формул .

Метатеорема 2 (МТ2).

Пусть Г – любое множество формул.

Тогда:

a) Если Г , то Г, В частности

b) Если , то

Следствие:

a) Если , то .

b) Если , то .

Метатеорема 3(МТ3).

Теорема дедукции (ТД), правило введения импликации (ВИ).

Пусть Г – любое множество формул.

Тогда:

c) Если Г, , то Г . В частности

d) Если , то .

Доказательство

По условию МТ3 вывод (1) формула B из множества формул (данный вывод).

Требуется доказать существование вывода (2) формула из формул множества Г (результирующий вывод).

Опишем алгоритм превращения данного вывода (1) в результирующей вывод (2). К каждой формуле данного вывода (1) припишем слово «». Тогда получим последовательность формул: , (3) заканчивающуюся нужной формулой . Эта последовательность не является, вообще говоря, выводом из множества формул Г. Однако можно перед каждой формулой вставить дополнительные формулы так, чтобы превратить последовательность формул (3) в (2). Вывод дополнительных формул зависит от того, с каким обоснованием формула входит в данный вывод (1). Возможны 4 типа обоснований:

1. - посылка множества Г;

2. - посылка А;

3. - аксиома;

4. – формула, полученная по MP из двух предшествующих формул и (p,q<i).

Рассмотрим каждый из этих случаев:

1. Пусть и . В этом случае является посылкой не только в данном выводе (1), но и в результирующем выводе (2). Тогда перед формулой последовательности (3) вставим две формулы и , из которых получается по правилу MP:

l. l. посылка

l +1. l +1. AC1

l +2. l +2. MP(l, l+1)

2. Пусть . Тогда - посылка в данном выводе (1), но не является таковой в результирующем выводе (2). В последовательности (3) будет стоять формула , которая является доказуемой (пример 1). Поэтому перед вставляем первые четыре формулы из ее доказательства.

3. Пусть – аксиома. Тогда поступаем, как и в случае 1.

4. Пусть – формула, полученная по MP из формул и (p,q<i) последовательности (1). Тогда должна иметь вид (или имеет вид ). Итак, получена из и по MP. В последовательности (2) в этом случае будут формулы и с некоторыми номерами S и t(S,t<i), и нужно обосновать включение в вывод (2) формула . Но формулы и и являются частями AC2. Таким образом, перед в данном случае необходимо вставить две формулы с номерами и :

S. S

……… …

t. t

……… …

U. AC2

U+1. MP(S, U)

U+2. MP(t,

Следствия:

a) Если , то . В частности;

b) Если , то .

Определение 1.18

Формальная аксиоматическая теория называется (просто) непротиворечивой, если ни для какой формулы A и не являются обе доказуемыми в ней. Формальная аксиоматическая теория называется (просто) противоречивой, если существует формула A, для которой одновременно А и доказуемы в этой теории.

Метатеорема 4 (МТ4)

Если , то для любой формулы E.

Следствие

Теория L непротиворечива.

Доказательство:

Допустим, что теория L противоречива. Тогда, согласно определению 1.18, существует формула А, такая, что и , и по МТ4 и , что противоречит предложению 1.5.

Полнота теории L.

В математике существует три важнейших математических проблемы:

Непротиворечивость,

полнота,

Разрешение.

Мы рассмотрим определение непротиворечивости. Введем понятие полноты.

Определение 1.19

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

Прежде чем установить полноту ИВ, необходимо доказать 4 лемма.

Лемма 1.1: Пусть д имеем логические операторы .

Для любой строки истинной таблицы любой из 5 операторов имеет место соответствия выводимость.

А	Выводимость
1. И Л 2. Л И
А В	Выводимость
3. И И И 4. И Л Л 5. Л Л Л 6. Л Л Л
А В
7. И И И 8. И Л Л 9. Л И И 10. Л Л Л
А В	Выводимость
11. И И И 12. И Л Л 13. Л И И 14. Л Л И
А В
15. И И И 16. И Л Л 17. Л И Л 18. Л Л И

 

Установим некоторые из выводимостей.

(1)

1. 1.Т1а

2. 2.Т1а

3. 3.ВО(1,2)

(9)

1. 1.Т1а

2. 2.ВД2

3. 3.Т1б(1,2)

Распространим свойство леммы 1.1 на случай произвольной формулы.

Лемма 1.2: Для любой формулы существует, содержащий атомы для любых из 2 строк ее истинной таблицы имеет место соответствия выводимость.

Доказательство данной леммы рассмотрим на л/з на конкретном примере.

Лемма 1.3: Если формула Е, содержащая атомы (и только их), общезначима, то .

Ø Пусть n=2.

 

 

E

И И И

И Л И

Л И И

Л Л И

1. ,

2. ,

3. ,

4. ,

5. , 5.УД(F1,F2)

6. , 6.УД(F3,F1)

7. , 7.УД(F5,F6)

Доказательство в общем случае получается в результате применения правила УД раз.

Лемма 1.4: для любой формулы.

Метатеорема 6: Если , то по лемме 1.4 (1.6)

Так как формула Е общезначимо, то по лемме 1.3 (1.7)

Из (1.6) и (1.7) по Т1б получим .

Следствие ИВ полна относительно общезначимости

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

Согласно Т6 если формула общезначима, то формула доказуема.

ИСЧИСЛЕНИЕ ВЫСКАЗЫВАНИЙ

Алфавит, формулы, система аксиом схем и правило вывода исчисления высказываний.

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

Алфавит и определение формулы – те же что и в алгебре высказываний. Но буквам алфавита не приписывается никакой смысл, - это просто символы, которые можно распознавать и различать.

В алгебре высказываний мы описали класс общезначимые формул, выражающих законы логики на основе понятия истинностного значения. Здесь же законы логики – множество доказуемых формул – они описываются по-другому. Некоторые формулы принимаются в качестве “аксиом”, а для получения новых формул вводится некоторое “правило вывода”. Позже рассмотрим, что обе формулировки логики высказываний – алгебра высказываний и теория L – дают эквивалентные результаты.

Определение 1.14

Аксиомами теории L называются веские формулы, которые порождают нижеследующие формульные схемы при любом выборе формул A,B,C:

1.

2.

3.

4.

5.

6.

7.

8.

9.

10.

11.

12.

13.

Каждая из схем (1)-(13) порождает счетное множество аксиом, если символы A, B, C заменять конкретными формулами. Поэтому записи (1)-(13) будем называть аксиомными схемами (AC).

Схемы (1)-(13) совпадают с первыми тринадцать формульными схемами предложения 1.6.

Определение 1.15

Правила вывода теории L называют процедуру перехода от двух формул вида A и к одной формуле вида B для любых A и B. Это правило называется modus pondus, MP. Правило MP называют также правилом удаления импликант и обозначают УИ. Формулы A и называют посылками, а B – заключением правила MP.