Definable subsets of $\mathbb N$ in the language of Presburger arithmetic are exactly the eventually periodic sets and quantifier free part corresponds to Integer Programming with linear inequalities and variations lead to mixed integer linear programming, convex integer programming with convex constraints. What about

  1. definable subsets of $\mathbb N$ in the language of Skolem arithmetic and

  2. would it be sensible to seek programming constructs that with 'decidable portions of Skolem' leads to (if I am not wrong then atomic formulae here might be of form $a\prod_{i=1}^nx_i^{b_i}\leq b$ or $a\prod_{i=1}^nx_i^{b_i}=b$)?

My background is not logic and not sure if I make sense however if there is reasonable way to salvage the post it will be nice. I am trying to see if fixed dimension linear integer programming that runs in polynomial time has an analogy in Skolem arithmetic where variable addition is disallowed?


$\def\mr{\mathrm}$As it happens, quantifier elimination for Skolem arithmetic came up recently in my research. The concise description is that every formula $\phi(x_1,\dots,x_k)$ is in $(\mathbb N^{>0},{\cdot})$ equivalent to a Boolean combination of formulas expressing $$\tag1\bigl|\{p\in\mathbb P:\psi(v_p(x_1),\dots,v_p(x_k))\}\bigr|\ge n,$$ where $\psi(y_1,\dots,y_k)$ is a formula of Presburger arithmetic, and $n\in\mathbb N$.

In the special case of formulas in one variable with parameters that you are interested in, this boils down to the following: definable subsets are Boolean combinations of sets defined by

  • $v_q(x)=n$,

  • $v_q(x)\equiv a\pmod m$,

  • $\bigl|\{p\in\mathbb P:v_p(x)=n\}\bigr|\ge b$,

  • $\bigl|\{p\in\mathbb P:v_p(x)\ge n,v_p(x)\equiv a\pmod m\}\bigr|\ge b$,

for some $q\in\mathbb P$, $n,b\in\omega$, $0\le a<m<\omega$.

That all definable relations in $(\mathbb N^{>0},{\cdot})$ are equivalent to Boolean combinations of (1) follows from the results of Mostowski [1]. I will sketch how to prove the other direction, that all sets of the form (1) are first-order definable.

Using $\cdot$, we can define the divisibility, coprimeness, and primality predicates as $$\begin{align*} x\mid y&\iff\exists z\,(y=x\cdot z),\\ x\perp y&\iff\forall z\,(z\mid x\land z\mid y\to z=1),\\ \mr{Prime}(x)&\iff x\ne1\land\forall z\,(z\mid x\to z=1\lor z=x). \end{align*}$$ Then, we can define the set of powers of a prime by $$\mr{Power}(p,x)\iff\mr{Prime}(p)\land\forall z\,(z\perp p\to z\perp x).$$ Finally, we can define for a given $x$ and a prime $p$ the power of $p$ that appears in the factorization of $x$ by $$\mr{Val}(p,x,y)\iff\mr{Power}(p,y)\land\exists z\,(x=y\cdot z\land z\perp p).$$ Now, for each prime $p$, $(\{x:\mr{Power}(p,x)\},{\cdot})$ is a model of Presburger arithmetic (which I assume to be formulated in a language with just a single binary function symbol $+$). Thus, if $\psi(y_1,\dots,y_k)$ is a formula of Presburger arithmetic, let $\psi^p(y_1,\dots,y_k)$ (with an extra free variable $p$) denote the formula of Skolem arithmetic obtained by replacing all occurrences of $+$ with $\cdot$, and relativizing all quantifiers to $\{x:\mr{Power}(p,x)\}$. Then (1) is defined by the formula $$\exists^{\ge n}p\,(\mr{Prime}(p)\land\exists y_1,\dots,y_k\,(\mr{Val}(p,x_1,y_1)\land\dots\land\mr{Val}(p,x_k,y_k)\land\psi^p(y_1,\dots,y_k))).$$

EDIT: I defined $\psi^p$ for formulas written in the language with $+$ only to keep the definition succinct, but in practice, it is more convenient to define it directly for a richer language: specifically, we may translate the constants $0$ and $1$ to $1$ and $p$, respectively, and $x\le y$ to $x\mid y$.

To put it differently, any Presburger formula $\psi(\vec y)$ is equivalent to a Boolean combination of integer inequalities $n+\sum_{i<k}n_iy_i\le m+\sum_{i<k}m_iy_i$, and congruences $y_i\equiv a\pmod m$. We may translate the former to $p^n\prod_{i<k}y_i^{n_i}\mid p^m\prod_{i<k}y_i^{m_i}$, and the latter to $\exists z\,(y_i=p^az^m)$.


[1] Andrzej Mostowski, On direct products of theories, Journal of Symbolic Logic 17 (1952), no. 1, pp. 1–31.

  • 1
    $\begingroup$ Where can I find more about the proof of your answer? $\endgroup$ – Erfan Khaniki Nov 30 '18 at 9:35
  • 1
    $\begingroup$ 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})$. ... $\endgroup$ – Emil Jeřábek Dec 2 '18 at 8:13
  • 1
    $\begingroup$ 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. $\endgroup$ – Emil Jeřábek Dec 3 '18 at 9:28
  • 1
    $\begingroup$ @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 ... $\endgroup$ – Emil Jeřábek Feb 7 at 10:08
  • 1
    $\begingroup$ ... “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. $\endgroup$ – Emil Jeřábek Feb 7 at 10:17

The fundamental theorem of arithmetic states that the monoid of positive integers under multiplication is a free commutative monoid on an infinite set of generators, the prime numbers.

So you get whatever is definable in such a free commutative monoid.


You can define $x=1$ by $(\forall y)x\cdot y = y$. Then we can define "$p$ is prime" by $p=x\cdot y\to x=1\vee y=1\vee x=p\vee y=p$. Then we can define "$r$ is a product of two primes" by "$(\exists p)(\exists q)(x=p\cdot q$, $p$ is prime, $q$ is prime)". And you can define things like "$s$ is a product $p^2q^{15}r^{12}$ where $p$, $q$, $r$ are prime".

However you can't define $x\le y$, which you may want for your Integer Programming application. Indeed if you add $\le$ you get the same definable sets as in all of first-order arithmetic, as described by Alexis Bès.

  • $\begingroup$ Is there programming construct similar to Integer Programming? $\endgroup$ – 1.. Nov 30 '18 at 5:53
  • $\begingroup$ Can you define “power of a semiprime”, i.e. $\{(pq)^k: p,q\ \text{prime},\ k\in\mathbf{N}\}$? It makes sense in a free commutative monoid but I don’t think it’s definable in Skolem arithmetic. $\endgroup$ – Matt F. Nov 30 '18 at 6:06
  • $\begingroup$ I thought you were reasoning more semantically....I don’t think you can define it in a first-order way in the theory of a free commutative monoid. $\endgroup$ – Matt F. Nov 30 '18 at 6:11
  • $\begingroup$ @MattF. isomorphic structures satisfy the same first-order sentences... and all free commutative monoids on countably infinitely many generators are isomorphic to $(\mathbb N,\cdot)$. $\endgroup$ – Bjørn Kjos-Hanssen Nov 30 '18 at 6:13
  • 1
    $\begingroup$ @Freeman. Proposition 45 says the theory is undecidable. In Theorem 43, the order is restricted only to primes. $\endgroup$ – Emil Jeřábek Nov 30 '18 at 14:04

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.