I'm trying to negate linear inequalities of integers while only using X-or-equal relationships; e.g. $\neg (n \geq 0) = (n \leq -1)$.
While the example with a single variable is trivial, how do you negate a more complex example ?
For instance, is it true that $\neg(n_1 + 3n_2\geq 1) = (n_1 + 3n_2 \leq 0)$ ? Is the formula simply $\neg(\textit{expr} \geq n) = (\textit{expr} \leq n-1)$ ? Thank you.
I'm assuming you have an additional constraint that $n_1,n_2\in \mathbb Z$. If yes, this is fine. If not and your variables may be arbitrary reals, I think a possible way without using the $<$ or $>$ symbols would be:
$$\neg(a_1n_1+b_1n_2\geq c) \equiv \exists x> 0 \textrm{ such that } a_1n_1+b_1n_2+x\leq c.\tag{1}$$
This works in the integer case as well, because $\mathbb Z$ is contained in $\mathbb R$.
This is also a more general negation, because the true negation is actually $$a_1n_1+b_1n_2 < c,$$ which may be alternatively written as the RHS of $(1)$.
What happens when you restrict to $\mathbb Z$ is that your $x$ is at least $1$, so you get
$$a_1n_1+b_1n_2+1\leq c\Rightarrow a_1n_1+b_1n_2\leq c -1 .$$
Possibly of interest and somewhat related: