What is the equivalent of SHORT-PROOFS for PSPACE? SHORT-PROOFS can be defined as the set of all first-order formulas $x$ that have a proof shorter than $\vert x \vert^k$.  With $k=\frac{3}{2}$, I like to think of it as the set of all theorems such that for every cubical box, if there is enough room on the side of the box to write the theorem, a proof of the theorem can fit inside the box.  It is in NP since the proof serves as a polynomial-size certificate and it is trivially complete since the identity function is a reduction from 3SAT.
Similarly we can define LONG-PROOFS as the set of all first-order formulas $x$ with a proof shorter than $2^{\vert x \vert ^ k}$, which is complete for NEXPTIME.
What is an analogous MEDIUM-PROOFS problem that is complete for PSPACE?
This would seemingly require a method of transforming a first-order formula to an instance of TQBF.  Or in other words, the formula is provable if and only if a certain game has a winning strategy.
Motivation: If there was such a method I am imagining it applied to a conjecture that is not in SHORT-PROOFS (assuming $NP \ne PSPACE$).  Even though this formula has no polynomial-size proof, it may correspond to a game that is winnable in a polynomial number of moves.  While we are unable to prove the game is always winnable, and are thus no closer to actually proving the conjecture, if it is the case that the game is easy to win quickly in practice (i.e. by some algorithm) maybe it would make sense to consider that as a heuristic in support of the conjecture.  It's sort of like how if a person claims to be able to play chess or some other finite game perfectly, there is no way for them to prove they have that ability since the game tree would be too large, but they can create evidence for it by beating all the top players, because IP=PSPACE they can demonstrate this (with some small error probability) using a polynomial-size interactive proof; can we do the same with arbitrary first-order arithmetic formulas?
 A: I think I figured out what I was looking for, but I am still interested in any references to help me understand the connections between complexity classes and proof systems (for example now I want to know what L and P correspond to in this scheme).
Define MEDIUM-PROOFS as the set of all theorems $x$ that have a proof which can be verified with a $\vert x \vert^k$-size sliding window, i.e. the proof is a list of sentences each of which is a direct logical consequence of some sentences appearing earlier in the proof at a distance bounded by a polynomial in the length of the theorem being proved, and ending with that theorem.  Or in other words, if the theorem can be written on the side of a box, its proof may not fit inside, but if it's full of blank paper there is enough paper to prove the theorem provided we erase earlier steps in the proof that we no longer need to refer back to; since we only ever write down anything for which we have evidence that is already written down at the time, if we conclude with the theorem written on the box, we can be sure it is provable even though some of the evidence for that evidence may have been erased.
MEDIUM-PROOFS is clearly in NPSPACE which is equal to PSPACE by Savitch's theorem.  Also I believe it is PSPACE-complete because TQBF reduces to it (using identity function), my attempt:
Given an instance $P = \forall x: x \lt 2 \rightarrow \exists y: y \lt 2 \land Q(x, y)$, suppose $\exists y: y \lt 2 \land Q(0,y)$ and $\exists y: y \lt 2 \land Q(1,y)$ both have $n$ bit encodings, and $P$ has a $n+m$ bit encoding.  Now assume as an inductive hypothesis that $\exists y: y \lt 2 \land Q(0,y)$ and $\exists y: y \lt 2 \land Q(1,y)$ both have proofs with $n^k$-size sliding windows.  We can't simply concatenate those proofs and then conclude $P$, because the proof of $\exists y: y \lt 2 \land Q(1,y)$ may be exponentially long and by the time we are finished with it the sliding window will no longer contain the already-proved sentence $\exists y: y \lt 2 \land Q(0,y)$.  But, since we are allowed to use a window of size $(n+m)^k$ to prove $P$, we can interleave the proof of $\exists y: y \lt 2 \land Q(1,y)$ with copies of the other sentence (its length is only $n$ and there are $m \cdot n^{k-1}$ extra bits to work with in the new window) so that both formulas are in the final window and we can conclude the proof with $P$.  So by induction on the number of quantifiers $P$ is in MEDIUM-PROOFS.
