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.