Does more time or space actually buy more computational power? The hierarchy theorems answer yes — provably, via diagonalization.
Definition · Time hierarchy theorem
For reasonable (time-constructible) bounds, there are languages decidable in time O(f(n)) but not in any meaningfully smaller time. More resources ⇒ strictly more decidable languages.
The proof builds a machine that diagonalizes against every machine running within the smaller bound — echoing the halting-problem argument, now counting steps instead of accept/reject.
A rare certainty
Unlike P vs NP, these separations are proved. For example P ⊊ EXPTIME is a theorem, not a conjecture.