A criterion for admissibility of rules in the modal system S4 and intuitionistic logic (Q1079558)

This important paper contains a positive solution of the Kuznetsov- Friedman problem on decidability of the set of rules admissible in intuitionistic propositional logic Int. It is known (Harrop 1960, Mints 1968) that Int is structurally incomplete, i.e. there are admissible but inderivable rules. Inference rules are defined as pairs of formulas with propositional parameters \(A(x_ 1,...,x_ n)/B(x_ 1,...,x_ n)\); such a rule is admissible iff Int\(\vdash A(C_ 1,...,C_ n)\) implies Int\(\vdash B(C_ 1,...,C_ n)\) for all formulas \(C_ 1,...,C_ n\). The rule is derivable iff Int\(\vdash A(x_ 1,...,x_ n)\to B(x_ 1,...,x_ n).\) The positive solution of this problem by the author was preceded by his investigation of the same problem for other intermediate and modal logics. Call a logic A-decidable if the set of its admissible rules is decidable. The following logics were proved by the author to be A- decidable: S5 (1979), tabular and pre-tabular logics (1981), extensions of S4.3 (1982), logics of finite slices (1984), S4 and Int (the present paper), Grz (1984, published in 1986). It follows from the results of the paper that the universal first order theories of Lindenbaum algebras for S4 and Int (i.e. of \(F_{\omega}(S4)\) and \(F_{\omega}(Int))\) are decidable (while their first-order theories are not - see the author's paper in Mat. Zametki 37, No.6, 797-802 (1985; Zbl 0593.03041).