Why does the denotational semantics for a while loop have a existence quantifier?
The existential quantifier is misplaced. This is due to lack of reasonable notation for what needs to be expressed, namely: "if there is $i$ safisfying condition $C$, then use that $i$", where we make sure that at most one such $i$ exists. It would be better to write (and by the way, you might appreciate LaTeX's cases environment):
$$
\mathcal F^{k}(\bot)(\sigma) = 
\begin{cases}
    [\![s]\!]^i  &amp; \text{if $i &lt; k$ and $[\![b]\!] [\![s]\!]^i \sigma = \text{false}$ and, for all $j &lt; i$, $[\![b]\!] [\![s]\!]^j \sigma = true$}\\
     \bot &amp; \text{otherwise}
\end{cases}
$$
It may be helpful to look at a simpler definition. Suppose we want a function $f : \mathbb{N} \to \mathbb{N}$ which maps an odd number to zero and an even number to half of itself. The following is a reasonable definition:
\begin{align*}
f(2 n) &amp;= n\\
f(2 n + 1) &amp;= 0
\end{align*}
as is the following (where $m$ and $n$ range over natural numbers):
$$
f(m) =
\begin{cases}
n &amp; \text{if $m = 2 n$,}\\
0 &amp; \text{otherwise.}
\end{cases}$$
The point is that precisely one branch applies, and in a unique way, as there can be at most one $n$ satisfying the condition $m = 2 n$. However, the following is not a reasonable definition:
$$
f(m) =
\begin{cases}
n &amp; \text{if $\exists n \in \mathbb{N} \,.\, m = 2 n$,}\\
0 &amp; \text{otherwise.}
\end{cases}$$
The problem is that the $n$ outside the $\exists$ quantifier is completely unspecified. This is so because the $n$ inside the $\exists$ quantifier is bound and can therefore be renamed at will:
$$
f(m) =
\begin{cases}
n &amp; \text{if $\exists k \in \mathbb{N} \,.\, m = 2 k$,}\\
0 &amp; \text{otherwise.}
\end{cases}$$
(And we do not rename the outer $n$ because it is not in the scope of $\exists$.) This makes it clear that the existential quantifier has no place there. It is important to understand variable bindings. In the above definition of $f$, the variable $n$ is bound in the entire case, not just in the condition.

From a very formal point of view, the map $f$ is defined here as a relation explaining how an argument of $f$ is related to its value. 
A definition of the form
$$f(m) =
\begin{cases}
e_1(m,n) &amp; \text{if $\phi_1(m,n)$} \\
e_2(m,n) &amp; \text{if $\phi_2(m,n)$}
\end{cases}
$$
is equivalent to
$$f(m) = \text{the $v$ such that $\psi(m,v)$}
$$
where
$$\psi(m,v) \iff
(\exists n \,.\, \phi_1(m,n) \land v = e_1(m,n)) \lor
(\exists n \,.\, \phi_2(m,n) \land v = e_2(m,n))$$
Now the quantifiers are justified. By the way, we could have used $\forall$ instead:
$$\psi(m,v) \iff
(\forall n \,.\, \phi_1(m,n) \Rightarrow v = e_1(m,n)) \land
(\forall n \,.\, \phi_2(m,n) \Rightarrow v = e_2(m,n)).$$