I always work with these two and use it with no distinction, but I am probably wrong.
I mean, are their signatures the same? And their axioms? I know that, for instance, the quantifier elimination procedure (Cooper) is the same for both, so that gives me strong evidence that they must be the same, but I cannot find a comparison of PA and LIA.
Which is the difference between them? The only difference I can think about is that LIA also includes the negation (while PA only talks about +). If this is so, which is the point of having two so similar theories?
Thanks!
Seems like, in theory, it is proper to distinguish them both where PA (proved by Presburger in 1929) is only related to naturals and LIA also includes integers. This way, in PA negation is a binary operation, while in LIA is unary.
However, they are both usually confused, and PA is used to refer to LIA. This is so because, essentially, $\Sigma_\mathbb{Z}$-formulae can be reduced to $\Sigma_\mathbb{N}$-formulae: therefore, since PA is decidable, the theory of negative and positive integers (LIA) is also decidable via rewriting of formulae into $\Sigma_\mathbb{N}$-formulae.
This can be seen in Bradley & Manna, Calculus of Computation, pg 76.