Spectra and satisfiability for logics with successor and a unary function
Arthur Milchior · Mathematical logic quarterly · 2018
Abstract We investigate the expressive power of two logics, both with the successor function: first‐order logic with an uninterpreted function, and existential monadic second order logic—that is first‐order logic over words—, with multiplication by a constant b . We prove that all b ‐recognizable sets are spectra of those logics. Furthermore, it is proven that some encoding of the set of halting times of a non‐deterministic 2‐counter automaton is also a spectrum. This yields undecidability of the finite satisfiability problem for those logics. Finally, it is shown that first‐order logic with one uninterpreted function and successor can encode quickly increasing functions, such as the Knuth's up‐arrows.