4

For any first-order formula $X$ in the first-order language $\langle 0, S, \le\rangle$ (possibly with free variables) does there necessarily exist another open formula $Y$ such that the equivalence $X \equiv Y$ is true on the set of all nonnegative integer numbers?

  • 1
    $Y = X\land X?$ – bof Jan 05 '17 at 23:58
  • @bof Depending on how complicated $X$ is, that isn't an open formula. – Noah Schweber Jan 06 '17 at 00:15
  • @NoahSchweber How can $X$ be an open formula and $X\land X$ not an open formula? – bof Jan 06 '17 at 00:24
  • @bof Where was $X$ asserted to be open? (I read "another open formula $Y$" as "another formula $Y$, which is open," - note that $X$ itself was only described as a "first-order formula".) – Noah Schweber Jan 06 '17 at 00:26
  • @NoahSchweber "another open formula" – bof Jan 06 '17 at 00:27
  • @bof See the edit to my comment. The OP should definitely clarify, but I'm pretty sure that's what this is asking. – Noah Schweber Jan 06 '17 at 00:27
  • @NoahSchweber Seemed like a silly question anyway. $X\land x=x$ is certainly an open formula and is logically equivalent to $X.$ – bof Jan 06 '17 at 00:31
  • @bof Only if $X$ itself is open. – Noah Schweber Jan 06 '17 at 00:32
  • @NoahSchweber An open formula is a formula that contains at least one free variable. Perhaps you are thinking of a quantifier-free formula? – bof Jan 06 '17 at 00:35
  • @bof That's not universally true - indeed, the definition I learned was that open = quantifier free. For a usage of this, see page 99 of this book. This is also how "open" is used in the study of models of arithmetic ("open induction"). – Noah Schweber Jan 06 '17 at 00:37
  • @Noah: For what it’s worth, I learned the same definition as bof: a formula with at least one free variable. – Brian M. Scott Jan 06 '17 at 00:48
  • 2
    @NoahSchweber According to Kleene's Introduction to Metamathematics, p. 151, an open formula is a formula with at least one free variable. I'm sorry to hear that some bad person has apparently written a textbook using "open" to mean "quantifier-free". – bof Jan 06 '17 at 00:53
  • @bof Well, the OP should indeed clarify what they mean, but I'll bet money that they mean "quantifier-free." And I think "some bad person" is misleading - the term "open formula" is used this way by a large portion of the logic community (as witnessed by the fact that "open induction" is the standard name for a particular theory of arithmetic). But whatever. – Noah Schweber Jan 06 '17 at 01:02

1 Answers1

1

Yes, this is true. The structure $(\mathbb{N}; 0, S, \le)$ admits quantifier elimination, and the proof of this is via induction on the complexity of $X$. For an example of such a proof, see this, which goes through the proof of quantifier elimination for a version of Presburger arithmetic.

Noah Schweber
  • 245,398