On two questions about feasibly constructive arithmetic
Morteza Moniri · Mathematical logic quarterly · 2003
Abstract IPV is the intuitionistic theory axiomatized by Cook's equational theory PV plus PIND on NP‐formulas. Two extensions of IPV were introduced by Buss and by Cook and Urquhart by adding PIND for formulas of the form A(x) ∨ B, respectively ¬¬A(x), where A(x) is NP and x is not free in B. Cook and Urquhart posed the question of whether these extensions are proper. We show that in each of the two cases the extension is proper unless the polynomial hierarchy collapses.