## Abstract

We study versions of second-order bounded arithmetic where induction and comprehension formulae are positive or where the underlying logic is intuitionistic, examining their relationships to monotone and deep inference proof systems for propositional logic.

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.

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.

Original language | English |
---|---|

Title of host publication | LICS '16 Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science |

Publisher | Association for Computing Machinery (ACM) |

Pages | 126-135 |

ISBN (Print) | 9781450343916 |

DOIs | |

Publication status | Published - 5 Jul 2016 |

Event | 31st Annual ACM/IEEE Symposium on Logic in Computer Science (LICS '16) - New York, United States Duration: 5 Jul 2016 → 8 Jul 2016 |

### Conference

Conference | 31st Annual ACM/IEEE Symposium on Logic in Computer Science (LICS '16) |
---|---|

Country/Territory | United States |

City | New York |

Period | 5/07/16 → 8/07/16 |