# zbMATH — the first resource for mathematics

The universal theory of the free pseudoboolean algebra $$F_ \omega{}(H)$$ in the signature extended by constants for free generators. (English) Zbl 0767.03007
Algebra, Proc. Int. Conf. Memory A. I. Mal’cev, Novosibirsk/USSR 1989, Contemp. Math. 131, Pt. 3, 645-656 (1992).
[For the entire collection see Zbl 0745.00034.]
H. Friedman [J. Symb. Logic 40, 113-129 (1975; Zbl 0318.02002)] has raised the problem of the existence of an algorithm recognizing admissibility of inferential rules in Heyting’s intuitionistic propositional calculus $$H$$. Using special intuitionistic Kripke models, the author solves a generalization of Friedman’s problem and proves the algorithmic solvability of logical equations in $$H$$. An algebraic corollary of these results is the decidability of the theory in the title.
##### MSC:
 03B25 Decidability of theories and sets of sentences 08B20 Free algebras 06D20 Heyting algebras (lattice-theoretic aspects) 03G10 Logical aspects of lattices and related structures 03B20 Subsystems of classical logic (including intuitionistic logic)