From positive and intuitionistic bounded arithmetic to monotone proof complexity

Research output: Chapter in Book/Report/Conference proceedingConference contribution

1 Citation (Scopus)
103 Downloads (Pure)

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.
Original languageEnglish
Title of host publicationLICS '16 Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science
PublisherAssociation for Computing Machinery (ACM)
Pages126-135
ISBN (Print)9781450343916
DOIs
Publication statusPublished - 5 Jul 2016
Event31st Annual ACM/IEEE Symposium on Logic in Computer Science (LICS '16) - New York, United States
Duration: 5 Jul 20168 Jul 2016

Conference

Conference31st Annual ACM/IEEE Symposium on Logic in Computer Science (LICS '16)
Country/TerritoryUnited States
CityNew York
Period5/07/168/07/16

Fingerprint

Dive into the research topics of 'From positive and intuitionistic bounded arithmetic to monotone proof complexity'. Together they form a unique fingerprint.

Cite this