# Expressiveness of bounded difference constraints with sets

Consider a restricted first-order theory over sets and natural numbers, with only bounded difference predicates such as $x-y<c$ where $c$ is a constant, and universal quantifiers. For instance, we can write $\forall x.(x\in A\rightarrow x+2\in A)$. Notice that predicates such as $x+y<1$ are not allowed.

A formal definition is given as

\begin{array}{l c l} \varphi &::=& \varphi \wedge \varphi \mid \neg \varphi \mid S \subseteq S \mid t\ o\ c \mid t - t\ o\ c \mid t \in S,\\ t &::=& x+c,\\ S &::= & \emptyset \mid S \cup S \mid S^c, \end{array}

where $x$ is an integer variable, $c$ is an integer constant, and $o \in \{\ge, \le, >, <, =\}$.

Formulas are of the form $\forall x_1...\forall x_n.\varphi$.

Is it possible to define the addition predicate $R(x,y,z):=x=y+z$? I suspect not, but do not know how to show this.

• Minor note: Something's wrong with your definition of the meta-variable $S$. Did you mean to allow mentioning of set-valued variables $A,B,C,\dots$? – D.W. Oct 20 '17 at 6:40
• If we disallow the $t \ o \ c$ construct, then one can prove that it's not possible to define the addition predicate. Imagine adding one million to the of each integer variable, and to each element of each set variable. Then every formula that was satisfied by the original values will remain satisfied after this modification. Thus, every predicate definable must have that property. The addition predicate doesn't have that property. – D.W. Oct 20 '17 at 6:46