The Smetanich constant and finite canonical model method

The method of finite canonical model described by K. Shchütte is applied to the Smetanich logic which determines a new logical constant in the intuitionistic propositional logic (in the sence of P. Novikov's approach). This method allows to prove semantical completeness and finite model property for Smetanich logic simultaneously.