Goldblatt's "Topoi" suggests the following exercise (16.3.2). Let $\varphi$ be some formula of some many-sorted language, and let $u$ be some term of the same sort as some free variable $v_i$ in $\varphi$. Show that the following is a pullback:
assuming all the usual things about variable capture/freeness, and where $\varphi(v_i/u)$ is the original formula with the $v_i$ variable substituted by the term $u$, $\mathbf{v} = (v_1 : a_1, ..., v_n : a_n)$ is a list of variables appropriate to the formula $\varphi$, $\mathbf{u}$ is one for $\varphi(v_i/u)$, $\mathcal{M}(\mathbf{v}) = \mathcal{M}(a_1) \times \dots \times \mathcal{M}(a_n)$, and $\mathcal{M}|v_i/u| : \mathcal{M}(\mathbf{v}) \rightarrow \mathcal{M}(\mathbf{u})$ projects $v_j$s out of $\mathbf{u}$ except for $v_i$, the latter being replaced by $\mathcal{M}^\mathbf{u}(u)$.
I've managed to do almost all of the cases for the structural induction on $\varphi$ except when it's quantified. So let's try show this for $(\forall w. \varphi)$. Here's the diagram I've been considering (where I denote $\varphi(v_i/u)$ as $\hat\varphi$):
The left face of this half-cube is our induction hypothesis, and I can see why the bottom one commutes. The orange dotted arrow on the right is what needs to be proven to:
- exist, and
- make it a pullback,
and I'm failing to see even just the existence. How do I construct this arrow, let alone prove it's the pullback we need?