I'm learning about model theory and first order logic. Recently, I read about finite model property and Presburger arithmetic, and I have two questions about them:
Does Presburger arithmetic has finite model property?
Given a Presburger formula. Clearly, it is SAT. Does it have finite number of models?
$$ \forall x.~ x>0 ~\wedge ~ y \ge 0 ~ \wedge ~ z \ge 0 ~ \wedge ~ x=y+z $$