In the positive setting a restriction of a Paris-Wilkie (PW) style translation yields quasipolynomial-size monotone propositional proofs from Π01 arithmetic theorems, as expected. We further show that, when only polynomial induction is used, quasipolynomial-size normal deep inference proofs may be obtained, via a graph-rewriting normalisation procedure from earlier work.
For the intuitionistic setting we calibrate the PW translation with the Brouwer-Heyting-Kolmogorov interpretation of intuitionistic implication to recover a transformation to monotone proofs. By restricting type level we are able to identify an intuitionistic theory, I1U12 , for which the transformation yields quasipolynomial-size monotone proofs. Conversely, we show that I1U12 is powerful enough to prove the soundness of monotone proofs, thereby establishing a full correspondence.