The Use Of The Transitive Closure Operator On Formulas With A Single Successor Function And Divisibility Predicates

We investigate transitive closure operator on formulas with successor function and divisibility predicates. We prove that transitive closure operator on two or more pairs of vaiables makes theory undecidable. We build equivalent analog without transitive closure operator for fomulas containing only transitive closure operator on one pair of variables.