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 …