As far as I know, formulae involving rationals and basic arithmetic ($+$, $-$, $\cdot$ and $/$) have decidable equality. Is this still the case if we add floor rounding (or integer division)?


Define a "basic formula" by the following grammar (in Backus-Naur form):


$$
\begin{matrix}
e &= &q \\
 &| &v \\
 &| &e + e \\
 &| &e - e \\
 &| &e \cdot e \\
 &| &e / e \\
 \end{matrix}
$$
Here, $q$ stands for rational literals and $v$ for a set of variables.


A valuation is the assignment of a rational number to every variable.
The semantics of such a formula for a given valuation is ordinary arithmetics. Two formulae are semantically equal if they are equal for every allowed valuation. (Division by 0 is not allowed, of course.)
As far as I understand, this notion of equality is decidable. Given two formulas, we essentially multiply by all denominators, apply the distributive law everywhere and then compare summands. We've basically reduced each expression to a normal form where we can compare.


Now, let us add the floor function, which rounds down to the nearest integer. We extend the above definition by:
$$
\begin{matrix}
e &= &\dots \\
 &| &\lfloor e \rfloor \\
 \end{matrix}
$$


Is equality still decidable here? It's not so obvious to me that a well-behaved normal form even exists, since the floor function satisfies some equations such as $\lfloor \lfloor x \rfloor + y \rfloor = \lfloor x \rfloor + \lfloor y \rfloor$, [Hermite's identities](https://en.wikipedia.org/wiki/Hermite%27s_identity) (e.g. $\lfloor x\rfloor + \lfloor x+1/3\rfloor + \lfloor x+2/3\rfloor = \lfloor 3x\rfloor$), and so on.


*Is there still some simple enough algorithm that decides whether two such formulae are equal?*


**Note**: I could have added integer division instead of the floor function as well, but I believe that this wouldn't make a difference.




---


Feel free to add or suggest tags, I'm not so sure whether the question is categorized well.



Is equality of formulas with floor rounding or integer division decidable?
Equality of formulas is undecidable. To prove this it is enough to show that an algorithm for equality of formulas would enable us to determine whether or not a multivariate polynomial with integer coefficients vanishes at at least one integer point, because the latter condition is undecidable according to the negative solution to Hilbert's Tenth Problem.


But the polynomial $f(x)$, where $x$ is a tuple of variables and $f$ has integer coefficients, does not vanish at any integer point if and only if the following equation holds at all integer points $x$: 
$$\Bigl\lfloor\dfrac{1}{1+f(x)^2}\Bigr\rfloor=0.$$


I believe this settles it. However it would be nice to know a simple elegant decidability result for formulas excluding division. 


