Undecidability of the first-order arithmetic A[P(x), 2x, x + 1]

摘要

It is shown that the first-order arithmetic A[P(x), 2x, x + 1] with two functions 2x, x + 1 and a monadic predicate symbol P(x) is undecidable, by using a kind of two-dimensional finite automata, called finite causal ω2-systems. From this immediately follows R.M. Robinson's result, which says that the monadic second-order theory with two functions 2x, x + 1 is undecidable. This is also considered as an improvement on H. Putnam's result about the undecidability of the first-order arithmetic with addition and a monadic predicate symbol.