×

On propositional quantifiers in provability logic. (English) Zbl 0805.03009

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

MSC:

03B45 Modal logic (including the logic of norms)
03F30 First-order arithmetic and fragments
03B25 Decidability of theories and sets of sentences
PDFBibTeX XMLCite
Full Text: DOI