Artemov, Sergej N.; Beklemishev, Lev D. On propositional quantifiers in provability logic. (English) Zbl 0805.03009 Notre Dame J. Formal Logic 34, No. 3, 401-419 (1993). Summary: The first-order theory of the Diagonalizable Algebra of Peano Arithmetic (DA(PA)) represents a natural fragment of provability logic with propositional quantifiers. We prove that the first-order theory of the 0- generated subalgebra of DA(PA) is decidable but not elementary recursive; the same theory, enriched by a single free variable ranging over DA(PA), is already undecidable. This gives a negative answer to the question of the decidability of provability logics for recursive progressions of theories with quantifiers ranging over their ordinal notations. We also show that the first-order theory of the free diagonalizable algebra on \(n\) independent generators is undecidable iff \(n\neq 0\). Cited in 5 Documents MSC: 03B45 Modal logic (including the logic of norms) 03F30 First-order arithmetic and fragments 03B25 Decidability of theories and sets of sentences Keywords:first-order theory; Diagonalizable Algebra of Peano Arithmetic; provability logic; propositional quantifiers; 0-generated subalgebra; recursive progressions of theories with quantifiers ranging over their ordinal notations; free diagonalizable algebra PDFBibTeX XMLCite \textit{S. N. Artemov} and \textit{L. D. Beklemishev}, Notre Dame J. Formal Logic 34, No. 3, 401--419 (1993; Zbl 0805.03009) Full Text: DOI