Let $\mathscr C$ be a cartesian (i.e. with finite limits) category with subobject classifier $\Omega$ and generic subobject $\tau:I\to\Omega$ (here $I$ denote the terminal object).
Let $f:X\to Y$ and $p:X\to\Omega$ be a morphisms. The quantificators $\exists_f(p):Y\to\Omega$ and $\forall_f(p):Y\to\Omega$ are characterized by the following:
for each $q:Y\to\Omega$, $\exists_f(p)\implies q$ if and only if $p\implies q\circ f$;
for each $q:Y\to\Omega$, $q\implies\forall_f(p)$ if and only if $q\circ f\implies p$.
Let assume that for each object $X$ and each pair of morphisms $f:X\to Y$, $p:X\to\Omega$ there exists $\forall_f(p):Y\to\Omega$. It's also true that there exists $\exists_f(p):Y\to\Omega$ too?
Following this piece taken from Lambek & Scott - Introduction to Higher Order Categorical Logic (page 129):
I deduced this formula relating $\forall$ with $\exists$:
$\exists_f(p)=\forall_{\pi_1}(\forall_{f\times 1_\Omega}(p\circ\pi_1\implies\pi_2)\implies\pi_2)$
where $p\circ\pi_1\implies\pi_2$ is a morphism $X\times\Omega\to\Omega$, while $\forall_{f\times 1_\Omega}(p\circ\pi_1\implies\pi_2)\implies\pi_2:Y\times\Omega\to\Omega$.
I proved that this formula holds whenever the universal quantificator "commutes" with pullback (see here). This is true, in particular, if for each object $X$ there exists $\Omega^X$.
Is the converse true? That's if the formula relating $\forall$ and $\exists$ is true, then $\forall$ commute with pullback? Power objects $\Omega^X$ needs to exists?