# zbMATH — the first resource for mathematics

Problems of substitution and admissibility in the modal system Grz and in intuitionistic propositional calculus. (English) Zbl 0709.03009
Summary: 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 $${\mathcal F}_{\omega}(Grz)$$ extended in signature by adding constants for the free generators. As corollaries we obtain: (a) there exists an algorithm for the recognition of admissibility of rules with parameters (hence also without them) in the modal system Grz, (b) the substitution problem for Grz and for the intuitionistic calculus H is decidable, (c) intuitionistic propositional calculus H is decidable with respect to admissibility (a positive solution of Friedman’s problem). A semantical criterion for the admissibility of rules of inference in Grz is given.

##### MSC:
 03B45 Modal logic (including the logic of norms) 03B20 Subsystems of classical logic (including intuitionistic logic) 03B25 Decidability of theories and sets of sentences
Full Text: