# 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?

• I don't understand. All formulae that have proofs have proofs shorter than $|x|^k$ for some $k$, and there's no way to talk about growth rates because formulae don't grow. Are you considering a fixed $k$ for this division? – Stella Biderman Mar 8 '17 at 19:20
• Yes, $k$ is a fixed parameter, as is the proof system, and the theory itself. SHORT-PROOFS is really a family of problems with those parameters. I'm supposing the theory is PA, the proof system is something reasonably expressive, and $k$ is something small like $3$ (large enough for the problem to be NP complete). – Dan Brumleve Mar 8 '17 at 19:29
• If $k$ is fixed, then I'm confused about the NP-completeness. 3SAT itself may be in SHORT-PROOFS for a given $k$, but other problems in NP that are reduced to 3SAT via a method involving a polynomial increase in problem size may require a larger exponent than $k$. – Matt Mar 10 '17 at 21:26
• Technically 3SAT is not a member of SHORT-PROOFS, it is a subset of it (as long as we choose a compatible encoding, and as long as we choose $k \gt 1$ so there is space to use a satisfying assignment as a witness). This matters because like you say not every NP-complete problem, even those with a compatible encoding, is a subset of SHORT-PROOFS, because some may require witnesses with an exponent larger than $k$. But SHORT-PROOFS is still NP-complete for any $k \gt 1$ (with assumptions about the proof system) because there is a polynomial-time reduction from such problems. – Dan Brumleve Mar 10 '17 at 22:08
• Are you familiar with the IP=PSPACE theorem? In Scott Aaronson words, "if a super-intelligent alien came to Earth, it could prove to us whether white or black has the winning strategy in chess, or if chess is a draw. It could play us and beat us, of course, but then all we'd know is that it's a better chess player. But it can prove to us which player has the winning strategy by reducing chess to this game of summing polynomials over large finite fields." – sdcvvc Mar 12 '17 at 17:31

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.
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.