In A New Approach to Abstract Syntax with Variable Binding, Pitts and Gabbay describe a "freshness" quantifier for their variant of set theory, where you can quantify over fresh names. This allows you to describe freshness conditions in a more formal way than the usual "x does not occur in M," and even reason about fresh names with formal logic. The quantification N x can be read: "for fresh x ..." This has a cool, dual universal/existential property: because the ambient universe of names is infinite, it's always true that there exists a fresh x, and because we don't care which one we choose, any proposition we prove using the freshness quantifier holds for all such fresh names.
What confused me for a while was that the quantifier just says "x is fresh;" it doesn't say "x is fresh with respect to M". But it seemed like if you take a name that's fresh at one point, but then use it in another context, you might have accidentally picked a name that conflicted with a name in the new context. In other words, I was concerned that having a local freshness condition without talking globally about all the names you're ever going to use doesn't carry enough information to avoid an incorrect choice of fresh name.
You have to dig a little deeper to see why this isn't a problem. The real meaning of the quantifier comes from the idea that the universe of names is infinite, but the construction of any particular term only involves a finite number of names. So not only can you find a fresh name at any point; but you can in fact choose any name other than the ones used in that term. So all but finitely many names are fresh. This is the more precise interpretation of N x: "for all but finitely many names x ..."
So the freshness quantifier isn't actually committing to a name. It's just saying that there's a huge set of names for which the proposition holds. Thus moving in and out of scope of particular terms doesn't affect the truth of a proposition built with the quantifier, because while the particular set of fresh names might change, the fact that that set involves all but a finite number of names does not. This allows us to abstract away from the actual choice of fresh names in a program when we're writing propositions about them.