Главная Обратная связь Поможем написать вашу работу!

Дисциплины:

Архитектура (936)
Биология (6393)
География (744)
История (25)
Компьютеры (1497)
Кулинария (2184)
Культура (3938)
Литература (5778)
Математика (5918)
Медицина (9278)
Механика (2776)
Образование (13883)
Политика (26404)
Правоведение (321)
Психология (56518)
Религия (1833)
Социология (23400)
Спорт (2350)
Строительство (17942)
Технология (5741)
Транспорт (14634)
Физика (1043)
Философия (440)
Финансы (17336)
Химия (4931)
Экология (6055)
Экономика (9200)
Электроника (7621)






Понятие логического следования



Формула F логически следует из множества формул G или, как говорят, множество формул G влечет множество формул F, G|-F, если для каждой интерпретации, при которой все формулы из G истинны, формула F также истинна. Можно говорить что F это логическое следование из G, ну или F следует из G, когда G и ~F невыполнимы одновременно. Подошли к логическому следованию с точки зрения интерпретации, рассматривая же его как формальный механизм, мы можем вмести понятия пропозиционального вывода, эквивалентного понятию логического вывода. Соответственно понятие пропозиционального вывода множество формул G влечет F, если F может быть выведено из G с использованием определенного набора правил вывода. Заметим, что правило вывода строится так, чтобы выражение F|-G и F выводится из G были эквивалентны. Понятие логического следования основано на смысле и является семантичным, понятие пропозиционального вывода основывается на правилах трактования формул и является синтаксическим.

Секвенция – выражение вида G|-F или F предпосылка G или вида G|-ложь, что значит что посылки G противоречивы. Здесь F – формула, G – некоторое конечное множество формул. Собственно, переход от сформулированных еще Аристотелем силлогических суждений, т.е. правил умозаключений, на естественном языке, т.е. переход к полным формальным правилам вывода был предложен еще Де Морганом в середине 19 века. Де Морган считал, что семантика естественного языка искажает строгий смысл правил умозаключений, поэтому он стремился перейти к манипуляциям с символами, не зависящим от того, какой смысл этим символам приписывается. Правило вывода – предписание, позволяющее из суждения 1 логической структуры, как предпосылок, вывести суждение другой логической структуры, как заключение. Правило вывода записывается в виде схемы, состоящей из верхней и нижней части. В верхней части записываются логические схемы предпосылок, в нижней логические схемы заключений. Сейчас будем использовать понятие вывода более сложное, чем то, которым будем пользоваться дальше, однако в рамках более сложного определения прекрасно укладываются некоторые метатеоремы. Все правила вывода делятся на 2 группы: основные и производные. Основные правила являются очевидными и не нуждаются в доказательстве, их делят, в свою очередь, на прямые и косвенные. Прямые правила непосредственно указывают на выводимость одних суждений из других. Косвенные дают возможность умозаключить о правомерности вывода одних суждений из других. Пример косвенного правила: правило введения дизъюнкции, из (G|-F)/(G|-FvU). Очевидно, т.к. F всегда истинно при истинных G, мы можем через дизъюнкцию приписать все, что угодно. Это правило, как видим, не содержит извлечения какой-либо части из суждений G и F, а просто говорит о формальном праве считать формулу FvU выводимой из G. Есть еще производные правила. Они описывают сокращенный процесс вывода. Выводятся из основных, т.е. если мы построили какую-то универсальную цепочку вывода, в которую может подставлять различные формулы, то этим результатом мы можем пользоваться многократно. Как мы уже говорили, правило вывода строится так, чтобы синтаксическое и семантическое определение логического следования совпадали. В связи с этим, говорят о корректности правил вывода. Правило вывода считается корректным, если для каждого примера этого правила, посылки которого являются тождественно истинными, его заключения также тождественно истинны. В данном случае примером правила будет указание конкретного множества формул G и конкретной формулы F, а также конкретной формулы U.



 



 

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

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

1) Деревом доказательства является пустое дерево, состоящие только из корня аксиоматической секвенции.

2) Пусть Т1 .. Тк деревья доказательства с корнями R1 .. Rk. Тогда (Т1 .. Тк)/S – дерево доказательства, где S некоторая секвенция, если S может быть получено из R1 .. Rk с помощью 1 из правил вывода. Корнем такого дерева является S.

E|-F следует из множества формул Е и формула E|-К можно утверждать, что из множества Е|-F&K. Мы можем построить следующую цепочку, рассмотрим Е в качестве формул множества G. Т.к. E|-F&K следует что E|-F&K&U, тогда мы сокращенно записываем т.к. E|-F и E|-K следует E|-F&KVU. Рассмотрим пример 1 из правил вывода, пусть из множества {q,r}|-p при этом из {pVq,r}|-~q, это значит что из определенного множества {q,r,pvq}|-p&~q. Здесь p q r уже некоторые конкретные формулы.

Рассмотрим ряд простых секвенций, часто используемых в логике высказываний. Их еще часто называют дедуктивными правилами вывода для высказываний.

1) Modus Ponendo Ponens или MP и это основное правило вывода в рамках любого исчисления высказываний. Это больше секвенция. (P->Q, P)/Q или P->Q,P|-Q.

2) Modus Tollento Tollens если из Р следует Q и при этом Q ложно то и Р ложно. P->Q,~Q / ~P или P->Q, ~Q|-P

3) Modus Ponendo Tollens если P и Q не могут быть истинными при этом P истинно то Q ложно. ~(P&Q),P / ~Q или ~(P&Q), P |- ~Q

4) Modus Tollento Ponens сначала формально: PvQ, ~P / Q или PvQ, ~p |-Q если либо P или Q является истинным и P не истинно, то истинно Q. Правило включающего или. Сама формулировка или или наталкивает использование исключающего или. Это тот случай, когда неопределенность, содержащаяся в естественном языке искажает смысл правила умозаключений, тогда как все становится предельно понятным в формульной записи.



Исчисление высказываний L.

Исчисление высказываний L является формальной аксиоматической теорией для логики высказываний. Понятие формулы задается по аналогии с уже рассмотренным, т.е. есть алфавит, состоящий из заглавных латинских букв A B C, есть (), есть связь –> not. Если А и В формулы, то (~A|B) тоже формула. Для упрощения записи часто не пишем (). В частности не имеет смысл писать скобки вокруг отрицания, вообще внешние скобки формулы, при этом они присутствуют. Выделены следующие аксиомы, точнее схемы аксиом.

(A1) A->(B->A)

(A2) A->(B->C)->((A->B)->(A->C))

(A3) (~B->~A)->((~B->A)->B)

Здесь А В и С – произвольные формулы, поэтому каждая из схем описывает бесконечное множество аксиом. Если бы мы считали их непосредственно аксиомами, нам бы пришлось вводить правило подстановки. В исчислении высказываний L используется правило вывода MP. A->B,A => B или A->B, A|-B

При любых А В и С схемы аксиом являются тавтологиями, что легко проверить, построив таблицу истинности. Кроме того, схемы аксиом выбраны так, чтобы множество теорем в исчислении высказывания L совпадало со множеством тавтологий логики высказываний. Полностью это утверждение будет сформулировано в виде теоремы о полноте, которую рассмотрим позднее.

Лемма: |-A->A или для любой формулы А формула А->A является теоремой исчисления высказываний L. Построим цепочку вывода:

1) В схеме аксиом А1 : заменяем В на А, В:=А Получаем формулу A->(A->A)

2) A2: проводим замену А:А, В заменяется В:=А->А С:=А

Получаем (A->((A->A)->A))->(A->(A->A))->(A->A))

3) В схему аксиом А1 подставим А:=А В:=А->А Получаем A->((A->A)->A)

4) Сравниваем 2 и 3-ю формулы, видим общую часть. По правилу МР получаем 2-ю часть формулы 2: ((A->(A->A))->(A->A)).

5) Сравниваем 4-ю формулу и 1, по МР получаем A->A.

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

Она является метатеоремой, т.к. формулируется на метаязыке.

Пусть Г – множество формул исчисления высказываний L. А и В – некоторые формулы. Пусть из множества Г и формулы А выводится В. Г,А|-В. Тогда из Г|-A->В. В частности, при пустом Г из выводимости В из А следует теорема: |-А->В

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

Теорему дедукции будем доказывать по индукции. Пусть из множества формул Г и формулы А выводится В, Г,А|-В, значит существует цепочка формул A1..An, причем An=В. Формулы Ai или принадлежат Г или совпадают с А или являются аксиомами или получены из предыдущих по правилу вывода. Покажем, что верно утверждение Г|-A->A. Рассмотрим базис индукции i=1, тогда А1 может быть:

1) аксиома

2) принадлежать Г

3) совпадать с формулой А

В первой и 2 случае поступаем следующим образом: в схему аксиом А1 подставляем вместо А:=А1, вместо В:=А. Получаем А1->(A->A1). Это соответственно получается аксиома по А1. Т.к. А1 или аксиома или принадлежит Г, то А1 есть. По МР А1->(A->A1),A1|-A->A1. 3-й случай: А1=А. Т.к. А->A выводима, то она выводима и из Г, Г|-A->A. Рассмотрим индуктивный переход. Предположим, что предположение индукции доказано для любого i<k. Рассмотрим формулу Ак. Формула Ак как и А1 может быть аксиомой, принадлежать Г, совпадать с А и быть полученной по правилу вывода из формул Ai,Aj, где I и j <k. В случаях 1-3 рассуждения аналогичны базису индукции. Рассмотрим 4-й случай. То что Ак получена по МР из Аi Aj означает, что Ai=Aj->Ak. Сделаем подстановку в схему аксиом А2. А2: А=А, В=Ai, С:=Ак.

Получаем (A->(Ai->Ak))->((A->Ai)->(A->Ak))*. По предположению индукции из Г|-A->Aj. С учетом того, что есть Aj: Г|-(A->(Ai->Ak))**. По МР из подстановки А2 получаем: MP*,**: (A->Ai)->(A->Ak)***. По предположению индукции А->Ai выводимо. Из А->Ai по МР***,A->Ai получаем А->Ak. Так индуктивный переход доказан, следовательно доказана и сама теорема дедукции.

Следствие теоремы дедукции.

Следствие 1.

Если из Г|-A->B и Г|-B-C, то Г|-A->C

Доказательство: из Г и А, А->B и B->C выводима А->C. По МР получаем формулу В: А, A->B|-B. Есть В, есть B->C, MP: B, B->C|- C, тогда по теореме дедукции из Г, A->, B->C |- A->C.

 

Следствие 2.

Если A->B->C и есть В то выводима А->C. Покажем, что из A->(B->C),A,B|-C. Из MP A->(B->C),A|-B->C, MP: B->C,B |- C => |-C, тогда по теореме дедукции имеем право перенести 1 из формул в правую часть, A->(B->C),B|-A->C.

 

Следствие 3.

Если из множества A1..An |-C, то выводима формула A1->(A2->(…An->C)…))). Для доказательства последовательно применяем теорему дедукции и переносим формулы Ai вправо от знака выводимости.

Теорема о полноте.

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

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

A B A->B

0 0 1

0 1 1

1 0 0

1 1 1

Любая формула, которая получается из аксиом по МР является тавтологией.

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

 


Просмотров 547

Эта страница нарушает авторские права




allrefrs.ru - 2021 год. Все права принадлежат их авторам!