A Stone–Weierstrass theorem for Polish spaces, given by logic

The Stone–Weierstrass theorem obtains every continuous function on a compact space as a uniform limit of functions built from a separating family by finitely many operations. We extend the theorem to every separable metric space, and in particular to every Polish space: every bounded uniformly continuous function is a uniform limit of functions built from countably many bounded separating functions by rational linear combinations, maxima and minima, and by countable suprema and infima whose admission is decided by weights computed from the construction; the functions so built are exactly the bounded Lipschitz functions. The theorem was discovered, and first proved, in infinitary real-valued logic, whose a priori bounds are the weights, and the proof by logic shows that the theorem is equivalent to an approximate form of Beth’s definability theorem, as Reggio proved the classical theorem equivalent to the Beth definability property of an infinitary equational logic. For readers outside logic, we also give a purely topological-analytic proof.