Why isn't there a first-order theory of well order?
Problem 1.4.1 of Model Theory by Chang and Keisler asks,
Is there a theory of well order in the first-order language $\{\leq\}$?
I'm pretty sure the answer is no, since well order is a property of "subsets" or "predicates", and first-order sentences only allow quantifiers over "individuals". However, I don't know how to prove this.
In particular, for every $n$, the first-order sentence $$\forall x_1 \ldots x_n\left(x_1 \neq x_2 \wedge \cdots \wedge x_{n - 1} \neq x_n \rightarrow \exists y\left((y = x_1 \vee \cdots \vee y = x_n) \wedge (y \leq x_1 \wedge \cdots y \leq x_n)\right)\right)$$ says that every subset of size $n$ has a least element, and I don't know how to rule out the possibility that it's possible to write down analogous sentences for infinite subsets (and that I just haven't found the right approach yet).
How can I prove that there is no first-order theory of well order?
If there were such a theory, throw in countably many new constant symbols $c_1, c_2,\dots$ and throw in the axioms $c_2 < c_1, c_3 < c_2, \text{etc.}$ Now this new theory is consistent, since any finite subset of the axioms has a model (e.g. natural numbers under usual $<$ with the finitely many constants assigned appropriately), but that is a contradiction, since a model of the (whole) new theory is a well ordering with an infinite descending sequence.