A Propositional Proof System with Quantification Over Permutations

Article type: Research Article

Authors: Herman, Grzegorz | Paterson, Tim | Soltys, Michael

Affiliations: Department of Computing and Software, McMaster University, Ontario, Canada. E-mail: {hermang,paterst,soltys}@mcmaster.ca

Abstract: We introduce a new propositional proof system, which we call H, that allows quantification over permutations. In H we may write (∃ab)α and (∀ab)α, which is semantically equivalent to α(a,b)∨α(b,a) and α(a,b)∧ α(b,a), respectively. We show that H with cuts restricted to Σ_1 formulas (we denote this system H_1) simulates efficiently the Hajós calculus (HC) for constructing graphs which are non-3-colorable. This shows that short proofs over formulas that assert the existence of permutations can capture polynomial time reasoning (as by [9], HC is equivalent in strength to EF, which in turn captures polytime reasoning). We also show that EF simulates efficiently H^*_1, which is H_1 with proofs restricted to being tree-like. In short, we show that H^*_1⩽_p EF⩽_p H_1.

Journal: Fundamenta Informaticae, vol. 79, no. 1-2, pp. 71-83, 2007