Compactness obstruction to expressing totality over an infinite codomain (source code)

= Compactness obstruction to expressing totality over an infinite codomain

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$.