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?



What are the definable sets in Skolem arithmetic?
$\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)$.


**Reference:**


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


