Relative strength of propositional calculi

Cook and Rechkow (1974/1979) looked at the question of whether or not there exists a sound propositional calculus with an adequate set of connectives such that tautologies have polynomial length derivations, i.e., such that there is a polynomial p(x) with the property that every tautology has a derivation for which the total number of occurrences of symbols in is no more than , being the length of the string . Such a is said to be polynomially bounded. (If a polynomially bounded propositional calculus exists then TAUT is in NP, and hence NP = co-NP.) In an effort to study the above question they introduced the notion of p-simulation (polynomial time simulation). A propositional calculus p-simulates another propositional calculus if there is a polynomial time translation from formulas of to formulas of and a polynomial time algorithm to convert derivations in into derivations of the translates in . If and p-simulate each other then we say they are p-equivalent. Cook and Rechkow focused on variations of well-known propositional calculi and arrived at the following relative strength diagram (where `arrow' as well as `is in the same box' in the diagram means `p-simulates'):

The main results are:

1. some system in a given box is polynomially bounded iff all systems in the box are polynomially bounded (for a fixed set of connectives)
2. resolution and truth tables are not polynomially bounded.

References

1

S.A. Cook and R.A. Rechkow, On the lengths of proof in the propositional calculus, Preliminary version. Proc. Sixth Annual ACM Symposium on Theory of Computing (1974), 135-148. Corrections for ``On the lengths of proofs in the propositional calculus''. SIGACT News (1974), 15-22.

2

S.A. Cook and R.A. Rechkow, The relative efficiency of propositional proof systems. J. Symbolic Logic 44 (1979), 36-50.