Decidability bounds for Presburger arithmetic extended by sine
Speaker:
Eion Blanchard, University of Illinois at Urbana-Champaign
Date and Time:
Friday, March 11, 2022 - 12:00pm to 1:00pm
Location:
Fields Institute, Room 230
Abstract:
We consider Presburger arithmetic (PA) 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 for $\mathbb{C}$. This procedure reduces decisions to the theory of the ordered additive group of real numbers extended by sine, whose decidability under Schanuel's conjecture for $\mathbb{C}$ follows from work of Macintyre and Wilkie. On the other hand, we also prove four alternating quantifier blocks suffice for undecidability of $\sin$-PA sentences. This work is joint with Philipp Hieronymi.