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.
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)