Decidability of the existential theory of the set of natural numbers with order, divisibility, power functions, power predicates, and constants

Abstract:

We construct an algorithm to test if a system of conditions of the types $\mu < \eta ,\mu /\eta ,\mu = {\eta ^a},{P_a}(\mu ),\neg (\mu < \eta ),\neg (\mu /\eta ),\neg (\mu = {\eta ^a})$, and $\neg ({P_a}(\mu ))$ has a solution in natural numbers. ($a \in N$, and ${P_a}$ denotes the set $\{ {n^a}:n \in N\}$.)