A proof of Bel’tyukov — Lipshitz theorem by quasi-quantifier elimination. II. The main reduction
Mikhail R. Starchak · Vestnik of Saint Petersburg University Mathematics Mechanics Astronomy · 2021
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.