В ИВ можно выделить некоторый класс формул, которые мы будем называть ВЫВОДИМЫМИ в ИВ. Правила, позволяющие из имеющихся выводимых формул получать новые, мы будем называть правилами вывода, а исходные выводимые формулы – АКСИОМАМИ.
Аксиомы ИВ: I. 1)A->(B->A). 2)(A->(B->C))->((A->B)-(A->C)). II. 1)A&B->A. 2)A&B->B 3)(A->B)->((A->C)->(A->B&C)). III. 1)A->A\/B. 2)B->A\/B. 3)(A->C)->((B->C)->(A\/B->C)). IV. 1)(A->B)->((not B)->(not A)). 2)A->(not A). 3)(not A)->A.
