Is there a notion of Skolemization for continuous logic (that of Ben Yaacov)? It seems to me that a Skolem function would be a minimizer, and minimizers are not continuous (from the parameters of the function being minimized).
If there isn't, is there a trick that gives the same effect (turning a formula into a universal one).
I an not sure what you are looking for exactly. Note that $\sup$ and $\inf$ are included as operators in the language so any Skolemization would need to have them.
BenYaacov et al. give some quantifier elimination results for continuous logic theories in the following paper:
Here is an alternative view that I personally find easier to work with and might be helpful:
theories in continuous logic can be thought of as theories in first-order rational Pavelka logic $RPL\forall$, which is in turn a conservative extension of classical first-order logic.
We use this to construct Henkin models for CL in the following paper:
The reference to learn more about $RPL\forall$ is
You may want to also check:
Many of the things you might want to do with Skolemization (such as producing Ehrenfeucht-Mostowski models) can be done by passing to a discretization of your theory and then Skolemizing there. Without having actually looked, I believe this is very similar to the technique Kaveh mentioned in their answer. (Although I should note that Henkin models can be constructed directly in continuous logic without too much difficulty.)
Of course, in some sense this requires modifying the underlying metric. As you point out, minimizing (or even approximately minimizing) is not continuous, even in compact structures, so a naïve definition of Skolemization is certainly not always possible. There is a weaker notion:
This is equivalent to ordinary Skolemization in discrete first-order logic, but even with this it's unclear that you can always pass to an expansion which is weakly Skolemized without modifying the metric.
With regards to weakly Skolemizing theories, the best that I know at the moment is this:
Every uniformly locally compact theory can be weakly Skolemized.
Every ultrametric theory can be weakly Skolemized.
If a theory $T$ has a weakly Skolemized expansion $T'$, then there is an intermediate expansion $T''$ (i.e., $T \subseteq T'' \subseteq T'$) such that the language of $T''$ is no larger than the language of $T$. (This is not a priori obvious.)
(Thinking about it now, I suspect that ultrametric theories can be Skolemized in a more direct sense. This is certainly true for ultrametric theories with discrete distance sets.) Beyond this I don't know very much. For instance, I don't know whether every expansion of Hilbert space can be weakly Skolemized. I gave a talk about this and also touch on it briefly in Remark 3.5.7 of my thesis.
If I interpret your broader question in what I would consider to be a 'non-trivially continuous' way, by which I mean, does every continuous theory $T$ have an expansion $T'$ with the same metric such that every formula is equivalent to a universal formula (or definable predicate, if you insist on considering those as distinct from formulas) over $T'$, then I believe it is currently unknown whether this always holds. (EDIT: I realized I was being dumb with this comment. Morleyization works fine in continuous logic and allows you to pass to an expansion with quantifier elimination, which is strictly stronger. That said, part of what Skolemization gives you is that the resulting theory is axiomatized by universal sentences. Since the standard semantic characterization of universal sentences works in continuous logic, I think this is equivalent to asking that the theory have a Skolemization in the strong sense, which I suspect is not always possible.) It is even unclear to me at the moment whether a theory $T$ having a weak Skolemization implies that it has an expansion with the property that every formula is logically equivalent to a universal formula, because, as I mention in my thesis, weak Skolemization is not witnessed by definable functions, but rather certain nice families of uniformly definable partial functions.
