Complement duality from Sigma-2-P to Pi-2-P
ProvedSipserGacsLautemann.sigma_two_complement_to_pi_twocomplexity-theorytheoretical-computer-science
Let L be a language over bit strings. If the complement of L has a polynomial-time existential-universal verifier, then L has a polynomial-time universal-existential verifier; equivalently, Lᶜ ∈ Σ₂ᴾ implies L ∈ Π₂ᴾ.
This theorem isolates the complement-duality step in the standard proof that BPP lies in the second level of the polynomial hierarchy. In the present formalization, it requires translating the concrete verifier for the complement into a verifier for the original language while exchanging acceptance with rejection and reversing the two bounded quantifiers.
Preamble
import Definitions.Def_sipser_gacs_lautemann
Formal statement
namespace SipserGacsLautemann
theorem sigma_two_complement_to_pi_two (language : Language) :
InSigmaTwoP languageᶜ → InPiTwoP language := by sorry
end SipserGacsLautemannSource
James Aspnes, Notes on Computational Complexity Theory (2017), Section 12.3, page 92, Theorem 12.3.1, https://www.cs.yale.edu/homes/aspnes/classes/468/notes-2017.pdf