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

Метатеорема modus tollens.

X => Y, ~Y|— ~X

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

Доказательство будет состоять из доказательства

X => Y |— ~Y => ~X - см.MT_Not_5

за которым последует еще один шаг дедукции:

~Y, ~Y => ~X |-> ~X // MP

Метатеорема MT_Not_6 (эта теорема нам понадобится для доказательства очередной связи между булевой алгеброй и КИВ):

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

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

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

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

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

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

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

- дано по условию

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

- по МТД из (1)

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

- по MT_Not_5

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

- объединением доказательства (2) и (3).

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

- передвиганием символа |— вправо.

Аналогично используем второе условие.

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

- дано по условию

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

- по МТД из (5)

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

- по MT_Not_5

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

- объединением доказательства (6) и (7).

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

- передвиганием символа вправо.

Применим к доказательствам (4) и (8) MT_Not_1:

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

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

G₁, G₂,... G_β |- ~~Y (9)

По MT_Not_4:

G₁, G₂,... G_β |- Y

Свойства конъюнкции

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

And1:

(a & b) => a

And2:

(a & b) => b

And3:

a => (b => (a & b))

Метатеорема MT_And_1 (введение/удаление &):

|— X & Y => X (1)

|— X & Y => Y (2)

X & Y |— X (3)

X & Y |— Y (4)

X, Y |— X & Y (5)

X, Y |— Y & X (6)

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

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

And1|— X & Y X // a ~> X, b ~> Y

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

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

And2 |— X & Y Y // a ~> X, b ~> Y

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

(5) состоит из следующих шагов:

1) And3 |-> X => (Y (X & Y)) // a ~> X, b ~> Y

2) X, №1 |-> Y => (X & Y) // MP

3) Y, №2 |-> X & Y // MP

(6) состоит из следующих шагов:

1) And3 |-> Y => (X => (Y & X)) // a ~> Y, b ~> X

2) Y, №1 |-> X => (Y & X) // MP

3) X, №2 |-> Y & X // MP