Well-ordering in a first-order language

[jgens]

Is it possible to express well-ordering in a first-order language?

For example:
If $X$ is a set and $<$ is a binary relation on $X$ such that $(X,<) \vDash \forall x \; \neg(x<x)$ and $(X,<) \vDash \forall x \forall y \forall z((x<y \wedge y<z) \rightarrow x<z)$, then $(X,<)$ is a partial order.

If $(X,<)$ is a partial order such that $(X,<) \vDash \forall x \forall y(x<y \vee x=y \vee y<x)$, then $(X,<)$ is a total order.

I cannot think of a way to express well-ordering in this language. Since the quantifiers range over all of $X$ and there is no obvious way to quantify over subsets of $X$, I am thinking it is not possible to express well-ordering in this way. But it is also possible that I am just not sufficiently clever to think of something.

Any help?

 

[jgens]

I think I found an answer to this question. The standard model for $(\mathbb{N};0,S,<,+,\times)$ is well-ordered but non-standard models are not. In particular, this means that there is no first-order sentence that expresses well-ordering.

 

[Preno]

Well that much is true, but relying on non-standard models of arithmetic in order to show that the property of being a well-ordering is not expressible in first-order classical logic seems to be a bit of an overkill. A more straightforward argument relies on compactness: call the theory of strict partial ordering with your two axioms SPO and suppose that the set of formulas T expresses the property that < is a well-ordering (M is a model of SPO+T iff < is a well-ordering on the domain of M). Add countably many constants $c_0, c_1, \ldots$ to the language along with the axioms Ax: $c_1 < c_0, c_2 < c_1, \ldots$. Each finite subset of SPO+T+Ax is satisfiable, hence by compactness, the whole set is satisfiable in some model M. But the set of all realizations of $c_i$ clearly has no minimum in M, which contradicts the definition of T.