Why does the denotational semantics for a while loop have a existence quantifier?

I was going through these notes and they have the following operator on partial functions:

$$
\mathcal F^{k}(\bot)(\sigma) =
\left\{
\begin{array}{ll}
\alpha( [\![s]\!]\sigma ) & [\![b]\!]\sigma=true \\
\sigma & [\![b]\!]\sigma=false \\
\bot & [\![b]\!]\sigma=\bot
\end{array}
\right.
$$

and supposedly it gives the following definition somehow (which ends up being the right denotation for while loops)

$$
\mathcal F^{k}(\bot)(\sigma) =
\left\{
\begin{array}{ll}
[\![s]\!]^i & \mbox{if $ \exists i \in [0,k)$ s.t. $ [\![b]\!] [\![s]\!]^i \sigma = false,\ [\![b]\!] [\![s]\!]^j \sigma = true,\ j \in [0,i) $}\\
\bot & \mbox{ o.w. }
\end{array}
\right.
$$

the proof by induction is shouldn't be hard. However, it feels that it doesn't really answer the question for me intuitively because I could do the induction mechanically without understanding what is going on. Why isn't the definition something like:

$$ f(\sigma,i) = [\![s]\!]^i\sigma$$

then the induction is easy:

$$ f(\sigma,0) = [\![s]\!]^0\sigma = \sigma$$

then the inductive step:

$$ f(\sigma,k+1) = f \circ f{\circ}^k(\sigma)= f \circ[\![s]\!]^{k}\sigma$$

but also notice $f = [\![s]\!]^1\sigma$ by strong induction:

$$ f(\sigma,k+1) = [\![s]\!]^{k+1}\sigma$$

as required. But that doesn't seem at all to be the sort of argument being used (assuming what I wrote is right). Did I miss something?

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 & \text{if $i < k$ and $[\![b]\!] [\![s]\!]^i \sigma = \text{false}$ and, for all $j < i$, $[\![b]\!] [\![s]\!]^j \sigma = true$}\\
\bot & \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) &= n\\
f(2 n + 1) &= 0
\end{align*}
as is the following (where $m$ and $n$ range over natural numbers):
$$
f(m) =
\begin{cases}
n & \text{if $m = 2 n$,}\\
0 & \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 & \text{if $\exists n \in \mathbb{N} \,.\, m = 2 n$,}\\
0 & \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 & \text{if $\exists k \in \mathbb{N} \,.\, m = 2 k$,}\\
0 & \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) & \text{if $\phi_1(m,n)$} \\
e_2(m,n) & \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)).$$

StackExchange Computer Science Q#98284, answer score: 4