Shifting bounded quantifiers The universe of the following variables are the natural numbers $\mathbb{N}$.
I found in the literature the following logic equivalence:
$\forall n <  k \exists m \ \varphi(m,n) \leftrightarrow \exists m \forall n < k \ \varphi(\langle m \rangle_n,n ) $
where $\varphi$ is an arbitrary formular and let $p$ code a $k$ tuple of natural numbers than $\langle p \rangle_i$ returns the $i$-th entry.
I am interested how to shift the bounded qunatifier in the following case
$\exists n <k \forall m \ \varphi(m,n) \leftrightarrow$ ?
In literature we should obtain this by negate both sides of the first equivalence:
$\exists n < k \forall m \ \neg \varphi(m,n) \leftrightarrow \forall m \exists n <k \ \neg \varphi (\langle m \rangle_n,n) $
But these both expressions seems not equivalent, since $m$ could code a constant sequence so that for no $n<k$ the formular holds.
What am I doing wrong? And how to shift the bounded quantifier in the second case?
Thank your for any help.
 A: To answer the specific question: if
$$
(\exists n < k)(\forall m) \phi(n,m)
$$
does not hold, then we can choose for each $n < k$ some $\sigma(n)$
such that
$$
(\forall n < k)\lnot \phi(n, \sigma(n)).
$$
But then, because some $m$ codes this $\sigma$, we have
$$
(\exists m)(\forall n < k) \lnot \phi(n, (m)_n)
$$
and thus
$$
\lnot (\forall m)(\exists n < k) \phi(n, (m)_n).
$$
In the remainder of this post, I'll go through both equivalences. The formatting doesn't look great on this site, but it is easier to put the formulas in display math at the expense of attractiveness, I think.
Moving an existential quantifier across a bounded universal quantifier
We show that
$$
(\forall n < k)(\exists m) \phi(n,m) \Leftrightarrow
(\exists m)(\forall n < k) \phi(n, (m)_n).
$$
For the first half, suppose
$$
(\forall n < k)(\exists m) \phi(n,m)
$$
Then there is a sequence $\sigma$ of length $k$ such that
$$
(\forall n < k) \phi(n, \sigma(n))
$$
holds, and thus, because we can code $\sigma$ into a natural number,
$$
(\exists m)(\forall n < k)\phi(n, (m)_n)
$$
holds.
Conversely, if 
$$
(\exists m)(\forall n < k)\phi(n, (m)_n)
$$
holds then it is immediate that
$$
(\forall n < k)(\exists m) \phi(n,m)
$$
holds.
Moving a universal quantifier across a bounded existential quantifier
We will show that 
$$
(\exists n < k)(\forall m) \phi(n,m) \Leftrightarrow 
(\forall m)(\exists n < k) \phi(n, (m)_n).
$$
For the first half, suppose that 
$$
(\exists n < k)(\forall m) \phi(n,m)
$$
holds. Then, in particular,
$$
(\forall n < k)(\exists m) \phi(n,m)
$$
does not hold. Thus there is no sequence $\sigma$ of length $k$ such that 
$$
(\forall n < k) \phi(n, \sigma(n))
$$
which means that
$$
(\forall \sigma)(\exists n < k) \phi(n, \sigma(n))
$$
does hold. So in particular, if we define a coding $(\cdot)$ such that $(m)_n$ is defined for all $m$ and $n$, then we have
$$
(\forall m)(\exists n < k) \phi(n, (m)_n).
$$
This gives us half of the equivalence.
For the other half, working by contraposition, assume that
$$
(\exists n < k)(\forall m) \phi(n,m)
$$
does not hold. Then we have
$$
(\forall n < k)(\exists m) \lnot \phi(n,m).
$$
Then, as above, there is a sequence $\sigma$ of length $k$ such that
$$
(\forall n < k)\lnot \phi(n, \sigma(n))
$$
Thus we have
$$
\lnot (\exists n < k) \phi(n, \sigma(n)).
$$
Letting $m_0$ code $\sigma_0$, we have
$$
\lnot (\exists n < k) \phi(n, (m_0)_n).
$$
In particular, this means we have
$$
\lnot (\forall m)(\exists n < k) \phi(n, (m)_n),
$$
which completes the proof by contraposition. 
