On the Various Translations between Classical, Intuitionistic and Linear Logic

Abstract

Several different proof translations exist between classical and intuitionistic logic (negative translations), and intuitionistic and linear logic (Girard translations). Our aims in this paper are (1) to consider extensions of intuitionistic linear logic which correspond to each of these systems, and (2) with this common logical basis, to develop a uniform approach to devising and simplifying proof translations. As we shall see, through this process of ``simplification'' we obtain most of the well-known translations in the literature.