The compactness tree yields a prime ideal for an enumerated Boolean algebra

Let $B_n=⟨b(0),\dots ,b(n-1)⟩$ and let level $n$ consist of all homomorphisms $e:B_n\to \mathbf{2}$, ordered by restriction. Each level is finite: $e$ is determined by the bit string $(e(b(0)),\dots ,e(b(n-1)))$, even when the enumeration repeats elements.

Level $0$ has the unique homomorphism on $\{0,1\}$ because $B$ is nontrivial. By F2 every level-$n$ node extends to level $n+1$, so finite induction makes every level nonempty.

Diagram compactness implies the prime-ideal assertion as follows. For the supplied enumeration of $B$, use variables $y_n$ and enumerate the requirements $y_i=0$ when $b(i)=0$, $y_i=1$ when $b(i)=1$, and $y_i=\mathrm{\neg }{y}_j$, $y_i=y_j\wedge y_k$, or $y_i=y_j\vee y_k$ whenever the corresponding equality holds in $B$, including $y_i=y_j$ for repeated enumerates. Every finite set of requirements is satisfied by a homomorphism on the finite subalgebra generated by its finitely many mentioned elements, using F2. A total solution induces a well-defined homomorphism $B\to \mathbf{2}$, whose zero fibre is prime by F1.

Call a node good if it has extensions at arbitrarily high levels. The level-$0$ node is good by step 2.1. A good node has at least one good immediate successor: its possible successors have bit $0$ or $1$, and if both existing successors had finite extension bounds, their maximum would bound the parent. Recursively take the bit-$0$ good successor when it exists and otherwise the bit-$1$ good successor. This definable binary preference produces a coherent branch $(e_n)$ in ZF, without applying choice or general König's lemma.

For $x\in B$, define $e(x)$ to be the unique value $e_n(x)$ occurring once $x\in B_n$; surjectivity supplies such an $n$ and coherence makes the value independent of $n$ and of repetitions in $b$. Every finite Boolean calculation occurs in some $B_n$, where $e_n$ preserves it, so $e:B\to \mathbf{2}$ is a total homomorphism.

The set $I=e^{-1}(0)$ contains $0$, omits $1$, is downward closed and join-closed, and $x\wedge y\in I$ implies $e(x)e(y)=0$, hence $x\in I$ or $y\in I$. Thus $I$ is a proper prime ideal.

The prime-ideal assertion implies diagram compactness. For an enumerated finitely satisfiable diagram $\mathrm{\Gamma }$, let $F$ be the countable free Boolean algebra of finite terms in its variables and let $J$ be the ideal generated by $p$ for every requirement $p=0$ and by $\mathrm{\neg }p$ for every requirement $p=1$. The ideal is proper: an equation $1\le g_1\vee \cdots \vee g_m$ with generators $g_j$ would be contradicted by a two-valued valuation satisfying their finitely many requirements. Hence $F\mathrm{/}J$ is a nontrivial enumerated Boolean algebra. A prime ideal of $F\mathrm{/}J$ gives a homomorphism to $\mathbf{2}$ by value $0$ on the ideal and $1$ on its complement; composed with the variables, it satisfies every requirement in $\mathrm{\Gamma }$.

Steps 5.1, 6.1, and 2.2 prove the prime-ideal claim and both directions of the stated equivalence in ZF. The only infinite recursion, step 3.1, uses a fixed preference between two bits; all other witness collections occur over a single finite set.