On synthesizing Skolem functions for first order logic formulae

Skolem functions play a central role in logic, from eliminating quantifiers in first order logic formulas to providing functional implementations of relational specifications. While classical results in logic are only interested in their existence, the question of how to effectively compute them is also interesting, important and useful for several applications. In the restricted case of Boolean propositional logic formula, this problem of synthesizing Boolean Skolem functions has been addressed in depth, with various recent work focussing on both theoretical and practical aspects of the problem. However, there are few existing results for the general case, and the focus has been on heuristical algorithms. In this article, we undertake an investigation into the computational hardness of the problem of synthesizing Skolem functions for first order logic formula. We show that even under reasonable assumptions on the signature of the formula, it is impossible to compute or synthesize Skolem functions. Then we determine conditions on theories of first order logic which would render the problem computable. Finally, we show that several natural theories satisfy these conditions and hence do admit effective synthesis of Skolem functions.