only set theoretical language is in use, as long as the definitions appropriate to ZFC are understood to be used in the ZFC context and the definitions appropriate to NFU are understood to be used in the NFU context. Whatever is proven to exist in a theory clearly provably exists in any extension of that theory; moreover, analysis of the proof that an object exists in a given theory may show that it exists in weaker versions of that theory (one may consider Zermelo set theory instead of ZFC for much of what is done in this article, for example). Empty set, singleton, unordered pairs and tuples These constructions appear first because they are the simplest constructions in set theory, not because they are the first constructions that come to mind in mathematics (though the notion of finite set is certainly fundamental). Even though NFU also allows the construction of set ur-elements yet to become members of a set, the empty set is the unique set with no members: For each object , there is a set with as its only element: For objects and , there is a set containing and as its only elements: The union of two sets is defined in the usual way: This is a recursive definition of unordered -tuples for any concrete (finite sets given as lists of their elements:) In NFU, all the set definitions given work by stratified comprehension; in ZFC, the existence of the unordered pair is given by the Axiom of Pairing, the existence of the empty set follows by Separation from the existence of any set, and the binary union of two sets exists by the axioms of Pairing and Union (). Ordered pair First, consider the ordered pair. The reason that this comes first is technical: ordered pairs are needed to implement relations and functions, which are needed to implement other concepts which may seem to be prior. The first definition of the ordered pair was the definition proposed by Norbert Wiener in 1914 in the context of the type theory of Principia Mathematica. Wiener observed that this allowed the elimination of types of n-ary relations for n > 1 from the system of that work. It is more usual now to use the definition , due to Kuratowski. Either of these definitions works in either ZFC or NFU. In NFU, these two definitions have a technical disadvantage: