On the complexity of finding falsifying assignments for Herbrand disjunctions

Pavel Pudlak

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 falsifiab…