Buss defined $V_2^1$ as a second-order bounded arithmetic corresponding to $\mathsf{PSPACE}$. Later, Skelley introduced $W_1^1$, a third-order bounded arithmetic of $\mathsf{PSPACE}$. Since the question $\mathsf{P =^? PSPACE}$ is still open, I think proof theory, especially incompleteness theorem related results in $V_2^1$ and $W_1^1$, deserves more attention. Similar ideas have already been studied a lot in the context of $S_2^i$ and $T_2^i$.
