Symmetry of IP complexity class

Wikipedia defines the IP complexity class as follows:


A language $L$ belongs to IP if there exists $V,P$ such that for all
$Q$, $w$,
$$w\in L\Rightarrow Pr[V\leftrightarrow P\text{ accepts }w]\geq2/3$$
$$w\notin L\Rightarrow Pr[V\leftrightarrow Q\text{ accepts }w]\leq1/3$$

Note that this definition is asymmetric; it says (if we are polynomial-bound) we can be convinced $w\in L$, but says nothing about convincing us that $w\notin L$. We could define a class coIP containing the complements of languages in IP; that is


A language $L$ belongs to coIP if there exists $V,P$ such that for all
$Q$, $w$,
$$w\notin L\Rightarrow Pr[V\leftrightarrow P\text{ accepts }w]\geq2/3$$
$$w\in L\Rightarrow Pr[V\leftrightarrow Q\text{ accepts }w]\leq1/3$$

It turns out IP=PSPACE and clearly PSPACE is symmetric under taking complement. Thus IP=coIP. Is there a direct way to see this? That is,


Given a proof system $(V,P)$ for proving membership in $L$, can we use
it to construct a proof system $(V',P')$ for proving membership in
$\bar L$?

There is no relativizing technique to show that $\mathrm{IP}$ is closed under complement.

Clearly, $\mathrm{NP}\subseteq\mathrm{IP}$.

Fortnow and Sipser gave an oracle relative to which $\mathrm{co}$-$\mathrm{NP}$ does not have interactive proof system.

So, you have to study the arithmetization technique that settles down this conjecture (long ago).

Are there interactive protocols for CO-NP

StackExchange Computer Science Q#91748, answer score: 2