# 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?

• The mechanical procedure you applied is correct. If the resulting sentence on the RHS doesn't hold, then neither does the LHS. – BrianO Jan 18 '16 at 21:39
• Thanks for your answer, but I still have trouble with the second equivalence. If the RHS would be true, than it also would be true for any m, n<k. But if the LHS would be true, it does not imply the RHS. – DerJFK Jan 18 '16 at 21:51
• But of course LHS => RHS, because in general $\exists\forall$ implies $\forall\exists$: the latter is weaker. – BrianO Jan 18 '16 at 21:59
• I got it now :) Thank you! I will post a answer later. – DerJFK Jan 18 '16 at 22:00
• Oh good :) You're welcome – BrianO Jan 18 '16 at 22:00

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.