# Presburger arithmetic and finite model property

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:

1. Does Presburger arithmetic has finite model property?

2. 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$$

• I do not understand question 2. First, what do you mean by SAT? Second, do you mean a generic formula or the formula you write? Third, the formula you write is not a closed formula, so it makes to sense to speak about models of that formula. Moreover, as I read it, the formula you write implies $\forall x\ x>0$, so it never satisfied. Please, clarify. Mar 10, 2015 at 8:45
• Hi, for SAT, I mean "satisfiable" and my question 2 is for this particular formula. For your last point, I think you mean validity. This formula is invalid, but it is Satisfiable. Mar 10, 2015 at 8:54
• OK. Then the formula you write is not satisfiable. N.B. I read it as $\forall x\ \big[~ x>0 ~\wedge ~ y \ge 0 ~ \wedge ~ z \ge 0 ~ \wedge ~ x=y+z\big]$ Mar 10, 2015 at 9:03
• See Heinz-Dieter Ebbinghaus & Jörg Flum, Finite Model Theory (2nd ed 1999) : Ch.5. Satisfiabi!ity in the Finite, page 95-on, for some results, e.g. : "any satisfiable universal sentence has a finite model." Mar 10, 2015 at 12:34
• If by finite model property for a class $\Phi$ of sentences we asks "whether every satisfiable sentence of $\Phi$ has a finite model", if $\Phi$ is the class of axioms of Presburger arithmetic, I think not : consider the domain with only $0$ and $1$. $1=s(0)$ but who is the successor of $1$ ? Not $0$, by axiom : $\forall x \lnot (0=s(x))$. Mar 10, 2015 at 12:54