A Hierarchy of Determinative Sequent Systems with Different Substitution Rules

A determinative sequent system DS for the classical propositional calculus is introduced on the base of well-known Tseitin’s transformation. It is proved that the system DS is polynomially equivalent to the propositional resolution system R and propositional cut-free sequent system PK^–. Then we define the system SDS (DS with a substitution rule) and the systems S_kDS (DS with restricted substitution rules, where the number of connectives in substituted formulas is bounded by k). It is proved that for every k ≥ 0 the system S_k+1DS has an exponential speed-up over the system S_kDS in the tree form, and the system SDS is polynomially equivalent to the Frege systems.