What is the significance of nominal techniques, as far as their application to the formal theory of bound variables is concerned?
I have been reading M. J. Gabbay's expository work on the topic that appeared in Bulletin of Symbolic Logic. I understand that, the main contribution of nominal techniques to the nasty problem of $\alpha$-conversion is that they introduced new principles of induction and recursion, and a new quantifier. However, I am not sure if the use of orbits instead of $\alpha$-equivalence classes is strictly necessary for these purposes - because orbits and equivalence classes are essentially the same thing.
I understand the theory of nominal sets are very fruitful in that it can be applied in many different areas - including infinite automata theory and domain theory, due mainly to its general nature. I would like to know the relevance of the theory's generality - replacing $\alpha$-equivalence classes with orbits - in the very first problem that it is meant to solve, that is, $\alpha$-equivalence of syntactic objects.
EDIT: I knew how nominal techniques could be applied to reasoning up to $\alpha$-equivalence; my question was more about the theory's internal methodology, that is, the focus on the group action.
Here's an attempt to answer my question: automorphisms on the set-theoretic universe induced by permutations of atoms are crucial in proving the new recursion/induction principles, so is the reinterpretation of $\alpha$-equivalence as orbits. However, this reinterpretation might or might not be relevant to the users of the recursion/induction principles.
Let me know if there is something in my answer to be added or corrected.
EDIT 2: My question might have been better phrased as: do we really need to appeal to axiomatic set theory - something very powerful - to get a proper treatment of alpha-equivalence?