[This question needs a major rewrite. Please regard it as 'paused' and inactive until I find the time to clarify the issues of concern. Thank you.]
Suppose we want to write very rigorous mathematics. Then, we need a foundation.
Now the naive approach is to just formalize everything within this foundation. Like, if our foundation is ZFC, then a group is an ordered pair (G,*), encoded as Kuratowski pair or otherwise, and formally speaking * is really a subset of G^3. By defining things in this very rigorous way, we might think that a high level of rigor is thereby achieved.
Actually, this is a really bad way of going about it! It means that if our foundations turns out to be inconsistent, then nothing we've proved in this way (say, about groups) can be trusted anymore. We have to start again from scratch. In reality, of course, we wouldn't need to start again from scratch, because most of the stuff we've proved doesn't need the full power of our foundations after all. For instance, if we're using ZFC as our foundations, well perhaps only 3 out of the 50 theorems we've proved need anything approaching the full power of ZFC, with the other results either following directly from the group axioms, or else being provable in much weaker systems.
Thus, in general, we want to prove things under minimal foundational assumptions, as opposed to committing to one particular foundations and carrying out all our activity therein.
This raises an interesting question. If foundational theories like ZFC are not the right place to formalize definitions like group, field, topological space, etc., then what is the proper role of foundations in rigorous mathematics?