Разрешимость универсальной теории натуральных чисел со сложением и делимостью

Рассматривается класс всех бескванторных формул, построенных из атомарных формул вида $(x+y=z)$, $(x=1)$ и $(x/y)$, где предикат “|” интерпретируется как отношение делимости неотрицательных целых чисел. Доказана разрешимость множества всех тех формул из рассматриваемого класса, которые истинны хотя бы для одного набора неотрицательных целых значений их переменных. Этот результат эквивалентен разрешимости универсальной теории натуральных чисел со сложением и делимостью. Библ. 5 назв.