On elementary theories of ordinal notation systems based on reflection principles

F. N. Pakhomov

Informatics and Automation, Selected issues of mathematics and mechanics, Tome 289 (2015), pp. 206-226

Résumé

L.D. Beklemishev has recently introduced a constructive ordinal notation system for the ordinal $\varepsilon _0$. We consider this system and its fragments for smaller ordinals $\omega _n$ (towers of $\omega $-exponentiations of height $n$). These systems are based on Japaridze's well-known polymodal provability logic. They are used in the technique of ordinal analysis of the Peano arithmetic $\mathbf {PA}$ and its fragments on the basis of iterated reflection schemes. Ordinal notation systems can be regarded as models of the first-order language. We prove that the full notation system and its fragments for ordinals ${\ge }\,\omega _4$ have undecidable elementary theories. At the same time, the fragments of the full system for ordinals ${\le }\,\omega _3$ have decidable elementary theories. We also obtain results on decidability of the elementary theory for ordinal notation systems with weaker signatures.