Decidability bounds for Presburger arithmetic extended by sine

TL;DR

This paper explores the decidability of Presburger arithmetic extended with the sine function, providing decision procedures under Schanuel's conjecture and establishing undecidability with four quantifier alternations.

Contribution

It introduces a decision algorithm for existential sine-Presburger sentences under Schanuel's conjecture and proves undecidability with four quantifier blocks.

Findings

Decision algorithm for existential $ ext{sin}$-PA under Schanuel's conjecture

Undecidability of $ ext{sin}$-PA with four quantifier blocks

Explicit interpretation of the grid's weak monadic second-order theory in $ ext{sin}$-PA

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.