Proposition 23    Let Σ be a formula from PROPps and let L be a subset of Lps. In the general case, there is no propositional formula Φ equivalent to ForgetLit(Σ, L) s.t. the size of Φ is polynomially bounded in |Σ| + | L |, unless NP ∩ coNP ⊆ P/poly.

Proof: The justification is twofold:
(1) ForgetLit(E,L) is the logically strongest consequence of E that is Lit-independent from L . Consequently, for every formula γ ∈ PROP P S ; we have Σ |= γ if and only if ForgetLit(Σ, L) |= γ, where L = Lit(Σ)\ Lit(γ). Because ForgetLit(Σ, L) depends only on literals of Lit (Σ) ∩ Lit (γ), it is an interpolant of Σ and γ, i.e., a formula ϕ s.t. Σ |= ϕ and ϕ |= γ hold; thus we have Σ |= ForgetLit(Σ, Lit(Σ) \ Lit(γ)) |= γ
(2) the existence of a propositional formula, interpolant of Σ and γ, and of size polynomially bounded in [ Σ ] + [ γ ] would imply that NP N coNP ⊆ P/poly (Boppana & Sipser, 1990),
which is considered very unlikely in complexity theory. Proposition 24   LIT-EQUIVALENCE and VAR-EQUIVALENCE are Π 2 -complete.

## Proof:

- Var-equivalence

Membership: In order to check the membership to the complementary problem, guessing a clause γ built up from V , and checking that ( Σ |= γ and Φ | ≠ γ ) or
( Σ 
in polynomial time when an NP oracle is available. Hence, the complementary problem belongs to Σ 2 .

Hardness: Let M be the mapping that associates the triple (Σ, true, Α) to the quantified boolean formula VABBE (where {A,B} is a partition of Var(Z)).

Clearly enough, M is polytime. Moreover, we have:
AA3B∑ is valid   if and only if   |= 3B  . Σ
if and only if   |= ForgetVar(Σ, B) if and only if  ∑ ≡ A true Since the validity problem for 2-QBF formulas is Π 2 -complete, this proves the Π 2 -hardness of VAR-EQUIVALENCE.

- Lit-equivalence.

- Membership: See the membership proof above, replacing "built up from V" by

"s.t. Lit(γ) ⊆ L"
- Hardness: Let M be the mapping that associates ( Σ, Φ, V) to ( Σ, Φ, L V). Clearly enough, M((Σ, Φ, V) can be computed in time polynomial in ((Σ, Φ, V)|. We have shown that Σ and Φ are Var-equivalent given V if and only if Σ and Φ are