In the fragment of first order logic with only the quantifiers $\forall$ and $\exists!$, and quantifiers restricted to prenex position, we can define something roughly analogous to the Skolemization that's also unique. This seems like an interesting property, but I'm not sure what (if anything) it entails. Has this fragment of first-order logic been studied? Does it have a name?
Consider the fragment of first order logic with only prenex quantifiers and a matrix in negative-normal form. I'm not using the negative-normal form assumption, but I don't need greater variety. Restrict the allowed quantifiers to $\forall$ and $\exists!$. $\exists!$ is normally thought of as an orthographic abbreviation for $(\exists x \mathop. \varphi(x)) \land (\forall x \mathop. \forall y \mathop. \varphi(x) \land \varphi(y) \to x = y)$, but for now we are treating it as part of the syntax.
The quantifiers $\forall$ and $\exists$ pseudocommute with each other in higher order logic in the following sense. Either quantifier can be moved ahead of the other by taking a dependency on the previously quantified-over thing, with $\varphi[x:=e]$ referring to a capture-avoiding substitution.
$$ \forall x : S \mathop. \exists y : T \mathop. \varphi \;\;\text{is equivalent to}\;\; \exists y : S \to T \mathop. \forall x \mathop : S . \varphi[y:=y(x)] $$
$$ \exists x : S \mathop. \exists y : T \mathop. \varphi \;\;\text{is equivalent to}\;\; \forall y : S \to T \mathop. \exists x \mathop : S . \varphi[y:=y(x)] $$
The quantifiers $\forall$ and $\exists!$ also pseudocommute, but in exactly one direction.
$$ \forall x : S \mathop. \exists! y : T \mathop. \varphi \;\; \text{is equivalent to} \;\; \exists! y : S \to T \mathop. \forall x : S \mathop. \varphi[y := y(x)] $$
$$ \exists! x : S \mathop. \forall y : T \mathop. \varphi \;\; \text{is not equivalent to} \;\; \forall y : S \to T \mathop. \exists! x : S \mathop. \varphi[y:=y(x)] $$
To prove the bottom, consider the fact that there's a unique set $x$ that is a subset of every set $y$ is true (for the empty set), but for every class-function $f$ from set to set there exists a unique set $x$ such that $x$ is a subset of $f(x)$ is false.
To prove the top, let's think about a game between the player and the environment where the player is exceptionally bad at playing the game and will lose any time they have to make a choice, even if every option wins. If that player wins by going second, then the response function if they go first is unique. If that player can win by going first with a unique response function, then postponing that move until after the environment plays will also result in a unique move.
This one-sided pseudo-commutative property gives us an interesting property for theories that are expressible in this fragment of FOL, namely that the operation roughly analogous to Skolemization of said theory is deterministic.
That's kind of interesting. It means we can, in a certain sense, identify a model with its model in the pseudo-Skolemized theory without losing anything since the newly introduced functions are already unique.