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.