arXiv · 2204.00099
Decidability bounds for Presburger arithmetic extended by sine
Abstract
We consider Presburger arithmetic extended by the sine function, call this extension sine-Presburger arithmetic ($\sin$-PA), and systematically study decision problems for sets of sentences in $\sin$-PA. In particular, we detail a decision algorithm for existential $\sin$-PA sentences under assumption of Schanuel's conjecture. This procedure reduces decisions to the theory of the ordered additive group of real numbers extended by sine, which is decidable under Schanuel's conjecture. On the other hand, we prove that four alternating quantifier blocks suffice for undecidability of $\sin$-PA sentences. To do so, we explicitly interpret the weak monadic second-order theory of the grid, which is undecidable, in $\sin$-PA.
Explore related subjects
Keep this discovery
Eion Blanchard, Philipp Hieronymi. 2022-03-31. Decidability bounds for Presburger arithmetic extended by sine. https://arxiv.org/abs/2204.00099
Cite the original work for its findings. Save a collection to share your selection of sources.