Доказательство теоремы Бельтюкова-Липшица квазиэлиминацией кванторов. I. Определения и НОД-лемма

Данная работа является первой частью нового доказательства разрешимости экзистенциальной теории структуры $\langle\mathrm{Z}; 0, 1,+,-,\leqslant, |\rangle$, где $|$ соответствует двухместному отношению делимости. Разрешимость этой теории была доказана в 1976 г. независимо А.П. Бельтюковым и Л.Липшицем. В 1977 г. В. И.Мартьянов получил эквивалентный результат, рассматривая трехместный предикат НОД вместо отношения делимости (эти предикаты экзистенциально выражаются друг через друга с помощью других символов сигнатуры). В работе вводится понятие алгоритма квазиэлиминации кванторов (квази-ЭК), обобщающее в некотором смысле понятие алгоритма элиминации кванторов, а затем строится алгоритм квази-ЭК для позитивной экзистенциальной теории структуры $\langle\mathrm{Z}_{>0};1, \{a \cdot\}_{a\in\mathrm{Z}_{>0}}, НОД\rangle$. К проблеме разрешимости для этой теории сводится проблема разрешимости для экзистенциальной теории структуры $\langle\mathrm{Z}_{>0};1, +, - , \leqslant, НОД\rangle$. Алгоритм квази-ЭК, осуществляющий такое сведение, будет построен во второй части доказательства. Преобразования формул основаны на обобщении китайской теоремы об остатках для систем вида $НОД(a_i, b_i + x) = d_i$ для всех $i \in [1..m]$, где $a_i$, $b_i$, $d_i$ - целые числа, такие что $a_i \neq 0$, $d_i > 0$.