a variation of Posts Correspondence Problem for bounded length input (but not the standard "bounded" version eg in Garey/Johnson that is called "bounded PCP" that limits the number of blocks in the solution to the cardinality of the block set) is complete for NEXPSpace and therefore larger than NP which is properly in Pspace. [1]

ie let there also be an input parameter $n$ specified in binary that determines the maximal length of the PCP answer. this is apparently complete for NEXPSpace via a straightfwd proof. havent seen a proof in the literature. it proceeds in a way similar to the construction relating it to TMs in [2]

note that all problems that are known to be larger than NP are also larger than PSpace. otherwise it (a proof of a language that is not in NP but is still in PSpace) might be something close to a coNP$\neq$NP and therefore also P$\neq$NP proof (because P is closed under complement), or resolve some other "nearby" currently open complexity class separation.

[1] Decidable restrictions of the Post Correspondence Problem

[2] A polynomial reduction from any NP-complete problem to bounded PCP

a variation of Posts Correspondence Problem for bounded length input (but not the standard "bounded" version eg in Garey/Johnson that is called "bounded PCP" that limits the number of blocks in the solution to the cardinality of the block set) is complete for NEXPSpace and therefore larger than NP which is properly in Pspace. [1]

ie let there also be an input parameter $n$ specified in binary that determines the maximal length of the PCP answer. this is apparently complete for NEXPSpace via a straightfwd proof. havent seen a proof in the literature. it proceeds in a way similar to the construction relating it to TMs in [2]

note that all problems that are known to be larger than NP are also larger than PSpace. otherwise it (a proof of a language that is not in NP but is still in PSpace) might be something close to a coNP$\neq$NP and therefore also P$\neq$NP proof (because P is closed under complement), or resolve some other "nearby" currently open complexity class separation.

[1] Decidable restrictions of the Post Correspondence Problem

[2] A polynomial reduction from any NP-complete problem to bounded PCP

a variation of Posts Correspondence Problem for bounded length input (but not the standard "bounded" version eg in Garey/Johnson that is called "bounded PCP" that limits the number of blocks in the solution to the cardinality of the block set) is complete for NEXPSpace and therefore larger than NP which is properly in Pspace. [1]

ie let there also be an input parameter $n$ specified in binary that determines the maximal length of the PCP answer. this is apparently complete for NEXPSpace via a straightfwd proof. havent seen a proof in the literature. it proceeds in a way similar to the construction relating it to TMs in [2]

note that all problems that are known to be larger than NP are also larger than PSpace. otherwise it (a proof of a language that is not in NP but is still in PSpace) might be something close to a coNP$\neq$NP and therefore also P$\neq$NP proof.

[1] Decidable restrictions of the Post Correspondence Problem

[2] A polynomial reduction from any NP-complete problem to bounded PCP

a variation of Posts Correspondence Problem for bounded length input (but not the standard "bounded" version eg in Garey/Johnson that is called "bounded PCP" that limits the number of blocks in the solution to the cardinality of the block set) is complete for NEXPSpace and therefore larger than NP which is properly in Pspace. [1]

ie let there also be an input parameter $n$ specified in binary that determines the maximal length of the PCP answer. this is apparently complete for NEXPSpace via a straightfwd proof. havent seen a proof in the literature. it proceeds in a way similar to the construction relating it to TMs in [2]

note that all problems that are known to be larger than NP are also larger than PSpace. otherwise it (a proof of a language that is not in NP but is still in PSpace) might be something close to a coNP$\neq$NP and therefore also P$\neq$NP proof (because P is closed under complement), or resolve some other "nearby" currently open complexity class separation.

[1] Decidable restrictions of the Post Correspondence Problem

[2] A polynomial reduction from any NP-complete problem to bounded PCP