## 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 |

Subtitle of host publication | Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science |

Publisher | Association for Computing Machinery (ACM) |

Pages | 126-135 |

Number of pages | 10 |

ISBN (Electronic) | 9781450343916 |

ISBN (Print) | 9781450343916 (PoD) |

DOIs | |

Publication status | Published - 5 Jul 2016 |

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

### Publication series

Name | LICS: Logic in Computer Science |
---|

### Conference

Conference | 31st Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2016 |
---|---|

Country/Territory | United States |

City | New York |

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

### Bibliographical note

Publisher Copyright:© 2016 ACM.

## ASJC Scopus subject areas

- Software
- Mathematics(all)