5
$\begingroup$

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.

$\endgroup$
  • 1
    $\begingroup$ 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. $\endgroup$ – Chris Eagle Apr 29 '12 at 10:13
7
$\begingroup$

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\Big(X0\,\land\forall x(Xx\to Xx+1)\land\forall Y\big(Y0\,\land\forall y(Yy\to Yy+1)\big)\to\forall x(Xx\to Yy)\Big)$$

(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$.

$\endgroup$
  • $\begingroup$ Right, of course. Thank you. :^) $\endgroup$ – Rachel Apr 29 '12 at 21:18

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.