Разнообразие вариантов КИВ относится и к аксиомам.
Среди аксиом обычно присутствует две аксиомы, описывающие свойства символа
Imp1:
(b
a)
А для второй можно привести как минимум пару вариантов:
Imp2:
b)
((a
(b
c))
(a
c))
Imp2':
(b
c))
((a
b)
(a
c))
Хммм... я надеюсь, что на примере аксиом Imp2 и Imp2' вы уже поняли, что в скобках и стрелках КИВ легко заблудиться. Поэтому, ради краткости, условимся опускать хотя бы стрелки между именами переменных:
Imp1:
Imp2:
Imp2':
Другие аксиомы я разделю на группы, каждая из которых предназначена для доказательства свойств одной из логических операций.
Свойства
Not1:
a
Not2:
b)
((a
~b)
~a)
Свойства
And1:
a
And2:
b
And3:
(b
(a & b))
Свойства
Or1:
(a
b)
Or2:
(a
b)
Or3:
c)
((b
c)
((a
b)
c))
Or3, сокращенно:
b c))
Свойства
Eq1:
b)
(a
b)
Eq2:
b)
(b
a)
Eq3:
b)
((b
a)
(a
b))
Свойства
Xor1:
b)
(~a
b)
Xor2:
b)
(b
~a)
Xor3:
~b)
((~b
a)
(a
b))
Если нас не интересуют свойства какой-то из логических операций, мы просто убираем из списка
аксиом соответствующую группу, и рассматриваем только эту часть КИВ. Понятно, что свойства
операции