I don't know of a way to completely formalize your question, but here is something with the same flavor that may hint at how to proceed. Blass and Gurevich defined a complexity class—or more accurately, a logic—that they called "Choiceless Polynomial Time with Counting" or $\tilde CPT+Card$. The exact definition is somewhat technical (their paper is easily findable with Google) but roughly speaking, the idea is that the properties of unlabeled graphs that are expressible in $\tilde CPT + Card$ are precisely those that are computable in polynomial time without choosing a labeling of the graph. I believe that it is still an open question whether every polynomial-time computable property of unlabeled graphs, including those that proceed by labeling the graph and then computing some property that ends up being independent of the labeling, is expressible in $\tilde CPT+Card$. I think most people expect the answer to be no, but it's not easy to come up with a candidate to separate the two classes. This question is closely related to the question of whether graph isomorphism is solvable in polynomial time.

Of course, what you're interested in doesn't involve any computational limitations. However, the above discussion suggests that if you wanted to formally prove that some particular property of an object requires an arbitrary choice, then you should:

1. define two classes of objects, one "labeled" and the other "unlabeled," where "unlabeled" basically means a class of labeled objects equivalent up to some notion of automorphism;

2. write down a logic that allows you to express properties of labeled objects, and another "choiceless logic" that allows you to express properties of the unlabeled objects "without choosing a labeling";

3. show that there is some property of labeled objects that is invariant under automorphism but that is inexpressible in your "choiceless logic."