Research output: Contribution to journal › Article › peer-review
A Proof of Bel’tyukov–Lipshitz Theorem by Quasi-Quantifier Elimination. I. Definitions and GCD-Lemma. / Starchak, M. R. .
In: Vestnik St. Petersburg University: Mathematics, Vol. 54, No. 3, 08.2021, p. 264–272.Research output: Contribution to journal › Article › peer-review
}
TY - JOUR
T1 - A Proof of Bel’tyukov–Lipshitz Theorem by Quasi-Quantifier Elimination. I. Definitions and GCD-Lemma
AU - Starchak, M. R.
N1 - Starchak, M.R. A Proof of Bel’tyukov–Lipshitz Theorem by Quasi-Quantifier Elimination. I. Definitions and GCD-Lemma. Vestnik St.Petersb. Univ.Math. 54, 264–272 (2021). https://doi.org/10.1134/S1063454121030080
PY - 2021/8
Y1 - 2021/8
N2 - This paper is the first part of a new proof of decidability of the existential theory of the structure 〈Z; 0, 1, +, –, ≤, |〉, 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 〈Z>0; 1, {a⋅}a∈Z>0, GCD〉. We reduce to the decision problem for this theory the decision problem for the existential theory of the structure 〈Z; 0, 1, +, –, ≤, GCD〉. 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≠0, di>0.
AB - This paper is the first part of a new proof of decidability of the existential theory of the structure 〈Z; 0, 1, +, –, ≤, |〉, 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 〈Z>0; 1, {a⋅}a∈Z>0, GCD〉. We reduce to the decision problem for this theory the decision problem for the existential theory of the structure 〈Z; 0, 1, +, –, ≤, GCD〉. 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≠0, di>0.
KW - Quantifier elimination
KW - Existential theory
KW - Divisibility
KW - Decidability
KW - Chinese remainder theorem
UR - https://link.springer.com/article/10.1134/S1063454121030080
M3 - Article
VL - 54
SP - 264
EP - 272
JO - Vestnik St. Petersburg University: Mathematics
JF - Vestnik St. Petersburg University: Mathematics
SN - 1063-4541
IS - 3
ER -
ID: 85580319