Proof that EXPTIME is well founded I was toying around with the idea of complexity classes and I realized I don't know of a decision problem, off the top of my head that rigorously requires exponential time to solve.
What would be an example of such a problem and a proof of its hardness?
 A: A regular expression is a certain type of expression that represents a set of strings.  See the Wikipedia article for the details of regular expressions.
The regular expression non-universality problem is as follows:

Given a regular expression $R$ over some alphabet $\Sigma$, does there exist a string $s\in\Sigma^*$ for which $s\notin R$?

This is known to be PSPACE-complete, so there is a polynomial-time algorithm if $P=PSPACE$.
To the usual regular expression operations of union, concatenation, and Kleene closure, we will add a new operation: squaring.    If $R$ is any regular expression, let $R^2$ be an abbreviation for $RR$.  Note that this allows us to write very short abbreviations for certain very long expressions.   For example $RRRR…R$ with 65536 $R$s can be abbreviated to $(((…((R^2)^2)…)))$ with only 16 nested applications of $\bullet^2$.
The non-universality problem for this extended notion of regular expressions is provably intractable, requiring exponential time in the worst case, even if $P=PSPACE$.
For the proof, see: Arto Salomaa ''Computation and Automata'', Cambridge University Press, 1985 p.177–179, and the surrounding section 6.5 “Provably Intractable Problems”.  There is also a brief discussion in Garey and Johnson, with a reference.  But the basic idea is that a short input involving several squarings might require us to decide the corresponding problem for an exponentially-larger instance of the problem for basic regular expressions.
