Abstract
In this paper we consider a theory of integers with the successor function, divisibility predicates, equality and a transitive closure operator. The order relation can be expressed in this theory using the transitive closure operator.
We prove that given a formula with the transitive closure operator on a single pair of variables one can effectively eliminate it.
Article PDF
Similar content being viewed by others
Avoid common mistakes on your manuscript.
References
A. Aho, J. Ulman, Proc. of 6th Symp. on Principles of Programming Languages, pp. 110–119 (1979).
G. S. Boolos and R. C. Jefferey, Computability and Logic (Cambridge University Press, 1994).
A. Church, J. of Symbolic Logic 1, 40–41 (1936).
A. Church, Amer. J. of Math. 58, 345–363 (1936).
M. Presburger, Comptes Rendus du I congres de Mathematiciens des Pays Slaves, pp. 92–101 (1929).
J. B. Rosser, J. of Symbolic Logic 1, 87–91 (1936).
A. Zolotov, Vestnik TvGU. Seriya Prikl. Mat. 28, 101–117 (2013).
Author information
Authors and Affiliations
Corresponding author
Rights and permissions
About this article
Cite this article
Zolotov, A.S. On decidability of the theory with the transitive closure operator. Lobachevskii J Math 36, 434–440 (2015). https://doi.org/10.1134/S1995080215040186
Received:
Published:
Issue Date:
DOI: https://doi.org/10.1134/S1995080215040186