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

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

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

Свойства :

Or1:

a (a b)

Or2:

b (a b)

Or3:

(a c) ((b c) ((a b) c))

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

ac (bc (ab 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))

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