<p>I'm wondering if there are any references on "reverse skolemization", that is, converting a formula with functions into one purely consisting of quantifiers by eliminating function applications.</p>

<p>I'm working in a boolean domain, and my end goal is to make something that can be solved by a QSAT solver.</p>

<p>For example, if I have a formula <span class="math-container">$\phi$</span> like this:  </p>

<p><span class="math-container">$\exists f : \mathbb{B}^n \to \mathbb{B}^n \ldotp \exists g : \mathbb{B}^n \to \mathbb{B} \ldotp \forall x : \mathbb{B}^n \ldotp g(x) \implies g(f(x)) $</span></p>

<p>I want to be able to convert it into an equi-satisfiable formula that quantifies over booleans, not functions, i.e. a formula whose skolemization is  <span class="math-container">$\phi$</span>.</p>

<p>Is this possible, and if so, are there any references for how to do this algorithmically in the general case?</p>

CC BY-SA 4.0
2019-07-08T06:13:16.430Z
You can obviously replace a quantifier over $f\colon\{0,1\}^n\to\{0,1\}^m$ by $m2^n$ Boolean quantifiers specifying the truth-table of $f$. This will give an exponentially larger formula. I’m pretty sure this is best possible in general, as the problem should be complete for alternating exponential time with polynomially many alternations, or something like that.
Emil Jeřábek
CC BY-SA 4.0
2019-07-08T07:17:35.800Z
In fact, already the special case of sentences of the form $\exists f\colon\mathbb B^n\to\mathbb B\,\forall x_1,\dots,x_m\in\mathbb B\,\phi(f,\vec x)$ with $\phi$ quantifier-free, is NEXP-complete to evaluate, hence it should not have any subexponential reduction to a PSPACE-complete problem like QSAT.
Emil Jeřábek
CC BY-SA 4.0
2019-07-08T16:53:35.703Z
Do you have a reference for the NEXPTIME-completeness of SAT with boolean functions?
Joey Eremondi
CC BY-SA 4.0
2019-07-09T13:49:38.273Z
I guess there are various variants of such results appearing in the literature. The specific result abount NEXP-completeness of sentences of the form $\exists f\colon\mathbb B^n\to\mathbb B\,\forall x_1,\dots,x_m\in\mathbb B\,\phi(f,\vec x)$ with quantifier-free $\phi$ is a restatement of Lemma 3.1 in my paper “Complexity of admissible rules” (note that quantification over $X\in\mathcal{P(P(}[n]))$ is the same as quantification over $\mathbb B^n\to\mathbb B$, and likewise, quantification over $a\in\mathcal P([n])$ is equivalent to quantification over $\mathbb B^n$). More generally, ...
Emil Jeřábek
CC BY-SA 4.0
2019-07-09T13:55:50.750Z
... Theorem 2.3 in my preprint “Rules with parameters in modal logic II” shows that for any constant $k$, the truth of sentences of the form $\exists f_1\colon\mathbb B^n\to\mathbb B\,\forall f_2\colon\mathbb B^n\to\mathbb B\,\dots\,Q f_k\colon\mathbb B^n\to\mathbb B\,\overline Q x_1,\dots,x_m\in\mathbb B\,\phi(\vec f,\vec x)$, where $\phi$ is quantifier-free, is complete for the level $\Sigma_k^{\exp}$ of the exponential hierarchy. (Here, $Q$ is $\exists$ or $\forall$ according to if $k$ is odd or even, and $\overline Q$ is its dual.) Of course, the $\Sigma_k^{\exp}$ upper bound holds ...
Emil Jeřábek
CC BY-SA 4.0
2019-07-09T13:59:56.103Z
... more generally for evaluation of sentences in prenex normal form whose prefix consists of $k$ alternating *blocks* of Boolean function quantifiers (starting with $\exists$) followed by (or even interleaved with) arbitrary ordinary Boolean quantifiers. And as I already wrote, the general problem of evaluating sentences with Boolean function quantifiers without restrictions on quantifier alternation should be complete for alternating exponential time with polynomially many alternations, but I don’t know if this appeared somewhere in the literature. (The upper bound is again obvious.)
Emil Jeřábek
CC BY-SA 4.0
2019-07-10T06:13:14.950Z
Just a note: the reverse of skolemization is trivially possible if each function symbol is used only once, in which case you can replace the application of the function with a quantifier.
Nicola Gigante
CC BY-SA 4.0
2019-07-12T22:47:12.533Z
When Skolemizing we never get "nested" Skolem functions - so your example can't occur because of the "$g(f(-))$" bit. Indeed, plenty of sentences of this form aren't equivalent to first-order sentences at all - see e.g. [this old MSE question](https://math.stackexchange.com/questions/3150259/can-we-specify-in-a-first-order-formula-that-a-variable-depends-not-on-all-previ?noredirect=1&lq=1).
Noah Schweber
<reference-request><lo.logic><sat><boolean-functions><first-order-logic>
Reverse Skolemization?
Joey Eremondi
# Reverse Skolemization?

(Asked by: username_0 on 2019-07-07)

I'm wondering if there are any references on "reverse skolemization", that is, converting a formula with functions into one purely consisting of quantifiers by eliminating function applications.

I'm working in a boolean domain, and my end goal is to make something that can be solved by a QSAT solver.

For example, if I have a formula $\phi$ like this:

$\exists f : \mathbb{B}^n \to \mathbb{B}^n \ldotp \exists g : \mathbb{B}^n \to \mathbb{B} \ldotp \forall x : \mathbb{B}^n \ldotp g(x) \implies g(f(x)) $

I want to be able to convert it into an equi-satisfiable formula that quantifies over booleans, not functions, i.e. a formula whose skolemization is $\phi$.

Is this possible, and if so, are there any references for how to do this algorithmically in the general case?

**Tags:** reference-request, lo.logic, sat, boolean-functions, first-order-logic
> **Comments:**
> **username_1**: You can obviously replace a quantifier over $f\colon\{0,1\}^n\to\{0,1\}^m$ by $m2^n$ Boolean quantifiers specifying the truth-table of $f$. This will give an exponentially larger formula. I’m pretty sure this is best possible in general, as the problem should be complete for alternating exponential time with polynomially many alternations, or something like that.  
> **username_1**: In fact, already the special case of sentences of the form $\exists f\colon\mathbb B^n\to\mathbb B\,\forall x_1,\dots,x_m\in\mathbb B\,\phi(f,\vec x)$ with $\phi$ quantifier-free, is NEXP-complete to evaluate, hence it should not have any subexponential reduction to a PSPACE-complete problem like QSAT.  
> **username_0**: Do you have a reference for the NEXPTIME-completeness of SAT with boolean functions?  
> **username_1**: I guess there are various variants of such results appearing in the literature. The specific result abount NEXP-completeness of sentences of the form $\exists f\colon\mathbb B^n\to\mathbb B\,\forall x_1,\dots,x_m\in\mathbb B\,\phi(f,\vec x)$ with quantifier-free $\phi$ is a restatement of Lemma 3.1 in my paper “Complexity of admissible rules” (note that quantification over $X\in\mathcal{P(P(}[n]))$ is the same as quantification over $\mathbb B^n\to\mathbb B$, and likewise, quantification over $a\in\mathcal P([n])$ is equivalent to quantification over $\mathbb B^n$). More generally, ...  
> **username_1**: ... Theorem 2.3 in my preprint “Rules with parameters in modal logic II” shows that for any constant $k$, the truth of sentences of the form $\exists f_1\colon\mathbb B^n\to\mathbb B\,\forall f_2\colon\mathbb B^n\to\mathbb B\,\dots\,Q f_k\colon\mathbb B^n\to\mathbb B\,\overline Q x_1,\dots,x_m\in\mathbb B\,\phi(\vec f,\vec x)$, where $\phi$ is quantifier-free, is complete for the level $\Sigma_k^{\exp}$ of the exponential hierarchy. (Here, $Q$ is $\exists$ or $\forall$ according to if $k$ is odd or even, and $\overline Q$ is its dual.) Of course, the $\Sigma_k^{\exp}$ upper bound holds ...  
> **username_1**: ... more generally for evaluation of sentences in prenex normal form whose prefix consists of $k$ alternating *blocks* of Boolean function quantifiers (starting with $\exists$) followed by (or even interleaved with) arbitrary ordinary Boolean quantifiers. And as I already wrote, the general problem of evaluating sentences with Boolean function quantifiers without restrictions on quantifier alternation should be complete for alternating exponential time with polynomially many alternations, but I don’t know if this appeared somewhere in the literature. (The upper bound is again obvious.)  
> **username_2**: Just a note: the reverse of skolemization is trivially possible if each function symbol is used only once, in which case you can replace the application of the function with a quantifier.  
> **username_3**: When Skolemizing we never get "nested" Skolem functions - so your example can't occur because of the "$g(f(-))$" bit. Indeed, plenty of sentences of this form aren't equivalent to first-order sentences at all - see e.g. [this old MSE question](https://math.stackexchange.com/questions/3150259/can-we-specify-in-a-first-order-formula-that-a-variable-depends-not-on-all-previ?noredirect=1&lq=1).  

---

## 0 answers

