We formalize the construction of Paterson’s variant of the Ajtai–Koml´os–Szemer´edi sorting network of logarithmic depth in the bounded arithmetical theory VNC1 ∗ (an extension of VNC1 ), under the assumption of existence of suitable expander graphs. We derive a conditional p-simulation of the propositional sequent calculus in the monotone sequent calculus MLK.