Show description

Rj ) L χ, if χ is provable in L from the assumptions r1 , . . , rj (so the sequence is understood as a set of atomic assumptions). We recall the main lemma in [8]. Let L be a consistent substructural logic satisfying (DP). By a substructural logic one means here an axiomatic extension of FL1 (possibly in a richer language). [8] admits axiomatic and rule extensions, but it makes no difference, since for the complexity results, discussed here, a logic can be identified with its set of provable sequents.

This encoding is the same as in [10], the encoding of quantifiers is different. For any 1 ≤ k ≤ n, the formula ϕk = Qk xk . . Q1 x1 ϕ0 is encoded by αk defined as follows. If Qk = ∀, then αk = (pk ∨ p¯k )\αk−1 . If Qk = ∃, then αk = (pk \qk ∨ p¯k \qk )/(αk−1 \qk ). ) A partial valuation ek assigns truth values 0, 1 to the variables xk+1 , . . , xn . It is encoded by the sequence of variables εk = (ekk+1 , . . , ekn ) such that eki = pi if ek (xi ) = 1, eki = p¯i if ek (xi ) = 0. en is the empty valuation, and εn = .

Xn stand here for propositional (boolean) variables occurring in ϕ0 (the reverse order in the prefix is a purely technical trick, making proofs by induction more elegant). It is well-known that the validity problem for closed QBFs is PSPACE-complete. We briefly recall the proof from [8]. Fix a closed QBF ϕ, presented as above. ϕ0 = ψ1 ∨ · · · ∨ ψm , where each ψj is a finite conjunction of literals. We fix different variables p1 , . . , pn , p¯1 , . . , p¯n , q1 , . . , qn (not all qi are really needed).