Abstracting objects

Question

I understand that one way of defining a mathematical object such as a group is to take an object we already know to exist, for example the integers, and take away some properties from them. This is not the only way, and perhaps not the best way, but it is a way.

Are we allowed in ZFC to make definitions in such a way? We may simply define whatever we want so long as there exists some object for which this definition holds ?

Answer 1

We can define the (possibly proper) class of all objects that satisfy the properties of interest. For example, we can define the class $\rm SemiGrp$ of all pairs $\langle X,+\rangle$ such that $+:X\times X\to X$ and $x+(y+z)=(x+y)+z$ for all $x,y,z\in X$. All this does is give a name to the property, and most properties defined this way are proper classes. There does not even need to exist an object satisfying the property - for example the class of all inaccessible cardinals may be a proper class, or it may be empty - but one can define the class itself with no issues.

There are properties that we cannot even define in this sense, for example the set of all Godel numbers of true formulas, because it would lead to a contradiction to have a totally faithful interpretation of the truth predicate (see Undefinability of Truth); the issue arises in trying to model ZFC within itself, because this leads to a proper class which you can't then quantify over in the way one would like.

Answer 2

There is really nothing magical about $\sf ZFC$ that requires dark magic to conjure definitions.

The whole point of foundations using set theory is to give a basic way to translate "usual definitions" into set theoretical objects using some basic "meta-algorithm" for translation. It is true that this algorithm is somewhat limited, but still, if you have a property that you want to abstract then this property is something that can be expressed in something which itself can be (usually) expressed within the set theoretical universe.

So abstraction is not the issue here.

If something is given, for example, the set $\Bbb Z$ and the set $+$ which happens to be a binary operator on $\Bbb Z$ satisfying the properties:

1. There is some $x\in\Bbb Z$ such that for all $y$, $x+y=y$.
2. For every $x$ there is some $y$ such that for all $z$, $(x+y)+z=z$.
3. For every $x,y,z\in\Bbb Z$, $(x+y)+z=x+(y+z)$.
4. For every $x,y$ we have that $x+y=y+x$.

Now we want to say that an object with this property is called an abelian group. What is "this property"? It means that there is a set which is non-empty, $G$ and a binary operator on $G$ which will shall denote by $+_G$, and it satisfies these properties, all of which really talk about the existence of certain ordered pairs and triplets inside that binary operator. All this happens within naive set theory, let alone with $\sf ZFC$.