Premium
Polynomial induction and length minimization in intuitionistic bounded arithmetic
Author(s) -
Moniri Morteza
Publication year - 2005
Publication title -
mathematical logic quarterly
Language(s) - English
Resource type - Journals
SCImago Journal Rank - 0.473
H-Index - 28
eISSN - 1521-3870
pISSN - 0942-5616
DOI - 10.1002/malq.200410008
Subject(s) - mathematics , bounded function , constructive , polynomial hierarchy , hierarchy , polynomial , discrete mathematics , negation , scheme (mathematics) , combinatorics , algebra over a field , pure mathematics , time complexity , computer science , mathematical analysis , process (computing) , economics , market economy , programming language , operating system
It is shown that the feasibly constructive arithmetic theory IPV does not prove (double negation of) LMIN(NP), unless the polynomial hierarchy CPV‐provably collapses. It is proved that PV plus (double negation of) LMIN(NP) intuitionistically proves PIND(coNP). It is observed that PV + PIND(NP ∪ coNP) does not intuitionistically prove NPB, a scheme which states that the extended Frege systems are not polynomially bounded. (© 2004 WILEY‐VCH Verlag GmbH & Co. KGaA, Weinheim)