DOI

We consider positively existentially definable sets in the structure 〈ℤ; 1, +, ⊥〉 It is well known that the elementary theory of this structure is undecidable while the existential theory is decidable. We show that after the extension of the signature with the unary '-' functional symbol, binary symbols for dis-equality ≠ and GCD(·, ·) = d for every fixed positive integer d, every positive existential formula in this extended language is equivalent in ℤ to some positive quantifier-free formula. Then we get some corollaries from the main result. The binary order ≤ and dis-coprimeness ⊥ relations are not positively existentially definable in the structure 〈ℤ; 1, +, ⊥〉. Every positively existentially definable set in the structure 〈N; S, ⊥〉 is quantifier-free definable in 〈N; S, ≠, 0, ⊥〉. We also get a decidable fragment of the undecidable ∀∃-Theory of the structure 〈ℤ; 1, +, ≤, |〉, where | is a binary predicate symbol for the integer divisibility relation.

Язык оригиналаанглийский
Название основной публикацииISSAC 2021 - Proceedings of the 2021 International Symposium on Symbolic and Algebraic Computation
ИздательAssociation for Computing Machinery
Страницы353–360
Число страниц8
ISBN (электронное издание)9781450383820
DOI
СостояниеОпубликовано - 18 июл 2021
СобытиеISSAC 2021 International Symposium on Symbolic and Algebraic Computation - EIMI, Санкт-Петербург, Российская Федерация
Продолжительность: 18 июл 202123 июл 2021
Номер конференции: 46
https://issac-conference.org/2021/

Серия публикаций

НазваниеProceedings of the International Symposium on Symbolic and Algebraic Computation, ISSAC

конференция

конференцияISSAC 2021 International Symposium on Symbolic and Algebraic Computation
Сокращенное названиеISSAC 2021
Страна/TерриторияРоссийская Федерация
ГородСанкт-Петербург
Период18/07/2123/07/21
Сайт в сети Internet

    Области исследований

  • Existential definability, Coprimeness, Quantifier elimination, Decidability, Chinese remainder theorem

    Предметные области Scopus

  • Математика (все)

ID: 84459010