Основной вопрос философии... тьфу ты, основной вопрос КИВ состоит в том, насколько она похожа на булеву алгебру. Этому вопросу мы посвятим несколько глав. Для начала попробуем оценить аксиомы КИВ. Интересно, что эти формулы представляют в булевой алгебре, какие таблицы истинности имеют? Аксиом у нас много, обезъянью работу по составлению таблиц истинности делать вручную не хочется. Что ж, заставим компьютер, у него голова железная, болеть не будет.

Ниже приведена несложная программа на C++, которая позволяет получить таблицу истинности для любой формулы, в которой есть от 1 до 26 переменных из A, B, C,..., Z. В языке C++ нет всех тех символов, которые мы используем в КИВ, так что придется сделать замену. Переменные останутся как есть, скобки - тоже, а также операции ~ и &. Для остальных операций подберем похожие символы (фактически, мы просто выберем немного другой алфавит):

• Вместо символа будем использовать >.
• Вместо символа будем использовать ==.
• Вместо символа будем использовать |.
• Вместо символа будем использовать +.
• Вместо символа true будем использовать t.
• Вместо символа false будем использовать f.

В нужном месте программы напишем формулу, для которой надо вычислить таблицу истинности с учетом этих поправок к алфавиту, а также укажем, порядок столбцов в таблице (а заодно и список переменных,которые есть в формуле). После чего скомпилируем программу, запустим и полюбуемся на результат.

Текст программы выглядит так (если вы не умеете программировать на языке C++, не обращайте на него внимания).

Результат выполнения программы для формулы (A B) ((B A) B) выглядит так:

  A  |  B  |
-----|-----|-----
false|false|true
false|true |true
true |false|true
true |true |true

Tavtologia

Заодно программа определяет тип формулы: тавтология, нейтральная или невыполнимая. Если прогнать эту программу для всех аксиом КИВ, то всякий раз получится тавтология.