On propositional quantifiers in provability logic.
Sergei Nikolaevich Artemov, Lev D. Beklemishev · Notre Dame Journal of Formal Logic · 1993
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 O-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 Φ 0.