Пропозициональный вывод
Существует другое определение следования, которое выглядит совершенно отличающимся от данного выше, но в действительности эквивалентное ему. В соответствие с этим определением, G влечёт F, если F может быть выведено из G с использованием определенного набора «правил вывода». Первое определение, основанное на интерпретации, – «семантическое», второе, основанное на понятии вывода – «синтаксическое» или «дедуктивное».
О корректности, полноте и разрешимости
Выводы в логике высказываний – наш основной объект изучения до конца данной части.
Вывод строятся из конструкций, которые называются « секвенциями ».
Определение 15 (Секвенция). Секвенция – это выражение вида G |– F (« F при посылках G») или G |– ^ («посылки G противоречивы»), где F – формула и G – конечное множество формул. *
Мы определим, какие секвенции рассматриваются «начальными», и опишем несколько «правил вывода» для порождения новых секвенций из секвенций, порождённых ранее. Начальные секвенции называются аксиомами.
Определение 16 (Аксиомы). Аксиомы в исчислении высказываний имеют вид
Мы определим 12 правил вывода, и удобно вводить их постепенно.
Предполагая, что это уже сделано, определим понятие вывода. Выводы у нас будут представляться в виде деревьев доказательства.
Определение 17 (Дерево доказательства). Дерево доказательства определим рекурсивно:
1. Деревом доказательства является пустое дерево доказательства, состоящее только из корня – аксиомы.
2. Пусть T 1 . Tk – деревья доказательства с корнями R 1 . Rk. Тогда
3. (где S – некоторая секвенция) – дерево доказательства, если S может быть получена из R 1 . Rk с помощью одного из правил вывода. Корнем такого дерева является S.
Определение 18 (Доказуемая секвенция). Если существует дерево доказательства с корнем R, то R называют доказуемой секвенцией. Если этот корень имеет вид G |– F, то говорят о выводе формулы F из G.
В соответствие с дедуктивным определением следования говорят, что F следует из G, если существует вывод F из подмножества G.
Понравилась статья? Добавь ее в закладку (CTRL+D) и не забудь поделиться с друзьями:
Источник
Пропозициональный вывод
Существует другое определение следования, которое выглядит совершенно отличающимся от данного выше, но в действительности эквивалентное ему. В соответствие с этим определением, влечёт F, если F может быть выведено из с использованием определенного набора «правил вывода». Первое определение, основанное на интерпретации, – «семантическое», второе, основанное на понятии вывода – «синтаксическое» или «дедуктивное».
О корректности, полноте и разрешимости
Выводы в логике высказываний – наш основной объект изучения до конца данной части.
Вывод строятся из конструкций, которые называются «секвенциями».
Определение 15 (Секвенция). Секвенция – это выражение вида |– F («F при посылках ») или |– («посылки противоречивы»), где F – формула и – конечное множество формул. *
Мы определим, какие секвенции рассматриваются «начальными», и опишем несколько «правил вывода» для порождения новых секвенций из секвенций, порождённых ранее. Начальные секвенции называются аксиомами.
Определение 16 (Аксиомы). Аксиомы в исчислении высказываний имеют вид
Мы определим 12 правил вывода, и удобно вводить их постепенно.
Предполагая, что это уже сделано, определим понятие вывода. Выводы у нас будут представляться в виде деревьев доказательства.
Определение 17 (Дерево доказательства). Дерево доказательства определим рекурсивно:
- Деревом доказательства является пустое дерево доказательства, состоящее только из корня – аксиомы.
- Пусть T1, . Tk – деревья доказательства с корнями R1, . Rk. Тогда
T1 . Tk - (где – некоторая секвенция) – дерево доказательства, если может быть получена из R1, . Rk с помощью одного из правил вывода. Корнем такого дерева является .
Определение 18 (Доказуемая секвенция). Если существует дерево доказательства с корнем R, то R называют доказуемой секвенцией. Если этот корень имеет вид |– F, то говорят о выводе формулы F из .
В соответствие с дедуктивным определением следования говорят, что F следует из , если существует вывод F из подмножества .
Правила для конъюнкции и импликации
Источник
23. Дерево доказательств
Для описания производных правил введем понятие дерево доказательств. Дерево доказательства определим рекурсивно:
- Деревом доказательства является пустое дерево, состоящие только из корня аксиоматической секвенции.
- Пусть Т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 из правил вывода, пусть из множества |-p при этом из |-~q, это значит что из определенного множества |-p&~q. Здесь p q r уже некоторые конкретные формулы.
Рассмотрим ряд простых секвенций, часто используемых в логике высказываний. Их еще часто называют дедуктивными правилами вывода для высказываний.
- Modus Ponendo Ponens или MP и это основное правило вывода в рамках любого исчисления высказываний. Это больше секвенция. (P->Q, P)/Q или P->Q,P|-Q.
- Modus Tollento Tollens если из Р следует Q и при этом Q ложно то и Р ложно. P->Q,~Q / ~P или P->Q, ~Q|-P
- Modus Ponendo Tollens если P и Q не могут быть истинными при этом P истинно то Q ложно. ~(P&Q),P / ~Q или ~(P&Q), P |- ~Q
- Modus Tollento Ponens сначала формально: PvQ, ~P / Q или PvQ, ~p |-Q если либо P или Q является истинным и P не истинно, то истинно Q. Правило включающего или. Сама формулировка или или наталкивает использование исключающего или. Это тот случай, когда неопределенность, содержащаяся в естественном языке искажает смысл правила умозаключений, тогда как все становится предельно понятным в формульной записи.
24. Исчисление высказываний l.
Исчисление высказываний L является формальной аксиоматической теорией для логики высказываний. Понятие формулы задается по аналогии с уже рассмотренным, т.е. есть алфавит, состоящий из заглавных латинских букв A B C, есть (), есть связь –> not. Если А и В формулы, то (~A|B) тоже формула. Для упрощения записи часто не пишем (). В частности не имеет смысл писать скобки вокруг отрицания, вообще внешние скобки формулы, при этом они присутствуют. Выделены следующие аксиомы, точнее схемы аксиом.
Здесь А В и С – произвольные формулы, поэтому каждая из схем описывает бесконечное множество аксиом. Если бы мы считали их непосредственно аксиомами, нам бы пришлось вводить правило подстановки. В исчислении высказываний L используется правило вывода MP. A->B,A => B или A->B, A|-B
При любых А В и С схемы аксиом являются тавтологиями, что легко проверить, построив таблицу истинности. Кроме того, схемы аксиом выбраны так, чтобы множество теорем в исчислении высказывания L совпадало со множеством тавтологий логики высказываний. Полностью это утверждение будет сформулировано в виде теоремы о полноте, которую рассмотрим позднее.
Лемма: |-A->A или для любой формулы А формула А->A является теоремой исчисления высказываний L. Построим цепочку вывода:
- В схеме аксиом А1 : заменяем В на А, В:=А Получаем формулу A->(A->A)
- A2: проводим замену А:А, В заменяется В:=А->А С:=А
- В схему аксиом А1 подставим А:=А В:=А->А Получаем A->((A->A)->A)
- Сравниваем 2 и 3-ю формулы, видим общую часть. По правилу МР получаем 2-ю часть формулы 2: ((A->(A->A))->(A->A)).
- Сравниваем 4-ю формулу и 1, по МР получаем A->A.
Источник