Abstract

Questions connected with the admissibility of rules of inference and the solvability of the substitution problem for modal and intuitionistic logic are considered in an algebraic framework. The main result is the decidability of the universal theory of the free modal algebra imageω extended in signature by adding constants for free generators. As corollaries we obtain: there exists an algorithm for the recognition of admissibility of rules with parameters in the modal system Grz, the substitution problem for Grz and for the intuitionistic calculus H is decidable, intuitionistic propositional calculus H is decidable with respect to admissibility . A semantical criterion for the admissibility of rules of inference in Grz is given