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

Задача 1.

Из данной совокупности секвенций выбрать доказуемые, построить их доказательства, для недоказуемых показать их недоказуемость с помощью: а) алгоритма Квайна, б) алгоритма редукций, в) метода резолюций. Среди этих доказательств недоказуемости выбрать оптимальное в каждом конкретном случае.

а) x y, x y, y z ├ u z

б) ├ (x y) (x y)

в) x y, x z, u (x z) ├ (u y) z

г) y├ (y x) x

Решение.

а) Проверим доказуемость с помощью таблицы истинности.

x	y	z	u	x y	x y	y z	1 2	4 3	u z	5 6

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

y├ y z├ z

12 12 4

x├ x y, x├ y z, y├ z; z├ (u z)

4 7 7

x├ (x y) y├ (x y) z├ (y z); z├ (u z)

12

x, y, z├ (x y); x, y, z├ (x y); x, y, z├ (y z); x, y, z├ (u z)

1

x, y, z├ (x y) (x y) (y z); ├ x, y, z (u z)

8

(x y) (x y) (y z)├ (u z)

б) ├ (x y) (x y) =(x y) (x y) // (по аксиоме)

x

y

x y

x y

(x y) (x y)

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

x├ x; y├ y x├ x

x, y├ x; x, y├ y x, y├ x

x, y├ (x y) x, y├ (x y)

(x y) (x y)

в) x y, x z, u (x z) ├ (u y) z

X

y

z

u

x y

x

x z

x z

u 4

1 3

6 5

u y

8 z

7 9

Покажем недоказуемость с помощью

1) Алгоритма Квайна:

((x y) ( x z) (u (x z))) ((u y) z)

x=0

(y u) ((u y) z)

y=0 y=1

0 (u z)=1. u (u z)

z=0 z=1

u u u 1=1

u=0 u=1

0 1=1 1 0=0

2)Алгоритма редукций:

предположим, что

((x y) ( x z) (u (x z))) ((u y) z)=0, т.е. предположим, что формула недоказуема, тогда

((x y) ( x z) (u (x z)))=1 ((u y) z)=0

значит: u y=1, z=0

отсюда: u=1, y=1, z=0;

x y=1, x z=1, u=1, x z=1

x 0=1, значит x=0

0 1=1, 0 0=1.

Противоречий нет. Формула недоказуема.

Наиболее оптимальным является алгоритм редукций.

г) y├ (y x) x

x

y

y x

1 x

y 2

Для доказательства воспользуемся эквивалентностями ИВ:

(φ ψ) ( φ ψ); (φ ψ) ( φ ψ);

(φ (ψ χ)) (φ ψ) (φ χ).

Преобразуем

(y x) x (y x) x ( y x) x (y x) x (y x) ( x x) y x

Получаем: y├ y x

Строим доказательство

y├ y

4

y├ y x