Let $\mathcal{L}$ be a countable propositional language and let $\Gamma$ be a set of propositions of $\mathcal{L}$ (i.e. $\Gamma \subseteq \text{Prop}(\mathcal{L})$).
Definition: $\Gamma$ is satisfiable if there exists an evaluation function $V:\text{Prop}(\mathcal{L}) \to \{\bot,\top\}$ such that $V(C)=\top$ for every $C \in \Gamma$ ($\{\bot,\top\}$ is the 2-elements boolean algebra).
Compactness theorem for countable languages: if every finite subset of $\Gamma$ is satisfiable then $\Gamma$ is satisfiable.
The compactness theorem for countable languages can be proved in ZF (Zermelo-Fraenkel set theory). Is it provable also in a constructive way (i.e. in CZF or in IZF)?
Otherwise, does the compactness theorem for countable languages imply some intuitionistic taboo?
No, this cannot be constructively proved.
Consider a one-proposition language $\mathcal{L} = \{P\}$. Fix a consider a meta-level proposition $Q$. Define $\Gamma = \{P \mid Q\} \cup \{\neg P \mid \neg Q\}$.
I claim every finite subset of $\Gamma$ is satisfiable. This is fairly straightforward, since every finite subset of $\Gamma$ is either $\emptyset$, $\{P\}$, or $\{\neg P\}$.
If $\Gamma$ is satisfiable, we examine the truth value $P$ takes in the model. If $P \mapsto \top$, then we know $\neg \neg Q$. And if $P \mapsto \bot$, then we know $\neg Q$. So if $\Gamma$ is satisfiable, then either $\neg Q$ or $\neg \neg Q$ holds.
But we cannot constructively prove $\neg Q \lor \neg \neg Q$.
Conversely, if we assume $\forall Q (\neg Q \lor \neg \neg Q)$, then we can prove the compactness theorem for $\mathcal{L} = \mathbb{N}$. We can define
$$V(i) = \begin{cases} \top & \text{there is no finite set } S \subseteq \Gamma \text{ such that there is no satisfier } V’ \text{ of } S \text{ with } \forall j < i, V’(j) = V(j) \text { and } V’(i) = \top \\ \bot & otherwise \end{cases} $$
on the atomic propositions (and extend in the obvious way to all propositions).
We can then prove by induction that for all $i \in \mathbb{N}$, for all finite subsets $S \subseteq \Gamma$, there exists a truth assignment $V’ \models S$ such that for all $j \leq i$, $V’(j) = V(j)$. It follows that $V \models \Gamma$.