A sorting network in bounded arithmetic

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.

• Type: Journal
• Year: 2011
• Where: APAL
• Authors: Emil Jerábek
• Keywords: APAL 2011, Monotone Sequent Calculus, Propositional Sequent Calculus, Sequent Calculus, Software Engineering