Правила для конъюнкции и импликации

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.31p Й (q Й p).

2.32p Й ((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.48p Й ((p Ъ q) є q).

2.49(p & (q Ъ r)) є ((p & q) Ъ (p & r)).

2.50p є p.

2.51(p Ъ q) є (p & q).

2.52Оба правила введения дизъюнкции корректны.

2.53Правило удаления дизъюнкции корректно.

---

Дата добавления: 2018-02-28; просмотров: 1014; Мы поможем в написании вашей работы!

Поделиться с друзьями:

---

---

Мы поможем в написании ваших работ!