关于以可计算数的整数幂扩充的实数存在理论

本文研究了 $\exists\mathbb{R}(r^{\mathbb{Z}})$，即通过为固定可计算实数 $r > 0$ 的整数幂添加一元谓词 $r^{\mathbb{Z}}$ 来扩充实数存在理论。如果仅能访问计算 $r$ 的图灵机，则无法判定该理论的输入公式是否可满足。然而，我们展示了一种算法，可在以下情况判定此问题：1. 已知 $r$ 是超越数，或 2. $r$ 是某个给定整系数多项式的根（即 $r$ 是代数数）。换言之，了解 $r$ 的代数性足以规避不可判定性。此外，在 $r$ 具备我们称之为多项式根障碍的前提下，我们确立了复杂度结果。利用这一概念，我们证明了 $\exists\mathbb{R}(r^{\mathbb{Z}})$ 的可满足性问题：1. 若 $r$ 是自然数，则属于 NEXPTIME；2. 若 $r$ 是代数数，则属于 EXPSPACE；3. 若 $r$ 属于包含 $\pi$ 和 Euler's $e$ 的超越数族，则属于 3EXP。作为结果的副产品，我们能够从具有有理概率、奖励和阈值的随机博弈的熵风险阈值问题的可判定性证明 [Baier et al., MFCS'23] 中移除对 Schanuel 猜想的依赖：当熵风险的底为 Euler's $e$ 且厌恶因子为固定的代数数时，该问题属于 EXP。