Herbrand strategies and the “greater deducibility” relation

A Herbrand strategy $T$ is that algorithm which for an arbitrary prenex formula $F$ gives a sequence of its Herbrand disjunctions. Let $F^T$ be the first tautology in this sequence. $T$ is complete if for every deducible $F$, FT exists. The strategy $T$ gives k superfluous terms for $F$ if k disjuncts can be removed from $F^T$ while preserving its tautological character; $T$ is optimal for $F$ if there exists no Herbrand disjunction for $F$ shorter than $F^T$. There are complete strategies that give arbitrarily small proportion of terms for all $F$. There are also strategies that work with incomplete information about $F$ (e.g., with the signature of $F$ or a list of its elementary subformulas). For any such complete strategy we can construct a class of formulas for which the proportion of superfluous terms tends to 1 as the length of the formula tends to $\infty$. However, there is no possible algorithm for finding the superfluous terms which may be dropped. Even for strategies that require complete and uniform review of all possible permutations of terms (for a given signature), the class of formulas for which $T$ is optimal is undecidable. The proof uses properties of the relation "$F$ is more deducible than $G$", studied in terms of the general theory of calculi.