A wild model of linear arithmetic and discretely ordered modules

Linear arithmetics are extensions of Presburger arithmetic ( Pr ) by one or more unary functions, each intended as multiplication by a fixed element (scalar), and containing the full induction schemes for their respective languages. In this paper, we construct a model M of the 2‐linear arithmetic LA2 (linear arithmetic with two scalars) in which an infinitely long initial segment of “Peano multiplication” on M is ⌀ ‐definable. This shows, in particular, that LA2 is not model complete in contrast to theories LA1 and LA0=Pr that are known to satisfy quantifier elimination up to disjunctions of primitive positive formulas. As an application, we show that M , as a discretely ordered module over the discretely ordered ring generated by the two scalars, does not have the NIP, answering negatively a question of Chernikov and Hils.