AI 中文总结
研究证明在弱算术理论$\rm PA_{smu}^-$中，即便附加标准模型的全称真语句，欧几里得除法原理pa16、pa17仍不可推导，通过构造模型完成该结论的证明。
AI 中文摘要
$\rm PA_{smu}^-$是一种弱算术理论，通过向离散有序环非负部分满足的基本公理添加两条关于2的幂的原理得到。我们引入理论$\rm PA_{wit}^-$，其中2的幂和所需见证由初始符号表示。我们证明，在算术标准模型的固定序列上，每个单变量项最终与二进有理数上的多项式一致。有限规避引理和紧致性定理随后产生一个$\rm PA_{smu}^-$的模型，其中除以3不成立。在该模型中，甚至标准欧几里得除法原理pa16的n=3实例也不成立。事实上，该模型可被选择为满足在标准模型中为真的每个全称$\rm \textit{L}_0$-语句。因此，即使将这些全称真语句附加到$\rm PA_{smu}^-$中，pa16和欧几里得除法原理pa17都不可推导。
英文摘要
$\mathrm{PA}_{\mathrm{smu}}^{-}$ is a weak theory of arithmetic obtained by adding two principles concerning powers of two to basic axioms satisfied by the nonnegative part of a discretely ordered ring. We introduce a theory $\mathrm{PA}_{\mathrm{wit}}^{-}$ in which powers of two and the required witnesses are represented by primitive symbols. We show that, along a fixed sequence in the standard model of arithmetic, every one-variable term eventually agrees with a polynomial over the dyadic rationals. A finite avoidance lemma and the Compactness Theorem then yield a model of $\mathrm{PA}_{\mathrm{smu}}^{-}$ in which division by $3$ fails. In this model even the $n=3$ instance of the Standard Euclidean Division Principle pa16 fails. In fact, the model can be chosen to satisfy every universal $\mathcal{L}_0$-sentence true in the standard model. Consequently, neither pa16 nor the Euclidean Division Principle pa17 is derivable even after these universal truths are adjoined to $\mathrm{PA}_{\mathrm{smu}}^{-}$.
Comments14 pages, no figures
