Editing Space hierarchy theorem (section)

== Corollaries ==

=== Corollary 1 ===

''For any two functions <math>f_1</math>, <math>f_2: \mathbb{N} \longrightarrow
\mathbb{N}</math>, where <math>f_1(n)</math> is <math>o(f_2(n))</math> and <math>f_2</math> is space-constructible, <math>\mathsf{SPACE}(f_1(n)) \subsetneq \mathsf{SPACE}(f_2(n))</math>.''

This corollary lets us separate various space complexity classes.
For any natural number k, the function <math>n^k</math> is space-constructible. Therefore for any two natural numbers <math>k_1 < k_2</math> we can
prove <math>\mathsf{SPACE}(n^{k_1}) \subsetneq \mathsf{SPACE}(n^{k_2})</math>.

=== Corollary 2 ===

:[[NL (complexity)|NL]] ⊊ [[PSPACE]].

==== Proof ====

[[Savitch's theorem]] shows that <math>\mathsf{NL} \subseteq \mathsf{SPACE}(\log^2n)</math>, while the space hierarchy theorem shows that <math>\mathsf{SPACE}(\log^2n) \subsetneq \mathsf{SPACE}(n)</math>. The result is this corollary along with the fact that TQBF &notin; NL
since TQBF is PSPACE-complete.

This could also be proven using the non-deterministic space hierarchy theorem to show that NL ⊊ NPSPACE, and using Savitch's theorem to show that PSPACE = NPSPACE.

=== Corollary 3 ===

:[[PSPACE]] ⊊ [[EXPSPACE]].

This last corollary shows the existence of decidable problems that are intractable. In other words, their decision procedures must use more than polynomial space.

=== Corollary 4 ===

There are problems in {{sans-serif|PSPACE}} requiring an arbitrarily large exponent to solve; therefore {{sans-serif|PSPACE}} does not collapse to {{sans-serif|DSPACE}}(''n''<sup>''k''</sup>) for some constant ''k''.

=== Corollary 5 ===

:SPACE(''n'') ≠ [[PTIME]].

To see it, assume the contrary, thus any problem decided in space <math>O(n)</math> is decided in time <math>O(n^c)</math>, and any problem <math>L</math> decided in space  <math>O(n^b)</math> is decided in time <math>O((n^b)^c)=O(n^{bc})</math>. Now <math>\mathsf{P}:=\bigcup_{k\in\mathbb N}\mathsf{DTIME}(n^k)</math>, thus P is closed under such a change of bound, that is <math>\bigcup_{k\in\mathbb N}\mathsf{DTIME}(n^{bk})\subseteq\mathsf{P}</math>, so <math>L\in\mathsf{P}</math>. This implies that for all <math>b, \mathsf{SPACE}(n^b)\subseteq\mathsf{P}\subseteq\mathsf{SPACE}(n)</math>, but the space hierarchy theorem implies that <math>\mathsf{SPACE}(n^2)\not\subseteq\mathsf{SPACE}(n)</math>, and Corollary 6 follows. Note that this argument neither proves that <math>\mathsf{P}\not\subseteq\mathsf{SPACE}(n)</math> nor that <math>\mathsf{SPACE}(n)\not\subseteq\mathsf{P}</math>, as to reach a contradiction we used the negation of both sentences, that is we used both inclusions, and can only deduce that at least one fails. It is currently unknown which fail(s) but conjectured that both do, that is that <math>\mathsf{SPACE}(n)</math> and <math>\mathsf{P}</math> are incomparable -at least for deterministic space.<ref>{{cite web | url=https://mathoverflow.net/questions/40770/how-do-we-know-that-p-linspace-without-knowing-if-one-is-a-subset-of-the-othe/40771#40771 | title=How do we know that P != LINSPACE without knowing if one is a subset of the other? }}</ref> This question is related to that of the time complexity of (nondeterministic) [[linear bounded automata]] which accept the complexity class <math>\mathsf{NSPACE}(n)</math> (aka as [[context-sensitive languages]], CSL); so by the above CSL is not known to be decidable in polynomial time -see also [[Linear_bounded_automaton#LBA_problems|Kuroda's two problems on LBA]].