Аксиомы КИВ

Разнообразие вариантов КИВ относится и к аксиомам.

Среди аксиом обычно присутствует две аксиомы, описывающие свойства символа . Первая аксиома, как правило, формулируется так:

Imp1:

a => (b => a)

А для второй можно привести как минимум пару вариантов:

Imp2:

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

Imp2':

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

На примере аксиом Imp2 и Imp2' было видно, что в скобках и стрелках КИВ легко заблудиться. Поэтому, ради краткости, условимся опускать хотя бы стрелки между именами переменных:

Imp1:

a(ba)

Imp2:

ab (a(bc)(ac))

Imp2':

a(bс) (ab(ac))

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

Свойства ~:

Not1:

~~a => a

Not2:

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

Свойства &:

And1:

(a & b) => a

And2:

(a & b) => b

And3:

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

Свойства V:

Or1:

a => (a V b)

Or2:

b => (a V b)

Or3:

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

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

ac (bc (aVb c))

Свойства ó:

Eq1:

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

Eq2:

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

Eq3:

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

Свойства :

Xor1:

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

Xor2:

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

Xor3:

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

Если нас не интересуют свойства какой-то из логических операций, мы просто убираем из списка аксиом соответствующую группу, и рассматриваем только эту часть КИВ. Понятно, что свойства операции => убрать нельзя, поскольку через эту связку определяются свойства всех других операций. Также для операции понадобится операция ~ (или надо будет придумать какие-то другие аксиомы для ).