One can often read things like: let (S,R) be an ordered set, that is the set S ordered by the relation R; or, let (G,+) be a group, that is a set G together with an operation verifying such and such properties.
This formulation is convenient, but is it absolutely rigorous?
In this formulation, are the relation R or the operation + considered extensionally or intensionally?
Officially, a relation or an operation are sets by themselves, sets of ordered pairs ( and even, sets of ordered pairs having an ordered pair as first element in the case of binary operations).
So the definition of a group as (G, +) would mean a group is an ordered pair of two sets.
Another problem : (1) an ordered pair is not a set, since in a set there is no order. (2) if an ordered set is the ordered pair (S, R), then an ordered set is not a set.
Last question: is there any formal manipulation that can be done with a symbol such as (S,R) or (G,+) ? I mean, are there cases in which these symbols can be used in a formal reasoning?
One case I can imagine is one in which we'd want to show that two groups are identical. We could maybe prove that (G, +) = (G', +') by showing that the two ordered pairs have the same first element and the same second element.
Best Answer
Although we often consider ordered pairing as "primitive," so that an ordered pair of sets is of different type than a single set, this isn't how things are actually implemented at the level of ZFC. There, we implement ordered pairs of sets as sets themselves. There are many ways to do this, with in my experience the most common being $$\langle a,b\rangle=\{\{a\}, \{a,b\}\}.$$ It's easy to see under this definition that $\langle\cdot,\cdot\rangle$ satisfies the key principle of ordered pair notions, namely that $$\langle a,b\rangle=\langle c,d\rangle\iff a=b\wedge c=d.$$ So this gives us a way to implement all the ordered pair language without going beyond sets.
Meanwhile, I'm not sure what your last question means, but I suspect the picture above will help clarify things.
EDIT: Addressing your edited last question, I think the answer is no. Set theory gives us a way of implementing mathematical objects which is very useful at the theory level but very useless at the practical level. In particular, we almost never care whether two groups are identical, only isomorphic; and the situations where we do care take place when both groups are already explicitly embedded in a larger domain which again we only care about up to isomorphism. For example, for a group $A$ the question "Is the group of inner automorphisms of $A$ the same as the group of outer automorphisms of $A$?" is potentially interesting and is about group equality rather than isomorphism, but it's really a question about what's going on inside the full automorphism group; and we don't care how exactly that's implemented in set theory.
It is almost never useful to work with specific set-theoretic implementations of structures. That doesn't mean set-theoretic implementation is pointless, just that it's relevant in a different way: it's a useful tool in proving global results (e.g. "every group ...") by telling us that we can apply coarse theorems about sets to ("small") mathematical structures in general.