On synthesizing Skolem functions for first order logic formulae

TL;DR

This paper investigates the computability and automatic synthesis of Skolem functions in first-order logic, providing both negative and positive results, including algorithms for effective interpretation in certain theories.

Contribution

It offers a comprehensive analysis of when Skolem functions can be effectively interpreted and presents algorithms for their synthesis in first-order logic.

Findings

Computability of Skolem functions is generally impossible under mild assumptions.

A characterization of theories admitting effective Skolem functions is provided.

Algorithms for synthesizing Skolem functions in certain theories are developed.

Abstract

Skolem functions play a central role in the study of first order logic, both from theoretical and practical perspectives. While every Skolemized formula in first-order logic makes use of Skolem constants and/or functions, not all such Skolem constants and/or functions admit effectively computable interpretations. Indeed, the question of whether there exists an effectively computable interpretation of a Skolem function, and if so, how to automatically synthesize it, is fundamental to their use in several applications, such as planning, strategy synthesis, program synthesis etc. In this paper, we investigate the computability of Skolem functions and their automated synthesis in the full generality of first order logic. We first show a strong negative result, that even under mild assumptions on the vocabulary, it is impossible to obtain computable interpretations of Skolem functions. We then show a positive result, providing a precise characterization of first-order theories that admit effective interpretations of Skolem functions, and also present algorithms to automatically synthesize such interpretations. We discuss applications of our characterization as well as complexity bounds for Skolem functions (interpreted as Turing machines).