Axioms of Linear Integer Arithmetic?

58 Views Asked by At

The slides I am reading don't give the axioms of LIA (linear integer arithmetic) instead only give it's signature. I looked on the internet and can't find the axioms of LIA. For the following signature of LIA denoted by $\Sigma_{\mathbb{Z}}$,

$\Sigma_{\mathbb{Z}} := \{ -2,-1,0,1,2,3, ... , ... , -2 \cdot , 2 \cdot , 3 \cdot, .. +,-, >, =\}$

where the intended meaning of $2 \cdot x$ ("$2 \cdot$" is a function symbol of arity 1) is mentioned to be $x + x$.

Now for this signature, I can easily see that the axioms of presbuger arithmetic (i.e. axioms of theory of equality, zero, successor, induction, plus zero and plus successor) carry over. But shouldnt there be additional axioms to put some structure on the $>, - $ and $... , -2 \cdot , 2 \cdot , 3 \cdot, ..$ symbols? If so, what are these axioms? Can someone clarify?