Is the two variable fragment of arithmetic, i.e., theory of ($\mathbb{N}, + ,\times$), decidable?

Any references would be appreciated. Most places only address different vocabularies (e.g. a survey of arithmetical definability by Bes).

• In "two-variable arithmetic" does every sentence have an equivalent prenex form consisting of an $x$-quantifier and a $y$-quantifier (in some order) followed by an open formula? Apr 3 '16 at 9:13
• No. In the first place, there are only finitely many formulae of the type you are talking about because the open formula can only say how x and y stand in relation to each other and the vocabulary is finite. Apr 3 '16 at 17:21
• Sorry, I should have asked "Is every sentence equivalent to a boolean combination of 2-quantifier formulas in prenex form?" Also, It would be helpful if you said what you mean by "the two variable fragment of arithmetic". Apr 3 '16 at 19:04
• @ThinniyamSrinivasanRamanatha That's true in a relational language, but not one with function symbols. There are infinitely many non-equivalent quantifier-free ("open") formulas, e.g. $x = y$, $x + x = y$, $x+x+x = y$, etc. Apr 3 '16 at 19:32
• If we just look at sentences with two quantifiers, without allowing variables to be rebound, then the answer is positive in practice, and conjectured to be always positive -- see the answer and comment of @FelipeVoloch at mathoverflow.net/a/21503/44143 Feb 8 '19 at 17:42