Using PSPACE-completeness of quantified boolean logic Valerii Sopin claimed to have obtained that PH = PSPACE, see https://arxiv.org/abs/1411.0628
The idea is the following:
- the quantified Boolean formula problem is equivalent to existing of boolean functions for each variable with the quantifier ∃, which make the formula to be Tautology (Skolem functions).
- size of boolean functions can be exponential, but it is considered in frames of full DNF. It allows to not construct precisely the boolean functions. Namely, iterations of ∀x∃y reduce to “long” conjunctions of separated ∀x∃y (XOR is the only issue here and it can be handled).
This way PSPASE-complete problem is solved using alternating Turing machine with only 4 alternations.
The consequences can be found in the paper.
A related point to consider is L. Gordeew, E. H. Haeusler, Proof Compression and NP Versus PSPACE, Studia Logica, 107:1, 2019, 55–83; L. Gordeew, E. H. Haeusler, Proof Compression and NP Versus PSPACE II, Bulletin of the Section of Logic , 49:3, 2020, 213–230.