Distinguishing characteristic and spurious properties When working in set theory with definitions of somehow primitive notions like ordered pairs (Kuratowski) or ordinal numbers (von Neumann) one is supposed to use only the characteristic properties of thus defined objects (i.e. sets). All other spurious properties are somehow "evil" and not to be used in proofs about those objects. 

But (how) can the distinction between characteristic and spurious
  properties be made formal and binding?

Is it just by "declaration", so the characteristic property is somehow part of the definition? (I think of automatic theorem provers: they must be told which properties they are allowed to use and which not.) What would be the appropriate language resp. framework for such a "declaration"?
 A: As far as I'm concerned, it is indeed "by declaration".
The choice is to some extent arbitrary, but I think of the characteristic properties $\Psi$ of a concept $\sf C$ as the (or perhaps, a) minimal set of conditions such that:

If $X$ enjoys all of $\Psi$, then $X$ may sensibly be called an instance of $\sf C$.


For example, as characteristic properties of an ordered pair $(\ast,\circ)$ we seek to extract, given $(\ast,\circ)$, that:


*

*The first element of the pair is $\ast$;

*The second element of the pair is $\circ$,


which in particular includes that $(\ast,\circ)=(\ast',\circ')$ implies $\ast = \ast'$ and $\circ=\circ'$.
For ordinals (it is probably best to talk about the class of ordinals), it is less obvious what exactly the characteristic properties include. It is clear that we should obtain "every well-ordered set is isomorphic to a unique ordinal"; the familiar (and heavily used) identity $\alpha = \{\beta: \beta < \alpha\}$ or perhaps $\alpha = \{\beta: \beta \text{ has an order-embedding into } \alpha\}$ is up for debate, although it is so convenient that I'd personally like to be allowed to use it.

It is worth pointing out that in category theory, this type of identifying "characteristic properties" (better known as "universal properties" in that field) is done all the time. Effectively, one takes a general viewpoint where the spurious properties are simply unavailable: once a certain thing (say, a Cartesian product) is constructed, we ditch the specific construction and simply work with the universal property (until the need to demonstrate another universal property arises).
