[proofplan]
We prove the two inclusions. The inclusion $\operatorname{PSPACE} \subseteq \operatorname{NPSPACE}$ follows because every deterministic Turing machine is a nondeterministic Turing machine with exactly one available transition at each configuration. For the reverse inclusion, a language in $\operatorname{NPSPACE}$ has a polynomial nondeterministic space bound, and [Savitch's Theorem](/theorems/6220) converts that nondeterministic polynomial space bound into a deterministic quadratic-in-space bound, which is still polynomial.
[/proofplan]
[step:View deterministic polynomial-space machines as nondeterministic polynomial-space machines]
Let $L \subseteq \{0,1\}^*$ be a language with $L \in \operatorname{PSPACE}$. By definition of $\operatorname{PSPACE}$, there exist a deterministic Turing machine $M$ and an integer $k \in \mathbb{N}$ such that $M$ decides $L$ and uses space $O(n^k)$ on inputs of length $n$.
Every deterministic Turing machine is a special case of a nondeterministic Turing machine: at each configuration there is exactly one transition available. Therefore the same machine $M$, regarded as a nondeterministic Turing machine, decides $L$ using the same space bound $O(n^k)$. Hence $L \in \operatorname{NPSPACE}$.
Since $L$ was arbitrary, we have
\begin{align*}
\operatorname{PSPACE} \subseteq \operatorname{NPSPACE}.
\end{align*}
[/step]
[step:Convert nondeterministic polynomial space to deterministic polynomial space]
Let $L \subseteq \{0,1\}^*$ be a language with $L \in \operatorname{NPSPACE}$. By definition of $\operatorname{NPSPACE}$, there exist a nondeterministic Turing machine $N$ and an integer $k \in \mathbb{N}$ such that $N$ decides $L$ and uses space $O(n^k)$ on inputs of length $n$.
For any function $s:\mathbb{N} \to \mathbb{N}$, let $\operatorname{SPACE}(s(n))$ denote the class of languages decidable by a deterministic Turing machine using $O(s(n))$ work-tape space on inputs of length $n$, and let $\operatorname{NSPACE}(s(n))$ denote the class of languages decidable by a nondeterministic Turing machine using $O(s(n))$ work-tape space on inputs of length $n$.
By Savitch's Theorem (citing a result not yet in the wiki: Savitch's Theorem), for every space bound $s:\mathbb{N} \to \mathbb{N}$ with $s(n) \geq \log n$ for all sufficiently large $n$,
\begin{align*}
\operatorname{NSPACE}(s(n)) \subseteq \operatorname{SPACE}(s(n)^2).
\end{align*}
Apply this with the polynomial space bound $s(n) = n^k$. Since $k \in \mathbb{N}$ and natural numbers start at $1$, we have $k \geq 1$, so $n^k \geq \log n$ for all sufficiently large $n$. The machine $N$ uses $O(s(n))$ space, so $L \in \operatorname{NSPACE}(s(n))$. Therefore Savitch's Theorem gives
\begin{align*}
L \in \operatorname{SPACE}((n^k)^2).
\end{align*}
Since $(n^k)^2 = n^{2k}$ and $2k \in \mathbb{N}$, this is still a polynomial deterministic space bound. Hence $L \in \operatorname{PSPACE}$.
[guided]
We now prove the nontrivial inclusion $\operatorname{NPSPACE} \subseteq \operatorname{PSPACE}$. Let $L \subseteq \{0,1\}^*$ be a language with $L \in \operatorname{NPSPACE}$. The meaning of this membership is that there is some polynomial amount of space sufficient for a nondeterministic machine to decide $L$. More precisely, there exist a nondeterministic Turing machine $N$ and an integer $k \in \mathbb{N}$ such that $N$ decides $L$ and uses space $O(n^k)$ on every input of length $n$.
We first name the two space-bounded complexity classes used by Savitch's Theorem. For any function $s:\mathbb{N} \to \mathbb{N}$, the class $\operatorname{SPACE}(s(n))$ consists of the languages decidable by deterministic Turing machines using $O(s(n))$ work-tape space on inputs of length $n$. The class $\operatorname{NSPACE}(s(n))$ consists of the languages decidable by nondeterministic Turing machines using $O(s(n))$ work-tape space on inputs of length $n$.
The key tool is Savitch's Theorem (citing a result not yet in the wiki: Savitch's Theorem). It says that nondeterministic space can be simulated deterministically at the cost of squaring the space bound: if $s:\mathbb{N} \to \mathbb{N}$ satisfies $s(n) \geq \log n$ for all sufficiently large $n$, then
\begin{align*}
\operatorname{NSPACE}(s(n)) \subseteq \operatorname{SPACE}(s(n)^2).
\end{align*}
We verify the hypothesis of Savitch's Theorem for the space bound in this problem. Take $s:\mathbb{N} \to \mathbb{N}$ to be the polynomial function $s(n) = n^k$. Since $k \in \mathbb{N}$ and natural numbers start at $1$, we have $k \geq 1$. Hence $n^k$ eventually dominates $\log n$, so $s(n) \geq \log n$ for all sufficiently large $n$. Also, because $N$ uses $O(n^k)$ space, the definition above gives $L \in \operatorname{NSPACE}(s(n))$. Thus Savitch's Theorem applies to the nondeterministic polynomial-space computation deciding $L$.
The conclusion is that $L$ is decidable by a deterministic Turing machine using space
\begin{align*}
s(n)^2 = (n^k)^2.
\end{align*}
Using the exponent law for powers of $n$, this becomes
\begin{align*}
(n^k)^2 = n^{2k}.
\end{align*}
Because $2k \in \mathbb{N}$, the function $n^{2k}$ is still a polynomial space bound. Therefore $L$ belongs to $\operatorname{PSPACE}$.
[/guided]
[/step]
[step:Conclude equality of the two space classes]
The previous steps prove both inclusions:
\begin{align*}
\operatorname{PSPACE} \subseteq \operatorname{NPSPACE}
\end{align*}
and
\begin{align*}
\operatorname{NPSPACE} \subseteq \operatorname{PSPACE}.
\end{align*}
By mutual inclusion of classes of languages, we conclude
\begin{align*}
\operatorname{PSPACE} = \operatorname{NPSPACE}.
\end{align*}
[/step]
