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 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 in which division by fails. In this model even the instance of the Standard Euclidean Division Principle pa16 fails. In fact, the model can be chosen to satisfy every universal -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 .

生成讲解博客的中文版本

生成AI智能校验的中文版本