论文标题
正弦的前伯伯算算术的可定性范围
Decidability bounds for Presburger arithmetic extended by sine
论文作者
论文摘要
我们考虑通过正弦函数扩展的Presburger算术，称此扩展名正弦 - 总计算术（$ \ sin $ -pa），并系统地研究了$ \ sin $ -pa中的一组句子的决策问题。特别是，我们详细介绍了在Schanuel猜想的假设下的存在$ \ sin $ -pa句子的决定算法。此过程将决策减少到Sine扩展的有序添加剂的理论，这是Schanuel的猜想可决定的。另一方面，我们证明了四个交替的量词块足以满足$ \ sin $ -pa句子的不可证明。为此，我们明确地解释了网格的弱小的二阶理论，该理论是不可决定的，用$ \ sin $ -pa。
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.
