References

In this paper, a new propositional proof system H is introduced, that allows quantification over permutations of the variables. In H the syntax of propositional logic is enriched by quantifiers (∃ab)α and (∀ab)α for variables a and b, which are intended to be semantically equivalent to α ∨ α[b/a, a/b] and α ∧ α[b/a, a/b], respectively. The paper studies the fragment of H with cuts restricted to Σ1-formulas, denoted H1. It is shown that H1 simulates efficiently the Hajós calculus (HC) for constructing graphs which are non-3-colorable. This shows that short proofs using formulas asserting the existence of permutations of the variables can capture polynomial time reasoning, as it is known [1] that HC is equivalent to Extended Frege systems (EF), which capture polynomial time reasoning. The converse direction is left open, but it is shown that at least E