Abstract:
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.