In `Reasoning about theoretical entities' I treat in detail two special cases of theoretical entities arising from equivalence relations, namely cardinal and ordinal arithmetic. There is an intelligible and plausible ontological stance to take in relation to cardinals to the effect that there are facts about cardinals, but no cardinals: facts about cardinals are just facts about sets and mappings between sets. The fact that cardinal multiplication is commutative is nothing more than the fact that $A \times B$ and $B \times A$ are the same size. On this analysis the only assertions that we can meaningfully make about cardinals arise from predicates of sets for which equipollence is a congruence relation. Although this is an attractive analysis (it explains why ``$3 \in 5$?" is a silly question, for example) it is a bit too restrictive, in that it outlaws (for example) the relation $\vert x\vert > min(x)$ (where $x$ is a finite set of naturals. This is relative largeness which we definitely want to keep. It turns out that a more fruitful analysis identifies as cardinal arithmetic those assertions about (naive) cardinals whose truth value does not depend on a choice of implementation of cardinals as sets. This lets in relative largeness but excludes $3 \in 5$ - as desired. To complete the picture there is a completeness/preservation theorem for a typing system. The typing system says there are two types: cardinals and sets, a binary relation: $\in$ and a unary function $\vert \vert$. `$x = \vert y\vert$' is well-typed iff `$x$' is of type CARDINAL and `$y$' is of type SET. `$x \in y$ is well typed iff `$y$' is of type SET. So we can prove that something is well-typed iff its truth-value is not affected by choice of implementation.

This completeness theorem is clearly a sensible result, and one we should be happy with. However the act of turning over this stone has revealed an interesting fact which--although perhaps not terribly surprising--is certainly significant and worth noting. This completeness theorem turns out to be equivalent to the axiom scheme of replacement. It is surely remarkable that a philosophically motivated way of merely thinking about cardinals (never mind proving theorems about them!) commits us to a set-existence axiom: the conclusion is that the decision to think of cardinal numbers in this rather natural way commits us to replacement. I think this is the strongest argument yet for replacement, and it appears to be new--although Adrian Mathias tells me that he once showed that replacement is equivalent to the assertion that $x \times y$ exists for all $x$ and $y$ and all implementations of pairing functions.