The “Hardest” natural decidable theory

We prove that any decision procedure for a modest fragment of L. Henkin´s theory of pure propositional types requires time exceeding a tower of 2´s of height exponential in the length of input. Until now the highest known lower bounds for natural decidable theories were at most linearly high towers of 2´s and since mid-seventies it was an open problem whether natural decidable theories requiring more than that exist. We give the affirmative answer. As an application of this today´s strongest lower bound we improve known and settle new lower bounds for several problems in the simply typed lambda calculus