BPI and arbitrary-language first-order compactness

Under BPI, let $T$ be finitely satisfiable. If $T⊢\mathrm{\perp }$, F7 gives a finite $T_0\subseteq T$ proving $\mathrm{\perp }$. Its assumed nonempty model contradicts F3. Thus $T$ is consistent, and F1 supplies $T_H$ and $L_{\mathrm{\infty }}$ as stated there. Let $S$ be the set of all $L_{\mathrm{\infty }}$-sentences. It is a set because sentences are finite strings on a set of symbols.

Separately, assume first-order semantic compactness. For propositional letters in a set $P$, take a language with one constant $c$ and unary predicates $R_p$ for $p\in P$. Translate $p$ to $R_p(c)$, commute with Boolean connectives, and translate true and false to $c=c$ and $\mathrm{\neg }(c=c)$. A propositional valuation gives a structure on $\{0\}$ by $c=0$ and $R_p=\{0\}$ or $\mathrm{\varnothing }$ according to the valuation. Structural induction on formulas shows its translated truths are exactly the propositional truths. Thus any finitely satisfiable propositional theory translates to a finitely satisfiable first-order theory. By the assumed compactness it has a nonempty model $M$. The function $p\mapsto 1$ exactly when $M\models R_p(c)$ is a valuation satisfying the original theory, by the same induction. F2 yields BPI. This also handles $P=\mathrm{\varnothing }$ and empty theories: the one-point interpretations and empty valuation still exist.

Return to the consistent $T_H$ of step 1.1. Use one propositional letter $p_{\sigma }$ for each $\sigma \in S$. Form a propositional theory $\mathrm{\Delta }$ with: $p_{\tau }$ for every $\tau \in T_H$; $\mathrm{\neg }{p}_{\mathrm{\perp }}$; $p_{\mathrm{\neg }\sigma }\leftrightarrow \mathrm{\neg }{p}_{\sigma }$; $p_{\sigma \wedge \rho }\leftrightarrow (p_{\sigma }\wedge p_{\rho })$; and $(p_{{\sigma }_1}\wedge \cdots \wedge p_{{\sigma }_n})\to p_{\rho }$ whenever the finite sentence set $\{{\sigma }_1,\dots ,{\sigma }_n\}$ derives $\rho$. The empty conjunction for $n=0$ is true, so all sentence theorems are required. Derivability is witnessed by finite strings, hence the collection of these requirements is a set.

Fix a finite ${\mathrm{\Delta }}_0\subseteq \mathrm{\Delta }$. Only finitely many letters $p_{\sigma }$ occur; call their sentence indices $S_0$. Enumerate this finite set and apply F5 finitely many times, starting at $T_H$, to obtain a consistent extension $K$ deciding every $\sigma \in S_0$. Set $v(p_{\sigma })=1$ if the positive decision is in $K$, and $0$ otherwise, and give all other letters value $0$. Consistency and F6 prevent both decisions being in $K$, so the negative decision is in $K$ exactly when $v(p_{\sigma })=0$. Every listed $p_{\tau }$ with $\tau \in T_H$ has value $1$, since a negative decision would contradict $\tau \in K$. Also $v(p_{\mathrm{\perp }})=0$ whenever that letter occurs. For a negation coherence requirement, equal positive values for $\sigma ,\mathrm{\neg }\sigma$ contradict consistency, and equal negative values give $\mathrm{\neg }\sigma ,\mathrm{\neg }\mathrm{\neg }\sigma \in K$, again a contradiction by F6. For a conjunction requirement, a positive conjunction with a negative conjunct contradicts elimination, while two positive conjuncts and a negative conjunction contradict introduction. Thus all Boolean coherence requirements in ${\mathrm{\Delta }}_0$ hold. Finally, if all antecedent letters of a deduction requirement are true, their sentences belong to $K$. F7 transfers their finite derivation of $\rho$ to $K$, and consistency with F6 prevents $\mathrm{\neg }\rho \in K$; hence the conclusion letter is true. A false antecedent satisfies the implication automatically. When $n=0$, the same argument transfers the theorem proof to $K$. Therefore $v\models {\mathrm{\Delta }}_0$. Only finitely many decisions were made, not a simultaneous choice of completions for all finite subsets.

BPI and F2 now give a valuation $v\models \mathrm{\Delta }$. Put $H=\{\sigma \in S:v(p_{\sigma })=1\}$. It contains $T_H$ and omits $\mathrm{\perp }$. Negation coherence makes it complete. If $H⊢\rho$, F7 yields finitely many premises ${\sigma }_1,\dots ,{\sigma }_n\in H$ deriving $\rho$; the corresponding requirement of $\mathrm{\Delta }$ forces $\rho \in H$. Thus $H$ is deductively closed, and it is consistent because a proof of $\mathrm{\perp }$ would put $\mathrm{\perp }$ in $H$. For each $\mathrm{\exists }x\varphi \in H$, F1 supplies its witness implication $\mathrm{\exists }x\varphi \to \varphi (c)$ in $T_H\subseteq H$. Closure under derivability puts $\varphi (c)$ in $H$. The seed from F1 remains in the language. All hypotheses of F4 therefore hold, giving a nonempty set model of $H$ and hence, by reduct to the original language, a model of $T$. No language enumeration, infinite succession of decisions, or representative choice is used. Together with step 1.2 this proves the equivalence. QED.