On elementary theories of ordinal notation systems based on reflection principles

L.D. Beklemishev has recently introduced a constructive ordinal notation system for the ordinal E > (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 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 a parts per thousand yen omega (4) have undecidable elementary theories. At the same time, the fragments of the full system for ordinals a parts per thousand currency sign omega (3) have decidable elementary theories. We also obtain results on decidability of the elementary theory for ordinal notation systems with weaker signatures