# Formal second-order statements of Archimedean and completeness properties

I am trying to translate the following statements from English to second-order logic, and I want to know if I got them right. I have a language for an ordered field $(F,+,\cdot,0,1,\leq)$, i.e., I don't have a predicate symbol for some equivalent of the natural numbers. Lowercase letters denote first-order variables; uppercase denote second-order.

Archimedean property:

For every element $x$ of the field, there exists some natural number $y$ such that $y > x$.

$$\exists X \; \forall x \; \exists y \; \forall z \; [X0 \land (Xz \rightarrow Xz+1) \land Xy \land x \leq y \land x \neq y]$$

Dedekind completeness:

Every nonempty subset of the field that is bounded above has a least upper bound in the field.

$$\forall X \; \exists Y \; \exists z \; \forall x,y \; [(Xx \land Yy) \rightarrow (x \leq y \land Yz \land z \leq y)]$$

This is not homework, by the bye, but a hint will do if something is wrong. Thanks.

-
Your attempt at the Archimedean property will be true in any ordered field, since we can just take the extension of $X$ to be everything. – Chris Eagle Apr 29 '12 at 10:13

The problem with your attempt at the Archimedean property is that it guarantees only that $X$ contains the $F$-analogue of $\Bbb N$, not that $X$ is that set. $X$ could be any inductive subset of $F$ containing $0$, including, as Chris Eagle points out, $F$ itself. You want to add something to ensure that $X$ is the smallest inductive set containing $0$. An easy way to do this is to mimic the induction axiom of Peano’s axioms:
$$\exists X\Bigg(X0\,\land\forall x(Xx\to Xx+1)\land\forall Y\Big(Y0\,\land\forall y\big(Yy\to Yy+1)\big)\to\forall x(Xx\to Yy)\Big)\Bigg)$$
(For greater clarity I’ve left the quantifiers in their natural locations instead of pulling them out to the front.) Intuitively this says that $X$ contains $0$ and is inductive, and if $Y$ is any inductive subset of $F$ that contains $0$, then $X\subseteq Y$. In other words, $X$ is the smallest inductive subset of $F$ containing $0$.