Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Research › peer-review
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.
| Original language | English |
|---|---|
| Title of host publication | ISSAC 2021 - Proceedings of the 2021 International Symposium on Symbolic and Algebraic Computation |
| Publisher | Association for Computing Machinery |
| Pages | 353–360 |
| Number of pages | 8 |
| ISBN (Electronic) | 9781450383820 |
| DOIs | |
| State | Published - 18 Jul 2021 |
| Event | ISSAC 2021 International Symposium on Symbolic and Algebraic Computation - EIMI, Санкт-Петербург, Russian Federation Duration: 18 Jul 2021 → 23 Jul 2021 Conference number: 46 https://issac-conference.org/2021/ |
| Name | Proceedings of the International Symposium on Symbolic and Algebraic Computation, ISSAC |
|---|
| Conference | ISSAC 2021 International Symposium on Symbolic and Algebraic Computation |
|---|---|
| Abbreviated title | ISSAC 2021 |
| Country/Territory | Russian Federation |
| City | Санкт-Петербург |
| Period | 18/07/21 → 23/07/21 |
| Internet address |
ID: 84459010