Provably recursive functions of constructiveand relatively constructive theories

摘要

In this paper we prove conservation theorems for theories of classicalfirst-order arithmetic over their intuitionistic version. We also prove generalized con-servation results for intuitionistic theories when certain weak forms of the principleof excluded middle are added to them. Members of two families of subsystems ofHeyting arithmetic and Buss-Harnik's theories of intuitionistic bounded arithmetic arethe intuitionistic theories we consider. For the first group, we use a method describedby Leivant based on the negative translation combined with a variant of Friedman'stranslation. For the second group, we use Avigad's forcing method