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
.
