A proof of Bel’tyukov - Lipshitz theorem by quasi-quantifier elimination. II. The main reduction
DOI:
https://doi.org/10.21638/spbu01.2021.406Abstract
This paper is the second part of a new proof of the Bel’tyukov - Lipshitz theorem, which states that the existential theory of the structure is decidable. We construct a quasi-quantifier elimination algorithm (the notion was introduced in the first part of the proof) to reduce the decision problem for the existential theory of to the decision problem for the positive existential theory of the structure 0; 1, {a·}a∈Z>0 , GCD>. Since the latter theory was proved decidable in the first part, this reduction completes the proof of the theorem. Analogues of two lemmas of Lipshitz’s proof are used in the step of variable isolation for quasi-elimination. In the quasi-elimination step we apply GCD-Lemma, which was proved in the first part.Keywords:
quantifier elimination, existential theory, divisibility, decidability, Chinese remainder theorem
Downloads
Download data is not yet available.
References
Литература
1. Бельтюков А.П. Разрешимость универсальной теории натуральных чисел со сложением и делимостью. Записки научных семинаров ЛОМИ 60, 15–28 (1975).
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. Старчак М.Р. Доказательство теоремы Бельтюкова - Липшица квазиэлиминациейкванторов. I. Определения и НОД-лемма. Вестник Санкт-Петербургского университета. Математика. Механика. Астрономия 8 (66), вып. 3, 455–466 (2021). https://doi.org/10.21638/spbu01.2021.307
4. 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
5. von zur Gathen J., Sieveking M. A bound on solutions of linear integer equalities and inequalities. Proceedings of the American Mathematical Society 72, iss. 1, 155–158 (1978). https://doi.org/10.2307/2042554
6. Barth D., Beck M., Dose T., Glaßer C., Michler L., Technau M. Emptiness problems for integer circuits. Electronic Colloquium on Computational Complexity, TR17-012 (2017). Доступно на: https://eccc.weizmann.ac.il/report/2017/012/ (дата обращения: 25.08.2021).
7. Mostowski A. On direct products of theories. The Journal of Symbolic Logic 17, iss. 1, 1–31 (1952). https://doi.org/10.2307/2267454
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. Starchak M.R. 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 (66), iss. 3, 455–466 (2021). https://doi.org/10.21638/spbu01.2021.307 (In Russian) [Engl. transl.: Vestnik St. Petersb. Univ. Math. 54, iss. 3, 264–272 (2021). https://doi.org/10.1134/S1063454121030080].
4. 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
5. von zur Gathen J., Sieveking M. A bound on solutions of linear integer equalities and inequalities. Proceedings of the American Mathematical Society 72, iss. 1, 155–158 (1978). https://doi.org/10.2307/2042554
6. Barth D., Beck M., Dose T., Glaßer C., Michler L., Technau M. Emptiness problems for integer circuits. Electronic Colloquium on Computational Complexity, TR17-012 (2017). Available at: https://eccc.weizmann.ac.il/report/2017/012/ (accessed: August 25, 2021).
7. Mostowski A. On direct products of theories. The Journal of Symbolic Logic 17, iss. 1, 1–31 (1952). https://doi.org/10.2307/2267454
Downloads
Published
2022-01-04
How to Cite
Starchak, M. R. (2022). A proof of Bel’tyukov - Lipshitz theorem by quasi-quantifier elimination. II. The main reduction. Vestnik of Saint Petersburg University. Mathematics. Mechanics. Astronomy, 8(4), 608–619. https://doi.org/10.21638/spbu01.2021.406
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.
