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

  • $\begingroup$ 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. $\endgroup$ Mar 10, 2015 at 8:45
  • $\begingroup$ 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. $\endgroup$
    – Trung Ta
    Mar 10, 2015 at 8:54
  • 1
    $\begingroup$ 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]$ $\endgroup$ Mar 10, 2015 at 9:03
  • $\begingroup$ 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." $\endgroup$ Mar 10, 2015 at 12:34
  • $\begingroup$ 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))$. $\endgroup$ Mar 10, 2015 at 12:54


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.