On elementary theories of ordinal notation systems based on reflection principles (Q281010)

There are several different ``natural'' ordinal systems for the ordinals below \(\varepsilon_0\) [\textit{G. Lee}, Ann. Pure Appl. Logic 147, No. 1--2, 48--70 (2007; Zbl 1121.03080)] which are of interest in the proof-theoretic analysis of Peano arithmetic. In [Arch. Math. Logic 42, 515--552 (2003; Zbl 1026.03041); Ann. Pure App. Logic 12, 103--123 (2004; Zbl 1048.03045)], \textit{L. D. Beklemishev} has introduced a constructive ordinal notation system for the ordinal \(\varepsilon_0\). In the paper under review, this system and its fragments for smaller ordinals \(\omega_n\) (towers of \(\omega\)-exponentiations of height \(n\)) are considered. These systems are based on polymodal provability logic \textbf{GLP}. It is proved that the full system and its fragments for ordinals \(\geq \omega_4\) have undecidable elementary theories. Further, the fragments of the full system for ordinals \(\leq \omega_3\) have decidable elementary theories. At the end, the decidability of the elementary theory for ordinal notation systems with weaker signatures is proved.