A proof of Bel’tyukov-Lipshitz theorem by quasi-quantifier elimination. I. Definitions and GCD-lemma
DOI:
https://doi.org/10.21638/spbu01.2021.307Abstract
This paper is the first part of a new proof of decidability of the existential theory of the structure , where | corresponds to the binary divisibility relation. The decidability was proved independently in 1976 by A. P. Bel’tyukov and L. Lipshitz. In 1977, V.I. Mart’yanov proved an equivalent result by considering the ternary GCD predicate instead of divisibility (the predicates are interchangeable with respect to existential definability). Generalizing in some sense the notion of quantifier elimination (QE) algorithm, we construct a quasi-QE algorithm to prove decidability of the positive existential theory of the structure <...>. We reduce to the decision problem for this theory the decision problem for the existential theory of the structure <...>. A quasi-QE algorithm, which performs this reduction, will be constructed in the second part of the proof. Transformations of formulas are based on a generalization of the Chinese remainder theorem to systems of the form GCD(ai, bi +x) = di for every i [1..m], where ai, bi, di are some integers such that ai 6 = 0, di > 0.Keywords:
quantifier elimination, existential theory, divisibility, decidability, Chinese remainder theorem
Downloads
Download data is not yet available.
References
Литература
1. Бельтюков А.П. Разрешимость универсальной теории натуральных чисел со сложением и делимостью. Записки научных семинаров ЛОМИ 60, 15–28 (1976).
2. Lipshitz L. The Diophantine problem for addition and divisibility. Transactions of the American Mathematical Society 235, 271–283 (1978). https://doi.org/10.1090/S0002-9947-1978-0469886-1
3. Мартьянов В.И. Универсальные расширенные теории целых чисел. Алгебра и логика 16 (5), 588–602 (1977).
4. Lipshitz L. Some remarks on the Diophantine problem for addition and divisibility. Bull. Soc. Math. Belg. Ser. B 33, iss. 1, 41–52 (1981).
5. Lechner A., Ouaknine J., Worrell J. On the complexity of linear arithmetic with divisibility. Proceedings of the 30th Annual ACM / IEEE Symposium on Logic in Computer Science (LICS), 667–676 (2015). https://doi.org/10.1109/LICS.2015.67
6. Weispfenning V. The complexity of linear problems in fields. Journal of Symbolic Computation 5, iss. 1–2, 3–27 (1988). https://doi.org/10.1016/S0747-7171(88)80003-8
7. Gu´epin F., Haase C., Worrell J. On the existential theories of B¨uchi arithmetic and linear p-adic fields. Proceedings of the 34th Annual ACM / IEEE Symposium on Logic in Computer Science (LICS), 1–10 (2019). https://doi.org/10.1109/LICS.2019.8785681
8. Schmid H. L., Mahler K. On the Chinese remainder theorem. Mathematische Nachrichten 18, 120–122 (1958).
References
1. Bel’tyukov A.P. Decidability of the universal theory of the natural numbers with addition and divisibility. Zapiski Nauchnyh Seminarov LOMI 60, 15–28 (1976). (In Russian)
2. Lipshitz L. The Diophantine problem for addition and divisibility. Transactions of the American Mathematical Society 235, 271–283 (1978). https://doi.org/10.1090/S0002-9947-1978-0469886-1
3. Mart’yanov V.I. Universal extended theories of integers. Algebra i Logika 16 (5), 588–602 (1977). (In Russian)
4. Lipshitz L. Some remarks on the Diophantine problem for addition and divisibility. Bull. Soc. Math. Belg. Ser. B 33, iss. 1, 41–52 (1981).
5. Lechner A., Ouaknine J., Worrell J. On the complexity of linear arithmetic with divisibility. Proceedings of the 30th Annual ACM / IEEE Symposium on Logic in Computer Science (LICS), 667–676 (2015). https://doi.org/10.1109/LICS.2015.67
6. Weispfenning V. The complexity of linear problems in fields. Journal of Symbolic Computation 5, iss. 1–2, 3–27 (1988). https://doi.org/10.1016/S0747-7171(88)80003-8
7. Gu´epin F., Haase C., Worrell J. On the existential theories of B¨uchi arithmetic and linear p-adic fields. Proceedings of the 34th Annual ACM / IEEE Symposium on Logic in Computer Science (LICS), 1–10 (2019). https://doi.org/10.1109/LICS.2019.8785681
8. Schmid H. L., Mahler K. On the Chinese remainder theorem. Mathematische Nachrichten 18, 120–122 (1958).
Downloads
Published
2021-09-26
How to Cite
Starchak, M. R. (2021). A proof of Bel’tyukov-Lipshitz theorem by quasi-quantifier elimination. I. Definitions and GCD-lemma. Vestnik of Saint Petersburg University. Mathematics. Mechanics. Astronomy, 8(3), 455–466. https://doi.org/10.21638/spbu01.2021.307
Issue
Section
Mathematics
License
Articles of "Vestnik of Saint Petersburg University. Mathematics. Mechanics. Astronomy" are open access distributed under the terms of the License Agreement with Saint Petersburg State University, which permits to the authors unrestricted distribution and self-archiving free of charge.
