Solvable classes of pseudoprenex formulas

For constructive (intuitionistic) predicate calculus without functional symbols and equality a complete description is derived, in terms of prefixes and signatures, of reduction classes and of classes of pseudoprenex formulas, i.e., formulas representable in form $PM$, where $M$ is a quantifier-free formula and $P$ is a finite sequence of quantifier complexes and expressions $\rceil\rceil$. The operation $L^p$ plays a fundamental role in the construction of solvable classes. From any pseudoprenex formula $A$ this operation constructs, preserving signature, a formula list $\Gamma$ such that $A$ is decidable in the constructive calculus if and only if some formula from $\Gamma$ is decidable in classical calculus. In the paper conditions are formulated sufficient for the carrying out of quantifier $\forall$ from a disjunction and the permutations of quantifiers $\forall$ and $\exists$ to preserve decidability in the constructive calculus. A signature-preserving method for the elimination of positive occurrences of equality is described as well. This method and the conditions mentioned play an important role in the construction of reduction classes. Also examined is the problem of recognition of refutability of pseudoprenex formulas on completely finite Kripke models, i.e., on those Kripke models in which both the set of “time instants” and also the union of objective domains are finite. A complete description in terms of prefixes and signatures is given for classes of pseudoprenex formulas for which the problem of recognition of refutability on completely finite Kripke models is solvable. This description differs essentially from the description of solvable pseudoprenex formulas for constructive predicate calculus.