Abstract When restricted to proving formulas, the quantified propositional proof system is closely related to the theorems of Buss's theory . Namely, has polynomial-size proofs of the translations of theorems of , and proves that is sound. However, little is known about when proving more complex formulas. In this paper, we prove a witnessing theorem for similar in style to the KPT witnessing theorem for . This witnessing theorem is then used to show that proves is sound with respect to formulas. Note that unless the polynomial-time hierarchy collapses is the weakest theory in the S2 hierarchy for which this is true. The witnessing theorem is also used to show that is p-equivalent to a quantified version of extended-Frege for prenex formulas. This is followed by a proof that Gi, p-simulates with respect to all quantified propositional formulas. We finish by proving that S2 can be axiomatized by plus axioms stating that the cut-free version of is sound. All together this shows that the connection between and does not extend to more complex formulas.

We investigate the problem of designing pairs (p,s) of words with the property that, if each word of a coded message is prefixed by p and suffixed by s, the resulting set of coded messages is error detecting with finite delay. We consider (combinatorial) channels permitting any combination of the substitution, insertion, and deletion (SID) error types, and address the cases of both scattered and burst errors. A pair (p,s) with the above property is evaluated in terms of three parameters: redundancy, delay of decoding, and frequency of the detectable errors. In the case of SID channels with burst errors, we provide a complete and explicit characterization of their error-detecting pairs (p,s), which involves the period of the word sp.