Timeline for What are the definable sets in Skolem arithmetic?
Current License: CC BY-SA 4.0
23 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Feb 7, 2021 at 10:17 | comment | added | Emil Jeřábek | ... “Skolem-closed products” (this refers to Skolem functions, not to Skolem arithmetic), which I originally discovered in connection with a follow-up to mathoverflow.net/questions/119375/… . It came to my attention that some form of this construction was meanwhile published by Derakhshan and Macintyre, so that’s unfortunately another thing that I will have to read first. This is all becoming more effort than what the modest end-result is worth, so that’s why I keep putting it off. | |
| Feb 7, 2021 at 10:08 | comment | added | Emil Jeřábek | @Alex No, I haven’t yet written up the results (whose primary goal was generalization of arxiv.org/abs/1803.05797 to Skolem arithmetic). That is, I have written it up in the form of personal notes, but not ready for publication. One thing that delayed it was indeed that I became aware of Cégielski’s work, which is unfortunately written in an obscure language, and I have not yet found the mental strength to decipher how much of it is relevant. Note that I do not need QE per se, but rather a description of models of Skolem arithmetic. The description I am using is in terms of ... | |
| Feb 6, 2021 at 16:15 | comment | added | Alex Kruckman | Hi Emil, did you ever end up writing up your results on Skolem arithmetic? In the comments above, you ask for another reference for the statement on quantifier elimination. Presumably you're aware of Cegielski's QE result in "Theorie elementaire de la multiplication des entiers naturels"? | |
| Jan 31, 2021 at 9:33 | comment | added | Emil Jeřábek | No. The $y_i$ variables in the Skolem formula denote powers of $p$ whose exponents correspond to the $y_i$ variables in the Presburger formula. | |
| Jan 31, 2021 at 8:23 | comment | added | Turbo | @EmilJeřábek Should it be $p^n\prod_{i<k}p^{y_in_i}|p^m\prod_{i<k}p^{y_im_i}$ and $\exists z\mbox{ }p^{y_i}=p^az^m$? | |
| Dec 3, 2018 at 9:28 | comment | added | Emil Jeřábek | If you are asking if there is an interpretation of Skolem arithmetic in Presburger arithmetic, the answer is no, because Presburger arithetic is an NIP theory, but Skolem arithmetic is not. | |
| Dec 2, 2018 at 20:15 | comment | added | Turbo | @EmilJeřábek I am just asking just as $\cdot$ was converted to $+$ making it a first order Skolem formula is there a way to make $+$ to $\cdot$ without blowing up too much. I do not see one. The reason I ask is there are integer programming tools we can use in Presburger. We lack that in Skolem. | |
| Dec 2, 2018 at 13:09 | comment | added | Emil Jeřábek | I am sorry, but I don’t understand what you are asking. What do you mean by “go from Skolem to Presburger”? And what do you mean by “formula is decidable”? Under any sensible interpretation I can think of, all formulas are decidable in Skolem arithmetic. | |
| Dec 2, 2018 at 10:27 | comment | added | Turbo | @EmilJeřábek Thank you. I see so we can always go from Presburger to Skolem. Is it possible to go from Skolem to Presburger when the formula is decidable? Or is it meaningless? | |
| Dec 2, 2018 at 9:22 | history | edited | Emil Jeřábek | CC BY-SA 4.0 |
added 642 characters in body
|
| Dec 2, 2018 at 8:17 | comment | added | Emil Jeřábek | ... One can take some shortcuts: this is equivalent to $x_1^{\prime a}x_2^{\prime b}\mid p^{c-1}$. (Also, the formula can be written more efficiently so that its length is linear in the length of $a,b,c$ in binary.) | |
| Dec 2, 2018 at 8:13 | comment | added | Emil Jeřábek | First, you have to rewrite the formula so that it uses only addition: for example, as $\exists u\,\exists z\,(u+u\ne u\land\forall v,w\,(v+w=u\to v+v=v\lor w+w=w)\land\underbrace{x'_1+\dots+x'_1}_a+\underbrace{x'_2+\dots+x'_2}_b+z=\underbrace{u+\dots+u}_{c-1})$. Then, $\psi^p$ is $\exists u\,\exists z\,(\mr{Power}(p,u)\land\mr{Power}(p,z)\land u\cdot u\ne u\land\forall v,w\,(\mr{Power}(p,v)\land\mr{Power}(p,w)\land v\cdot w=u\to v\cdot v=v\lor w\cdot w=w)\land\underbrace{x'_1\cdot\dots\cdot x'_1}_a\cdot\underbrace{x'_2\cdot\dots\cdot x'_2}_b\cdot z=\underbrace{u\cdot\dots\cdot u}_{c-1})$. ... | |
| Dec 2, 2018 at 4:40 | comment | added | Turbo | @EmilJeřábek Thank you for the answer. Just to understand relativization if $\psi(x_1',x_2')$ is $ax_1'+bx_2'<c$ then what is $\psi^p(x_1',x_2')$ explicitly? Also I made a slight update. If it makes sense and if it is possible you may possibly update accordingly. | |
| Dec 2, 2018 at 4:16 | vote | accept | Turbo | ||
| Dec 2, 2018 at 4:03 | vote | accept | Turbo | ||
| Dec 2, 2018 at 4:05 | |||||
| Dec 1, 2018 at 5:29 | vote | accept | Turbo | ||
| Dec 2, 2018 at 0:17 | |||||
| Nov 30, 2018 at 20:23 | comment | added | Erfan Khaniki | @EmilJeřábek, Thank you very much for the sketch and the reference. | |
| Nov 30, 2018 at 14:51 | comment | added | user44143 | Nice answer. In case anyone wants an example of the fourth bulleted formula, we can define the set of $x$ such that “there are at least 7 primes $p$ for which $x$ can be written as $p^{8k+9}q$ with $q$ relatively prime to $p$”. | |
| Nov 30, 2018 at 13:45 | comment | added | Emil Jeřábek | I added a sketch of the easier part of the characterization. | |
| Nov 30, 2018 at 13:44 | history | edited | Emil Jeřábek | CC BY-SA 4.0 |
Include more details
|
| Nov 30, 2018 at 12:33 | comment | added | Emil Jeřábek | Well, my work (which is mostly concerned with a definable variant of the Mostowski-Feferman-Vaught theorem, and rigid models of Skolem arithmetic) is not yet written up. If you find another reference for the statement on quantifier elimination, I would be actually interested to see it. | |
| Nov 30, 2018 at 9:35 | comment | added | Erfan Khaniki | Where can I find more about the proof of your answer? | |
| Nov 30, 2018 at 9:29 | history | answered | Emil Jeřábek | CC BY-SA 4.0 |