Time hierarchy theorem

Remarks

The proof is a diagonalization. A machine $D$, on input $w$, simulates the machine encoded by $w$ on input $w$ for about $g(\abs{w})$ steps and answers the opposite. A universal machine simulates $t$ steps of any fixed multitape machine in $O(t \log t)$ steps. So every machine running in time $O(f(n))$ is fully simulated on long enough inputs, and it cannot decide the same language as $D$. Juris Hartmanis and Richard Stearns proved a first version of the theorem in 1965.

Consequence: P is strictly contained in EXPTIME, the class $\bigcup_k \mathrm{DTIME}(2^{n^k})$. Indeed $\mathrm{P} \subseteq \mathrm{DTIME}(2^n) \subsetneq \mathrm{DTIME}(2^{2n})$. Time-constructibility cannot be dropped: the Borodin gap theorem gives computable $f$ with $\mathrm{DTIME}(f(n)) = \mathrm{DTIME}(2^{f(n)})$.

Going deeper

For a student

The theorem gives the separation $\mathrm{P} \ne \mathrm{EXPTIME}$, one of few known unconditional separations. It says nothing about P versus NP, since NP is defined by another resource, nondeterministic time. A version for nondeterministic time also holds, with a different and subtler proof. Diagonalization proofs of this kind relativize, which is why the same method cannot settle P versus NP.