The most nonelementary theory (Q598194)

The author affirmatively settles the following problem [\textit{K. J. Compton} and \textit{C. W. Henson}, Ann. Pure Appl. Logic 48, 1--79 (1990; Zbl 0705.03017)]: ``Is there a `natural' decidable theory with a lower bound of the form \(\exp_\infty(f(n))\), where \(f\) is not linearly bounded?'' The author proves that testing the validity of formulas in a decidable rudimentary theory of finite typed sets requires such a lower bound.