Константа Сметанича и метод конечной канонической модели

Метод конечной канонической модели, разработанный К. Шютте, применяется к так называемой логике Сметанича, определяющей новую логическую константу в интуиционистской пропозициональной логике. Это позволяет одновременно доказать семантическую полноту в классе соответствующих моделей Крипке и финитную аппроксимируемость логики Сметанича.