×

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)
PDF BibTeX XML Cite