On the complexity of finding falsifying assignments for Herbrand disjunctions

TL;DR

This paper demonstrates that finding falsifying assignments for Herbrand disjunctions derived from consistent sentences is computationally hard, linking it to the complexity of total polynomial search problems.

Contribution

It establishes a reduction from any total polynomial search problem to the problem of finding falsifying assignments for Herbrand disjunctions, highlighting the problem's computational difficulty.

Findings

Finding such falsifying assignments is as hard as any total polynomial search problem.

The complexity of these problems is connected to the conjecture that no complete total polynomial search problems exist.

The results imply limitations on the reducibility of search problems related to consistent sentences.

Abstract

Suppose that $\Phi$ is a consistent sentence. Then there is no Herbrand proof of $\neg \Phi$, which means that any Herbrand disjunction made from the prenex form of $\neg \Phi$ is falsifiable. We show that the problem of finding such a falsifying assignment is hard in the following sense. For every total polynomial search problem $R$, there exists a consistent $\Phi$ such that finding solutions to $R$ can be reduced to finding a falsifying assignment to an Herbrand disjunction made from $\neg \Phi$. It has been conjectured that there are no complete total polynomial search problems. If this conjecture is true, then for every consistent sentence $\Phi$, there exists a consistence sentence $\Psi$, such that the search problem associated with $\Psi$ cannot be reduced to the search problem associated with $\Phi$.