A propositional proof system with quantification over permutations

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 H1*, which is H1 with proofs restricted to being tree-like. In short, we show that H1*≤p EF≤p H1.