Developing mathematics within ZFC

Question

Hello, I'm interested in just how "everyday mathematics" is expressed within the language of ZFC. For example, a function is a set all of whose members are ordered pairs and satisfies the formula "for all x,y,z, if (x,y) and (x,z) are in f, then y=z", and a mapping f:A->B can be defined as a triple (A,B,f) where f is a set thats a function and satisfies the formula "for all x, if there exist y such that (x,y) is in f, then x is in A" and the opposite for range of f is a subset of B. But I don't how to express more complicated things like groups, spaces, modules, categories etc. and morphisms between them.

I would like to know how to tell whether a set is one of these objects. Everyone can describe these things with natural human language, but not so many people know how to express them with just the membership relation! So can someone recommend me a source that expresses ordinary mathematical objects within the formal language of ZFC? Thanks for any help.

Answer 1

Once you have set-theoretic definitions of a few basic notions, like the ordered pairs, ordered triples, and functions that you mentioned in your question, plus natural numbers, you can define other concepts in terms of these using the standard definitions from their respective fields of mathematics. For example, a group can be defined as an ordered pair consisting of a set and a binary operation on it, subject to the usual axioms for groups. Similarly for the other notions you asked about. In other words, once the basic concepts are formalized in ZFC, you don't need (and shouldn't want) to go all the way back to the ZFC primitive notion $\in$ to define higher-level concepts. Of course, the higher-level concepts could be translated back into the primitive language, by replacing low-level concepts they depend on, like functions, by their set-theoretic definitions. The resulting translations would be huge, unreadable messes; that's why nobody uses them.

Many set theory books, for example those by Enderton and by Zuckerman, explain the set-theoretic representation of mathematical entities up to real numbers. But once you get to that level (or even earlier) it's time to stop trying to drag everything down to the primitive level of sets.

Answer 2

Responding to qwerty's answer-as-comment:

I'm going to assume that you are happy with me writing $X \times Y$, and writing ordered pairs $(x,y)$, without me having to expand these into raw set theoretic notation. Here is the statement "$m: G \times G \to G$ is an associative binary function" unpacked into ZFC:

$M$ is a subset of $G \times G \times G$ such that:

(1) For all $x$ and $y$ in $G$, there is a $z$ in $G$ such that $(x,y,z) \in M$.

(2) For all $x$, $y$, $z$ and $z'$ in $G$, if $(x,y,z) \in M$ and $(x,y,z') \in M$, then $z=z'$.

(3) For all $x$, $y$, $z$, $a$, $b$, $c$ and $d$ in $G$, if $(x,y,a) \in M$, $(a,z,b) \in M$, $(y,z,c) \in M$ and $(x,c,d) \in M$, then we have $b=d$.

Hopefully this makes it clear that there is nothing deep here, and that you never want to write out any large notion without some useful shorthands.

Answer 3

(Sorry I'm on a public computer it clears cache when I log off so I had to post my response as a new answer)

Hi Andreas Blass, thanks for your answer, but groups are exactly where my problems are! The usual elementry theory of groups has a binary function symbol (intended for +), an unary function (intended for -), and a constant 0. To say the associative law we need to REFER to an element, and only function symbols and constants allow us to refer to elements. So in order to say what a group is within ZFC, it seems to me that we must introduce a function symbol for every group. I don't think that's how it's done, and furthermore, a binary function symbol + in ZFC must be defined for all pairs of sets, whereas we only want + to be defined for pairs (x,y) with x and y both in some underlying set X.

I know how to code relational structures (i.e. structures with only relation symbols, such as partially ordered sets or ZFC itself) within ZFC, but I just don't understand what to do for structures with function symbols, where we refer to elements.

Answer 4

Really you should set up the category of sets using ZFC, and then work with that. Things like real numbers or natural numbers are characterised up to isomorphism by demanding they have certain properties (by being a complete ordered field, or by being a 'natural numbers object'), and then once you know you have one model, say by constructing the Dedekind reals (i.e. cuts), or the Cantor-von Neumann natural numbers, then you know that such things exist and you can forget the malarky about the global membership relation encoding everything.

And if you are particularly interested with groups, just consider a group object in the category of sets as you have just constructed - this is specified with a finite number of maps and commuting diagrams.

As far as sticking pedantically with the membership relation, it should be possible to define a set together with an element (identity) and relations that encode the maps and commuting diagrams, but this isn't ordinary mathematics. People doing PDEs don't worry about the construction of the real numbers they use, or even things like the construction of the (co)tangent bundle, or any other way of thinking about differential operators from a foundational viewpoint (and defining jets or synthetic differential geometry or D-modules is a long way from 'bare' foundations viz. ZFC)