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
and
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 ``?" is a silly
question, for example) it is a bit too restrictive, in that it outlaws
(for example) the relation
(where 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 - 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: and a unary function .
`' is well-typed iff `' is of type CARDINAL and `' is
of type SET. ` is well typed iff `' 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
exists
for all and and all implementations of pairing functions.