On propositional quantifiers in provability logicстатья
Информация о цитировании статьи получена из
Scopus
Статья опубликована в журнале из списка Web of Science и/или Scopus
Дата последнего поиска статьи во внешних источниках: 26 августа 2016 г.
Аннотация: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 ≠ 0.