Propositional compactness theorem

A set of propositions has a model exactly when every finite subset has a model. Syntactically, a contradiction uses only finitely many assumptions, and every consistent set extends by Zorn lemma to a maximal consistent set in propositional logic.

With atoms $p_{x,y}$, finitary propositions can enforce that the true pairs form an injective partial function. If the codomain is infinite, they cannot enforce that every $x$ has a value: adjoining every $\neg p_{x_0,y}$ remains finitely satisfiable, so compactness produces a model omitting $x_0$.