“School of Mathematics”
Back to Papers HomeBack to Papers of School of Mathematics
Paper IPM / M / 2295  


Abstract:  
IPV is the intuitionistic theory axiomatized by Cook's
equational theory PV plus PIND on NPformulas. 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.
Download TeX format 

back to top 