Слава Ф.
православный христианин нет доступа на форум
Тема: #83189
Сообщение: #3161094 05.03.09 21:58
|
Хорошо, я отвечу на вашу логику с точки зрения предмета и значения логической семантики.
Пропозициональный вывод
Существует другое определение следования, которое выглядит совершенно отличающимся от данного выше, но в действительности эквивалентное ему. В соответствие с этим определением, G влечёт F, если F может быть выведено из G с использованием определенного набора ``правил вывода''. Первое определение, основанное на интерпретации, – ``семантическое'', второе, основанное на понятии вывода – ``синтаксическое'' или ``дедуктивное''.
О корректности, полноте и разрешимости
Выводы в логике высказываний – наш основной объект изучения до конца данной части.
Вывод строятся из конструкций, которые называются ``секвенциями''.
Определение 15 (Секвенция). Секвенция – это выражение вида G |– F (``F при посылках G'') или G |– ^ (``посылки G противоречивы''), где F – формула и G – конечное множество формул. *
Мы определим, какие секвенции рассматриваются ``начальными'', и опишем несколько ``правил вывода'' для порождения новых секвенций из секвенций, порождённых ранее. Начальные секвенции называются аксиомами.
Определение 16 (Аксиомы). Аксиомы в исчислении высказываний имеют вид
{ F } |– F.
Мы определим 12 правил вывода, и удобно вводить их постепенно.
Предполагая, что это уже сделано, определим понятие вывода. Выводы у нас будут представляться в виде деревьев доказательства.
Определение 17 (Дерево доказательства). Дерево доказательства определим рекурсивно:
1. Деревом доказательства является пустое дерево доказательства, состоящее только из корня – аксиомы.
2. Пусть T1, ..., Tk – деревья доказательства с корнями R1, ..., Rk. Тогда
T1 ... Tk
S
(где S – некоторая секвенция) – дерево доказательства, если S может быть получена из R1, ..., Rk с помощью одного из правил вывода. Корнем такого дерева является S.
Определение 18 (Доказуемая секвенция). Если существует дерево доказательства с корнем R, то R называют доказуемой секвенцией. Если этот корень имеет вид G |– F, то говорят о выводе формулы F из G.
В соответствие с дедуктивным определением следования говорят, что F следует из G, если существует вывод F из подмножества G.
Правила для конъюнкции и импликации
G |– F G |– G
(В&)
G |– F & G
G |– F & G
(У&)
G |– F
G |– F & G
G |– G
G И { F } |– G
(ВЙ)
G |– F Й G
G |– F G |– FЙ G
(УЙ)
G |– G
В каждом из этих пяти правил вывода, одно или два выражения над горизонтальной чертой представляют ``посылки'', к которым правило может быть применено, и выражение под чертой представляет ``заключение'' которое выводится по этому правилу. Правила В& и ВЙ – ``правила введения'' конъюнкции и импликации; У& и УЙ – ``правила удаления''. Подставляя конкретные формулы вместо метапеременных F и G и конкретные конечные множества формул вместо метапеременной G некоторое правило вывода, мы получаем пример этого правила. Например,
{q, r} |– p {p Ъ q, r} |– ¬q
{q, r, p Ъ q} |– p & ¬q
есть пример правила введения конъюнкции.
Пример простого вывода. . Выведем формулу q из посылки p & q. Этот вывод получается за один шаг с помощью второго правила удаления конъюнкции.
{q} |– q
(У&)
{p & q} |– q
2.26 Найдите вывод q & p из p & q.
см. Решение
В двух следующих задачах выведите данную формулу из пустого множества посылок.
2.27 (p & p) Й p.
2.28 (p & p) є p.
Правило введения посылки
Мы построили несколько примеров простых выводов. Однако, используя только правила для конъюнкции и импликации, мы не сможем построить вывод формулы p & q из множества посылок {p, q}. Действительно, формулу {p, q} |– p & q мы можем получить с помощью правила (В&) из формулу {p, q} |– p и формулу {p, q} |– q. Однако ``очевидные'' формулы {p, q} |– p и {p, q} |– q мы не сможем вывести. У нас нет правила, позволяющего выводить формулу из некоторого множества посылок, если она выводится из более узкого множества. Это правило вывода назовём правилом введения посылки.
G |– F
(ВП)
G И {G} |– F
Пример вывода. Мы приводим вывод p Й ((p Й q) Й (p & q)) из пустого множества посылок:
{p} |– p
(ВП)
{p,p Й q} |– p
{p} |– p
(ВП)
{p,p Й q} |– p
{p Й q} |– p Й q
(ВП)
{p,p Й q} |– p Й q
(УЙ)
{p,p Й q} |– q
(В&)
{p,p Й q} |– p & q
(ВЙ)
{p} |– (p Й q) Й (p & q)
(ВЙ)
Ж |– p Й ((p Й q) Й (p & q))
2.29 Найдите вывод p Й r из p Й q и q Й r.
2.30 Найдите вывод r из p & q и p Й (q Й r).
В каждой из следующих задач выведите данную формулу из пустого множества посылок.
2.31 p Й (q Й p).
2.32 p Й ((p & q) є q).
2.33 ((p & q) Й r) є (p Й (q Й r)).
Корректность правил вывода
Определение 19 (Истинность секвенций). Секвенция G |– F тождественно истинна, если G влечёт F.*
Определение 20 (Корректность правил вывода). Правило вывода корректно, если для каждого примера этого правила посылки которого являются тождественно истинными, его заключение также тождественно истинно.
2.34 Правило введения посылки корректно.
2.35 Оба правила удаления конъюнкции корректны.
2.36 Правило введения конъюнкции корректно.
2.37 Правило удаления импликации корректно.
2.38 Правило введения импликации корректно.
Правила для отрицания и правила противоречия
Следующие четыре правила вывода – правила введения и удаления отрицания ``правило сведения к противоречию'' и ``правило противоречия''.
G И { F } |– ^
(В¬)
G |– ¬F
G И { ¬F } |– ^
(У¬)
G |– F
G |– F G |– ¬F
(В^)
G |– ^
G |– ^
(У^)
G |– F
Выведите секвенции:
2.39 {¬¬p} |– p.
см. Решение
2.40 {p} |– ¬¬p.
В каждой из следующих задач выведите данную формулу из пустого множества посылок.
2.41 ¬(p & ¬p).
2.42 (p & ¬p) Й q.
Определение 21 (Истинность секвенций). Секвенция G |– ^ тождественно истинна, если G не выполнимо.
2.43 Правило удаления отрицания корректно.
2.44 Правило введения отрицания корректно.
2.45 Правило противоречия корректно.
Правила для дизъюнкции
Оставшиеся три правила вывода – правила введения и удаления дизъюнкции:
G |– F
(В Ъ)
G |– F Ъ G
G |– G
G |– F Ъ G
G |– F Ъ G G И F |– C G И G |– C
(У Ъ)
G |– C
Здесь F и G – формулы, и C – либо формула, либо ^.
Теперь описание системы вывода для логики высказываний завершено.*
Мы рекомендуем строить деревья доказательства, начиная с корней (т.е. с формул, которые надо вывести) и постепенно нарашивая дерево, добиваясь, чтобы конечными формулами в дереве были аксиомы.
О том, как строить дерево доказательства.
В каждой из следующих задач выведите данную формулу из пустого множества посылок.
2.46 (p Ъ q) Й (q Ъ p).
2.47 (p Ъ p) є p.
2.48 ¬p Й ((p Ъ q) є q).
2.49 (p & (q Ъ r)) є ((p & q) Ъ (p & r)).
2.50 ¬¬p є p.
2.51 ¬(p Ъ q) є (¬p & ¬q).
2.52 Оба правила введения дизъюнкции корректны.
2.53 Правило удаления дизъюнкции корректно.
Корректность и полнота логики высказываний
Теорема корректности. Если существует вывод F из G, тогда G логически влечёт F.
Теорема полноты. Для любой формулы F и любого множества формул G, если G влечёт F, тогда существует вывод F из подмножества G.
Полнота логики высказываний (для другого множества правил вывода) была установлена Емилем Постом в 1921 году.
Рад был поделиться информацией и опытом.Попробуйте попрактиковать высказанное мною. Удачи!)))
|