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

Запятые в спиcке гипотез можно заменять на символ & и обратно.

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

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

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

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

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

и обратно

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

Составляем доказательство (2) следующим образом:

Строки доказательства X & Y |— X из MT_And_1.

Строки доказательства X & Y |— Y из MT_And_1.

Строки доказательства G₁, G₂,... G_β, X, Y |— Z из (1).

Составляем доказательство (1) следующим образом:

Строки доказательства X, Y|— X & Y из MT_And_1.

Строки доказательства G₁, G₂,... G_β, X & Y |— Z из (2).

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

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

Or1:

a => (a V b)

Or2:

b => (a V b)

Or3:

(a => c) => ((b => c) => ((a V b) => c))

Or3, сокращенно:

ac (bc (aVb c))

Метатеорема MT_Or_1 (введение V ):

|— X => X V Y (1)

|— Y=> X V Y (2)

X X V Y (3)

Y XV Y (4)

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

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

Or1 |-> X => X V Y // a ~> X, b ~> Y

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

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

Or2 |-> Y => X V Y // a ~> X, b ~> Y

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

Метатеорема MT_Or_2 (удаление ):

Два доказательства, отличающиеся одной гипотезой, можно объединить в одно, если объединить различающиеся гипотезы через .

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

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

G₁, G₂,... , X |— Z и

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

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

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

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

Из доказательства G₁, G₂,... G_β, X |— Z, которое дано в условии, получим с помощью МТД:

G₁, G₂,... G_β X => Z (1)

Из доказательства G₁, G₂,... G_β, Y |— Z, которое дано в условии, получим с помощью МТД:

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

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

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

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

1) Or3 |-> (X => Z) => ((Y => Z) => (X V Y => Z)) // a ~> X, b ~> Y, c ~> Z

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

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

4) X V Y, №3 |-> Z // MP

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

Докажем несколько метатеорем, описывающих свойства символа в КИВ. Будем пользоваться только аксиомами для материальной импликации (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). Операция в булевой алгебре представляет собой своего рода зеркальное отражение операции ... и в КИВ свойства этих двух операций имеют определенное сходство.

X or1:

(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)