Let $H$ be a complex Hilbert space and $H_1,...,H_n$ be closed subspaces of $H$. Set $H_0:=H_1\cap H_2\cap...\cap H_n$ and let $P_i$ be the orthogonal projection onto $H_i$, $i=0,1,2,...,n$. I study the functions $f_n:[0,1]\to\mathbb{R}$ defined by $$ f_n(c)=\sup\{\|P_n...P_2 P_1-P_0\|\,|\, c_F(H_1,...,H_n)\leqslant c\},\,c\in[0,1], $$ where the supremum is taken over all complex Hilbert spaces $H$ and systems of closed subspaces $H_1,...,H_n$ of $H$ for which the Friedrichs number $c_F(H_1,...,H_n)$ is less than or equal to $c$ (the Friedrichs number is a certain numerical characteristics of a system of subspaces). Note that all such systems of subspaces do not form a set. Despite of this, the function $f_n$ is well-defined (see my Question Can we take a supremum over all Hilbert spaces?). Indeed, let $A_{n}(c)$ be the set of all $a\in\mathbb{R}$ for which there exist a complex Hilbert space $H$ and a system of closed subspaces $H_1,...,H_n$ of $H$ such that $c_F(H_1,...,H_n)\leqslant c$ and $\|P_n...P_2 P_1-P_0\|=a$. Then by the axiom (scheme) of separation $A_{n}(c)$ is a set and thus we can take its supremum.

I need to show that $f_n(c)\leqslant g_n(c)$ for some function $g_n$. I argue as follows. Consider arbitrary element $a\in A_{n}(c)$. Then there exist a complex Hilbert space $H$ and a system of closed subspaces $H_1,...,H_n$ of $H$ such that $c_F(H_1,...,H_n)\leqslant c$ and $\|P_n...P_2 P_1-P_0\|=a$. After this I work with this system of subspaces $(H;H_1,...,H_n)$ and show that $\|P_n...P_2 P_1-P_0\|\leqslant g_n(c)$. Thus $a\leqslant g_n(c)$. Since this inequality holds for every $a\in A_{n}(c)$, we conclude that $\sup A_{n}(c)\leqslant g_n(c)$, i.e., $f_n(c)\leqslant g_n(c)$.

Questions. Are all these arguments correct, say, in the axiomatic theory ZFC? I am suspicious here because we need to choose an element (system of subspaces) from a class (and work with this element). Do we need here something like the Axiom of Choice?

In response to Nate Eldredge's comment: essentially, the core of my worries is the following. Unfortunately, and this is the worst, is that I do not understand if the function $A_n(c)\ni a\mapsto (H;H_1,...,H_n)$ such that $c_F(H_1,...,H_n)\leqslant c$ and $\|P_n...P_2 P_1-P_0\|=a$, is needed in the arguments above or not.

Please help me.

  • 2
    $\begingroup$ I think generically, the question is as follows? You have a first-order formula $\varphi(x,y)$, with $x,y$ free, and a set $A$ (maybe $A \subset \mathbb{R}$ here), and you can prove $\forall x \in A \: \exists y \: \varphi(x,y)$. You would like to conclude there exists a function $f : A \to B$, where $B$ is some set, such that $\varphi(a, f(a))$ for all $a \in A$. $\endgroup$ Mar 24, 2021 at 22:21
  • $\begingroup$ @NateEldredge Unfortunately, and this is the worst, is that I do not really understand if the function is needed here or not. $\endgroup$ Mar 25, 2021 at 0:06

1 Answer 1


It is often tempting to think that all our existential instantiations happen "in advance", a sort of proof theoretic "mise en place" if you will.

But they don't, and they don't have to be. For a given $a$, we pick some $H$ and $H_i$'s, and so on. At each step, we only need to instantiate finitely many quantifiers.

Now, you may still wonder, how do we choose an element from a proper class? Well, the axiom of choice has absolutely nothing to do with that. As we know, a class is really a formula, i.e. $C$ is a class when there's some $\varphi(x)$ which defines it (we allow parameters, but I'm omitting them as they are fixed through this discussion anyway). To say that $C$ is not empty is exactly to say that $\exists x\,\varphi(x)$ holds. Now apply existential instantiation and we're done.

Even if you want to choose infinitely many elements from a class, which the above reasoning doesn't allow you, we can easily prove in $\sf ZF$ that no class is finite, and so that every class must contain an infinite set: simply look at $C\cap V_\alpha$, where $V_\alpha$ is the $\alpha$th step of the von Neumann hierarchy. Since we must add new elements unboundedly often, there is some $\alpha$ such that $C\cap V_\alpha$ is infinite. If we also assume choice, then we can even argue that we surpass every possible cardinality.

  • $\begingroup$ "But it's not, and it doesn't have to be" → "But they don't, and they don't have to be"? (I love that mise en place metaphor.) $\endgroup$
    – LSpice
    Mar 24, 2021 at 21:10
  • 1
    $\begingroup$ I presume you mean "no proper class is finite". (-: $\endgroup$ Mar 24, 2021 at 23:50
  • 2
    $\begingroup$ @LSpice: It puts the saying "we're cooking up a proof" in a whole light. $\endgroup$
    – Asaf Karagila
    Mar 25, 2021 at 1:27
  • 2
    $\begingroup$ @Ivan: As I said, that would be misleading to the reader, apparently also for you. Just because you wrote $f(a)$ does not mean that it is actually define a function. It is a notation, it tells you that $f$ depends on $a$ and that it is fixed within a given context. That is all. $\endgroup$
    – Asaf Karagila
    Mar 25, 2021 at 22:07
  • 4
    $\begingroup$ @Ivan: You need to use AC when you need to choose things uniformly. When you just want to claim that something is independent of the choice, you can just pick representatives when necessary. Don't feel bad, it's confusing for a lot of mathematicians. You need time and practice to get used to it. $\endgroup$
    – Asaf Karagila
    Mar 25, 2021 at 23:26

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.