theory, so the same formal definitions "the x such that " can be contemplated in the two theories. A specific form of definition in the language of set theory is set-builder notation: means "the set A such that for all x, " (A cannot be free in ). This notation admits certain conventional extensions: is synonymous with ; is defined as , where is an expression already defined. Expressions definable in set-builder notation make sense in both ZFC and NFU: it may be that both theories prove that a given definition succeeds, or that neither do (the expression fails to refer to anything in any set theory with classical logic; in class theories like NBG this notation does refer to a class, but it is defined differently), or that one does and the other doesn't. Further, an object defined in the same way in ZFC and NFU may turn out to have different properties in the two theories (or there may be a difference in what can be proved where there is no provable difference between their properties). Further, set theory imports concepts from other branches of mathematics (in intention, all branches of mathematics). In some cases, there are different ways to import the concepts into ZFC and NFU. For example, the usual definition of the first infinite ordinal in ZFC is not suitable for NFU because the object (defined in purely set theoretical language as the set of all finite von Neumann ordinals) cannot be shown to exist in NFU. The usual definition of in NFU is (in purely set theoretical language) the set of all infinite well-orderings all of whose proper initial segments are finite, an object which can be shown not to exist in ZFC. In the case of such imported objects, there may be different definitions, one for use in ZFC and related theories, and one for use in NFU and related theories. For such "implementations" of imported mathematical concepts to make sense, it is necessary to be able to show that the two parallel interpretations have the expected properties: for example, the implementations of the natural numbers in ZFC and NFU are different, but both are implementations of the same mathematical structure, because both include definitions for all the primitives of Peano arithmetic and satisfy (the translations of) the Peano axioms. It is then possible to compare what happens in the two theories as when