when skolemizing (like here) apparently we only take into account universally quantified variables, for example for the formula$\forall x\, \exists y : D(x,y)$ for some predicate $D$. If we skolemize this expression, we get $D\big(x,f(x)\big)$.
My question now is about what happens if we have multiple existentially quantified variables. For example this expression: $$\exists z \, \forall x \, \exists y : D(x,y,z) \,\,\xrightarrow{\text{Skolemizing}}\,\,D\big(x,f(x),z\big).$$Although $f$ should intuitively be a function of $x$ and $z$, if we follow the procedure described here and in numerous other textbooks, if is just a function depending on $x$, like in above's formula.
Why is that? Is it just clear to everybody that $f$ clearly depends on $z$ anyway, therefore we don't write it down?
Any explanation would be highly appreciated!
2026-04-12 07:10:35.1775977835