 Given a prenex formula, the Skolem normal form \(A^S\) is defined dually to \(A^H\), i.e., by replacing existentially quantified variables by witnessing functions. If \(\Gamma\) is a set of prenex sentences, let \(\Gamma^S\) denote the set of their Skolem normal forms. Using the deduction theorem and Herbrand’s theorem, it is  not hard to show that the following are pairwise equivalent: \[ \begin{align} \Gamma &amp;\text{ proves } A \\ \Gamma &amp;\text{ proves } A^H \\ \Gamma^S &amp;\text{ proves }A \\ \Gamma^S &amp;\text{ proves } A^H \end{align} \]   