In Hodges' "Shorter Model Theory", there are two instances where one shows that a certain formula $\phi$ is equivalent modulo a theory $\mathcal{T}$ to some infinitary formula $\chi$. Typically, this $\chi$ is of the form "infinitary disjunction of infinitary conjunctions". It is then claimed that "two applications of compactness" reduce $\chi$ to a first-order quantifier-free formula.
This happens in the proof of Theorem 7.1.3, and also as part of exercise 7.2.13.
It seems intuitively clear that if your infinitary formula is equivalent to a first-order one, then it should be possible to find a finite part of the disjunction, and then a finite part of the corresponding conjunction which turn out to be equivalent to the infinitary formula, but I'm struggling to give a formal compactness argument to show this, which seems to be what Hodges is hinting at. Here are my current thoughts:
Let's say $\chi(\bar{x}) = \bigvee_I\bigwedge_J \psi^i_j(\bar{x})$, where $I$ and $J$ are infinite, and $\mathcal{T} \vdash \forall \bar{x} (\phi(\bar{x}) \iff \chi(\bar{x}))$.
Given the equivalence between $\phi$ and $\chi$, there must be a proof of $\phi(t)$ out of $\chi(t)=\bigvee_I\bigwedge_J \psi^i_j(t)$ and $\mathcal{T}$, for every closed term $t$. But proofs are finite, so when I write down such a proof, it must only ever involve finite subsets of $I$ and $J$. So I should in fact have that $\mathcal{T} \cup \{\chi'(t)\} \vdash \phi(t)$, for $\chi'(t)$ the formula obtained out of $\phi$ from those finite subsets of $I$ and $J$.
Conversely, I should be able to prove $\chi'(t)$ out of $T \cup \{\phi(t)\}$. As it is clear that $\chi(t)$ implies $\chi'(t)$, and we have the equivalence between $\phi$ and $\chi$, that should be ok.
This argument doesn't sit fully well with me. It is not completely clear to me what it means to have an infinitary sentence as a hypothesis. What exactly does it mean to say that $\bigvee_J \phi_j \vdash \phi$, when $J$ is infinite, for example? I suppose for $\bigwedge_J \phi_j \vdash \phi$,we're meant to see this as the theory with axioms $\phi_j$ proving $\phi$, in which case the compactness reduction is clear.
Would anyone kindly explain this and give a formal Compactness argument to reduce $\chi$ to a first-order formula?
Don't think about proofs, think about entailment. I'm not sure why Hodges writes $\vdash$ here instead of $\models$, but there's a clear meaning of $T\models \varphi$ for infinitary sentences $\varphi$, namely that every model of $T$ satisfies $\varphi$.
Now let's prove that if $T$ is a first-order theory, $\varphi(x)$ and $\{\psi_{i,j}(x)\mid i\in I, j\in J_i\}$ are first-order formulas, and $T\models \forall x\, (\varphi(x)\leftrightarrow \bigvee_{i\in I} \bigwedge_{j\in J_i} \psi_{i,j}(x))$, then there are finite subsets $I'\subseteq I$ and $J'_i\subseteq J_i$ for all $i\in I'$ such that $T\models \forall x\, (\varphi(x)\leftrightarrow \bigvee_{i\in I'} \bigwedge_{j\in J_i'} \psi_{i,j}(x))$. Note that $x$ may be a tuple of variables here - I just want to simplify notation by not writing $\overline{x}$.
First, fix $i\in I$. Note that $T\models \forall x\, (\bigwedge_{j\in J_i} \psi_{i,j}(x)\to \varphi(x))$, so $T\cup \{\psi_{i,j}(x)\mid j\in J_i\}\cup \{\lnot \varphi(x)\}$ is inconsistent. By compactness, there is a finite subset $J'_i\subseteq J_i$ such that $T\cup \{\psi_{i,j}(x)\mid j\in J'_i\}\cup \{\lnot \varphi(x)\}$ is inconsistent. Let $\chi_i(x) = \bigwedge_{j\in J'_i} \psi_{i,j}(x)$. Note that (a) $\chi_i(x)$ is first-order, (b) $T\models \forall x\, (\bigwedge_{j\in J_i} \psi_{i,j}(x)\to \chi_i(x))$, and (c) $T\models \forall x\, (\chi_i(x)\to \varphi(x))\}$.
Having defined $\chi_i(x)$ for all $i$, we note that $T\models \forall x\,(\bigvee_{i\in I} \bigwedge_{j\in J_i} \psi_{i,j}(x)\to \bigvee_{i\in I} \chi_i(x))$ and $T\models \forall x\,(\bigvee_{i\in I} \chi_i(x)\to \varphi(x))$, and hence $T\models \forall x\, (\bigvee_{i\in I} \chi_i(x)\leftrightarrow \varphi(x))$. In particular, $T\cup \{\lnot \chi_i(x)\mid i\in I\}\cup \{\varphi(x)\}$ is inconsistent. By compactness, there is a finite subset $I'\subseteq I$ such that $T\cup \{\lnot \chi_i(x)\mid i\in I'\}\cup \{\varphi(x)\}$. Thus $T\models \forall x\, (\varphi(x)\to \bigvee_{i\in I'}\chi_i(x))$. Since also $T\models \forall x\, (\bigvee_{i\in I'}\chi_i(x)\to \bigvee_{i\in I} \chi_i(x))$ and $T\models \forall x\, (\bigvee_{i\in I} \chi_i(x)\to \varphi(x))$, it follows that $T\models \forall x\, (\varphi(x)\leftrightarrow \bigvee_{i\in I'}\bigwedge_{j\in J'_i} \psi_{i,j}(x))$.