Beth definability and the Stone-Weierstrass Theorem

The Stone-Weierstrass Theorem for compact Hausdorff spaces is a basic result of functional analysis with far-reaching consequences. We introduce an equational logic $\log_Δ$ associated with an infinitary variety Δ and show that the Stone-Weierstrass Theorem is a consequence of the Beth definability property of $\log_Δ$, stating that every implicit definition can be made explicit. Further, we define an infinitary propositional logic $\Log_Δ$ by means of a Hilbert-style calculus and prove a strong completeness result whereby the semantic notion of consequence associated with $\Log_Δ$ coincides with $\log_Δ$.