Свойства отрицания

До сих пор мы использовали только аксиомы Imp1, Imp2, Imp2', описывающие свойства символа . Теперь настало время для символа ~. Напомню соответствующие аксиомы:

Not1:

~~a => a

Not2:

(a => b) => ((a => ~b) => ~a)

Докажем несколько метатеорем, описывающих свойства символа ~ в КИВ. Будем пользоваться только аксиомами для материальной импликации (Imp1, Imp2) и отрицания (Not1, Not2).

Почти все доказательства в этой и в последующих главах (вплоть до главы "Непротиворечивость") довольно просты и требуют минимальных пояснений (которые будут даны). Можете относиться к ним как к упражнениям: некоторые (или все) метатеоремы можно попробовать сначала доказать самому, а уже потом подсмотреть одно из возможных решений, кликнув на надпись "Посмотреть доказательство" (Java-скрипты в браузере должны быть включены).

Метатеорема MT_Not_1 (сокращение означает "(М)ета(т)еорема для операции "Not" номер 1"). Это - основное орудие для доказательства формул, начинающихся со значка ~.

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

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

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

G₁, G₂,... G_β, X |— Y и

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

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

G₁, G₂,... G_β |— ~X

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

G₁, G₂,... G_β X |— Y

С помощью МТД получаем из

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

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

G₁, G₂,... G_β |— X => ~Y

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

1.1) Здесь все строки доказательства G₁, G₂,... G_β |— X => Y

...

2.1) Здесь все строки доказательства G₁, G₂,... G_β |— X => ~Y

...

3.1) Not2 |-> (X => Y) => ((X => ~Y) => ~X) // a ~> X, b ~> Y

3.2) X Y, №3.1 |-> (X => ~Y) => ~X //MP

3.3) X ~Y, №3.2 |-> ~X //MP

Метатеорема 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)