The most nonelementary theory

We give a direct proof by generic reduction that testing validity of formulas in a decidable rudimentary theory Ω of finite typed sets (Henkin, Fundamenta Mathematicæ 52 (1963) 323–344) requires space and time exceeding infinitely often(1)where n denotes the length of input. This gives the highest currently known lower bound for a decidable logical theory and affirmatively settles Problem 10.13 from (Compton and Henson, Ann. Pure Applied Logic 48 (1990) 1–79):

Is there a “natural” decidable theory with a lower bound of the form exp_∞(f(n)), where f is not linearly bounded?

The highest previously known lower (and upper) bounds for “natural” decidable theories, like WS1S, S2S, are of the form exp_∞(dn), with just linearly growing stacks of twos.Originally, the lower bound (1) for Ω was settled in (12th Annual IEEE Symposium on Logic in Computer Science (LICS’97), 1997, 294–305) using the powerful uniform lower bounds method due to Compton and Henson, and probably would never be discovered otherwise. Although very concise, the original proof has certain gaps, because the method was pushed out of the limits it was originally designed and intended for, and some hidden assumptions were violated. This results in slightly weaker bounds—the stack of twos in (1) grows subexponentially, but superpolynomially, namely, as for formulas with fixed quantifier prefix, or as 2^cn/log(n) for formulas with varying prefix. The independent direct proof presented in this paper closes the gaps and settles the originally claimed lower bound (1) for the minimally typed, succinct version of Ω.