Описание базиса в полу-редуцированной форме для правил вывода интуиционистской логики

Показывается, что множество всех правил в полу-редуцированной форме, посылки которых удовлетворяют набору специфичных условий, образуют базис всех допустимых в IPC правил. Данные условия достаточно естественны и многие из них выглядят как свойства максимальных теорий из канонической модели Крипке для IPC. Кроме того, строится аналогичный базис для правил, допустимых в суперинтуиционистской логике KC –логике закона слабого исключенного третьего.