Правила вывода исчисления высказываний

 

Будем использовать 2 правила вывода:

a. Правило отдаления (modus ponens):

b. Правило подстановки (S): Каждую букву заменяем на формулу. Конечная формула будет истинна, если для подстановки использовались общезначимые формулы (берем общезначимую формулу и заменяем в ней каждую букву на формулу)

 

Аксиомы

1.

2.

3. - правило введения

4. - правило удаления

5. - правило введения

6. - правило удаления &

7. - правило введения

8. - правило удаления

9. - правило введения

10. - правило удаления

Если вместо пропозициональных букв будем использовать любую формулу исчисления высказываний, то можем получить бесконечное множество аксиом заданной структуры (схем аксиом).

Доказуемость формул

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

Пример доказательства формулы:

- по первой аксиоме

- используем подстановку

- по второй аксиоме

- подстановка

- подстановка в формулу 1

8.

Выводимость формул

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

 

Пример: (вывод из посылок )

- аксиома удаления &

- первая посылка

- modus ponens 1.2

- аксиома удаления &

- первая посылка

- modus ponens 4,5

- вторая посылка

- modus ponens 3,7

- modus ponens 6,8

Возникает вопрос: Можем ли мы вместо С подставить любую формулу?

Ответ: Нельзя, правило подстановки имеют ограничение, его нельзя применять к пропозициональным буквам, которые содержатся в формулах, введенных в качестве посылок.

Транзитивность секвенций

Теорема 1: Правило силлогизма

Если существуют выводы , то существует вывод

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

Вывод - означает, что есть последовательность формул . Вывод - означает, что есть последовательность формул . Запишем два вывода последовательно , полученная запись и есть вывод .

Теорема дедукции

Теорема 2: Теорема дедукции.

Импликация доказуема тогда и только тогда, когда формула выводима из .

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

Необходимость:

Пусть формула является доказуемой. Это означает что существует последовательность . Добавим в качестве посылки: получили .

Достаточность: не будем рассматривать в силу громоздкости вывода.

 

 

Непротиворечивость исчисления высказываний

Теорема 3: Теорема об общезначимости доказуемых формул.

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

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

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

Следствие 1: О непротиворечивости исчисления высказывания

Ни для какой формулы из исчисления высказываний не может быть доказана и сама формула и её отрицание.

 

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

Предположим, что формула доказуема это означает, что она общезначима . Общезначимая формула в любой интерпретации истинна . Теперь рассмотрим формулу , она будет ложна в любой интерпретации это означает, что не общезначима . По теореме об общезначимости .

Полнота исчисления высказываний

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

Если формула общезначима, то она доказуема

Следствие 1:

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

!Нельзя усилить ИВ добавлением недоказуемой формулы к системе аксиом.

Из теорем 3 и 4 следует:

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

Исчисление предикатов

Для того чтобы задать исчисление предикатов необходимо задать:

Язык (алфавит). Он совпадает с языком логики и включает в себя: пропозициональные буквы, предикатные буквы, пропозициональные переменные и формулы.

2. Аксиомы. Аксиомы исчисления высказываний актуальны для исчисления предикатов. Чаще используются схемы аксиом:

a.

b.

c. Замена возможна, если индивидные переменные не входят в формулу свободно.

Правила вывода

Дополнительные правила вывода

1. Правило всеобщности. , где С – формула исчисления предикатов, х – не входит свободно в С. Тогда можно записать .

Покажем справедливость данного правила:

Правила вывода должны быть корректными (при истинных посылках, истинные следствия)

Тогда имеем

1. Пусть тогда должно быть Истинно при всех

2. Пусть тогда при любых

2. Правило существования (). , если х не входит свободно в С, то мы можем записать

Покажем справедливость данного правила:

Имеем

1. Пусть

2. Пусть

 

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

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

Вывод формулы из множества формул Г – это некоторая последовательность формул которая заканчивается формулой , причем формулы являются аксиомами, формулами выведенными с помощью правил вывода или формулы являющиеся посылками т.е.

Примечание: Дополнительные правила вывода нельзя применять к переменным, которые были введены в качестве посылки. Такие переменные называются фиксированными переменными.

- фиксированные переменные.

Пример вывода:

Выведем, что

- допущение

- аксиома всеобщности

- modus ponens 1,2

- аксиома всеобщности

- modus ponens 3,4

Теорема дедукции

- формулы исчисления предикатов - множество формул исчисления предикатов

Необходимость

Пусть тогда имеем вывод где . Далее запишем в качестве посылки и применим правило отделения

Достаточность

Это доказательство мы опустив в связи с его громоздкостью.

Теорема: Правило силлогизма

Если то существует вывод где - формулы ИП

Используем теорему о дедукции

Тогда имеем вывод используя правило отделения получим

Теорему о дедукции и правило силлогизма можно записать в виде вспомогательных правил вывода. Вспомогательные правила вывода используются для доказательства значения факта, что вывод или доказательство существует.

- правило введения импликации (из теоремы о дедукции)

– правило силлогизма

 

Если существует вывод, записанный сверху, то существует вывод записанный снизу.