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

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

Eq1:

(a ó b) => (a => b)

Eq2:

(a ó b) => (b => a)

Eq3:

(a => b) => ((b => a) => (a ó b))

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

X => Y, Y => X |— X ó Y (1)

X ó Y |— X => Y (2)

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

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

Доказательство (1) состоит из следующих шагов:

1) Eq3 |-> (X => Y) => ((Y => X) => (X ó Y)) // a ~> X, b ~> Y

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

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

Доказательство (2) состоит из следующих шагов:

1) Eq1 |-> (X ó Y) => (X => Y) // a ~> X, b ~> Y

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

Доказательство (3) состоит из следующих шагов:

1) Eq2 |-> (X ó Y) => (Y => X) // a ~> X, b ~> Y

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

Метатеорема MT_Eq_2 (вариант modus ponens для равноистинности):

X, X ó Y |— Y (1)

Y, X ó Y |— X (2)

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

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

X ó Y |— X => Y

Передвигаем символ на шаг вправо:

X ó Y, X |— Y

Меняем местами гипотезы:

X, X ó Y |— Y

- получили (1).

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

X ó Y |— Y => X

Передвигаем символ на шаг вправо:

X ó Y, Y |— X

Меняем местами гипотезы:

Y, X ó Y |— X

- получили (2).

Метатеорема MT_Eq_3 (вариант пункта 1 в MT_Eq_1):

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

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

и

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

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

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

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

Составляем новое доказательство из таких частей:

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

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

1) Eq3 |-> (X => Y) => ((Y => X) => (X ó Y)) // a ~> X, b ~> Y

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

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

Свойства исключающего "ИЛИ"

Докажем несколько метатеорем, описывающих свойства символа в КИВ. Будем пользоваться только аксиомами для материальной импликации (Imp1, Imp2) и исключающего "ИЛИ" (Xor1, Xor2, Xor3). Операция в булевой алгебре представляет собой своего рода зеркальное отражение операции ... и в КИВ свойства этих двух операций имеют определенное сходство.

Xor1:

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

Xor2:

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

Xor3:

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

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

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

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

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

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

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

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

Доказательство (1) состоит из следующих шагов:

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

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

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

Доказательство (2) состоит из следующих шагов:

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

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

Доказательство (3) состоит из следующих шагов:

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

2) X Y, №1 Y => ~X // MP

Доказательство (4).

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

- доказательство (2)

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

- по MT_Not_5

X Y |— ~Y => X

- тривиальное объединение (4.1) и (4.2)

Доказательство (5).

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

- доказательство (3)

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

- по MT_Not_5

X Y |— X => ~Y

- тривиальное объединение (4.1) и (4.2)

Метатеорема MT_Xor_2 (вариант modus ponens для равноистинности):

~X, X Y |— Y (1)

Y, X Y |— ~X (2)

~Y, X Y |— X (3)

X, X Y |— ~Y (4)

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

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

Доказательство (2) получается из доказательства (3) в MT_Xor_1 передвиганием символа |— на шаг вправо и перестановкой гипотез.

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

Доказательство (4) получается из доказательства (5) в MT_Xor_1 передвиганием символа |— на шаг вправо и перестановкой гипотез.

Метатеорема MT_Xor_3 (вариант пункта 1 в MT_Xor_1):

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

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

и

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

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

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

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

Составляем новое доказательство из таких частей:

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

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

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

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

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