 A wff of the form \(\forall \bx^1 \ldots \forall \bx^n\bC\), where \(\bC\) is quantifier-free, is provable in \(\cT\) iff \({\downarrow} \bC\) is tautologous. On the other hand, the decision problem for wffs of the form \(\exists \bz\bC\), where \(\bC\) is quantifier-free, is unsolvable. (By contrast, the corresponding decision problem in first-order logic with function symbols is known to be solvable (Maslov 1967).) Since irrelevant or vacuous quantifiers can always be introduced, this shows that the only solvable classes of wffs of \(\cT\) in prenex normal form defined solely by the structure of the prefix are those in which no existential quantifiers occur.