Метатеорема MT_Not_2

Если бы можно было доказать противоречие, то можно было бы доказать все, что угодно.

Или формально:

Можно составить доказательство: X, ~X |— Y

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

Сначала берем тривиальное доказательство (о тривиальных доказательствах смотрите учебник по дедуктивному методу):

X, ~X, ~Y |— X

Берем другое тривиальное доказательство:

X, ~X, ~Y |— ~X

Это как раз случай, описанный в MT_Not_1: несколько гипотез, из которых следует противоречие. По MT_Not_1 получаем доказательство:

X, ~X |— ~~Y

Новое доказательство будет иметь вид:

1.1) Здесь все строки доказательства X, ~X |— ~~Y

...

2.1) Not2 |— ~~Y => Y // a ~> Y

2.2) ~~Y, №2.1 |— Y //MP

Метатеорема MT_Not_3:

Двойное отрицание доказывается из формулы без двойного отрицания и наоборот.

Или формально:

|— ~~X => X (1)

~~X |— X (2)

|— X => ~~X (3)

X |— ~~X (4)

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

(1) состоит из одного шага подстановки:

Not1 |-> ~~X |— X // a ~> X

(2) получается передвиганием значка |— на один шаг влево в формуле (1).

(4) получается применением MT_Not_1 к двум тривиальным доказательствам:

X, ~X |— X - тривиальное доказательство

X, ~X |— ~X - тривиальное доказательство

X |— ~~X - MT_Not_1

(3) получается применением МТД к (4)

Метатеорема MT_Not_4:

Вывод и любую гипотезу можно заменять на ее двойное отрицание и обратно.

Или формально:

Если имеется доказательство:

G₁, G₂,... G_β, X |— Y, (1)

то можно составить как доказательство

G₁, G₂,... G_β, X |— ~~Y, (2)

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

G₁, G₂,... G_β, ~~X |— Y, (3)

и обратно.

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

Объединим доказательства:

G₁, G₂,... G_β, X |— Y - (1)

Y |— ~~Y - из MT_Not_3

и получим:

G₁, G₂,... G_β, X |— ~~Y - (2)

- тем самым доказана возможность из (1) получить (2)

Объединим доказательства:

G₁, G₂,... G_β, X |— ~~Y - (2)

~~Y |— Y - из MT_Not_3

и получим:

G₁, G₂,... G_β, X |— Y - (1)

- тем самым доказана возможность из (2) получить (1)

Объединим доказательства:

~~X |— X - из MT_Not_3

G₁, G₂,... G_β, X |— Y - (1)

и получим:

G₁, G₂,... G_β, ~~X |— Y - (3)

- тем самым доказана возможность из (1) получить (3)

Объединим доказательства:

X |— ~~X - из MT_Not_3

G₁, G₂,... G_β, ~~X |— Y - (3)

и получим:

G₁, G₂,... G_β, X |— Y - (1)

- тем самым доказана возможность из (3) получить (1)

Метатеорема MT_Not_5 (правила обращения импликации):

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

Или формально:

(X => Y) |— (~Y => ~X) (1)

(X => Y) => (~Y => ~X) (2)

(~X => ~Y) |— (Y => X) (3)

(~X => ~Y) => (Y => X) (4)

(~X => Y) |— (~Y => X) (5)

(~X => Y) => (~Y => X) (6)

(X => ~Y) |— (Y => ~X) (7)

(X => ~Y) => (Y => ~X) (8)

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

Доказательство (1) и (2):

Пробное передвигание значка |— влево дает список гипотез X => Y, ~Y => ~X. Для доказательства ~X попробуем MT_Not_1. Для нее в список гипотез надо будет добавить X.

X => Y, ~Y, X |— ~Y - тривиальное доказательство

X => Y, ~Y, X |— Y - в один шаг: X, X Y Y // MP

X => Y, ~Y |— ~X - по MT_Not_1

X => Y |— ~Y => ~X - по МТД - формула (1)

|— (X => Y) => (~Y => ~X) - по МТД - формула (2)

Доказательство (3) и (4):

~X => ~Y, Y, ~X |— Y - тривиальное доказательство

~X => ~Y, Y, ~X |— ~Y - в один шаг: ~X, ~X => ~Y |— ~Y // MP

~X => ~Y, Y |— ~~X - по MT_Not_1

~X => ~Y, Y|— X - по MT_Not_4

~X => ~Y |— Y => X - по МТД - формула (3)

|— (~X => ~Y) => (Y => X) - по МТД - формула (4)

Доказательство (5) и (6):

~X => Y, ~Y, ~X |— ~Y - тривиальное доказательство

~X => Y, ~Y, ~X |— Y - в один шаг: ~X, ~X Y |— Y // MP

~X => Y, ~Y |— ~~X - по MT_Not_1

~X => Y, ~Y |— X - по MT_Not_4

~X => Y |— ~Y => X - по МТД - формула (5)

|— (~X => Y) => (~Y => X) - по МТД - формула (6)

Доказательство (7) и (8):

X => ~Y, Y, X |— Y - тривиальное доказательство

X => ~Y, Y, X |— ~Y - в один шаг: X, X => ~Y|— ~Y // MP

X => ~Y, Y |— ~X - по MT_Not_1

X => ~Y|— Y => ~X - по МТД - формула (7)

|— (X => ~Y) => (Y => ~X) - по МТД - формула (8)