Взаимосвязь аксиом исчисления высказываний

Формулы исчисления высказываний (тавтологии в стандартной бинарной логике), введенные ниже, проверяются на совместность на различных интерпретациях в произвольных N-значных логиках. Базовые связки - импликация (->) и отрицание (!). Правило вывода - modus ponens. Истиной T считается значение (N-1), а "ложь" - это 0. Всегда (T -> T) = T, поэтому из истинных формул выводятся только истинные. Формула, не равная всегда истине не зависит от формул, которые в этой модели логики являются тавтологиями (т.е. равными N-1).

N = фиксировать отрицание (!a=base-a) не только правило MP, но и правило TD
показывать сколько раз встретилась формула
показывать число пересечений пар
показывать все сочетания пересечений формул
показывать возможные системы пар аксиом (max аксиом = )
показывать возможные следования формул (max посылок = )