On the Various Translations between Classical, Intuitionistic and Linear Logic

TL;DR

This paper explores extensions of intuitionistic linear logic to unify various proof translations between classical, intuitionistic, and linear logic, simplifying and systematizing their derivations.

Contribution

It introduces extended intuitionistic linear logic systems to create a unified framework for deriving and simplifying proof translations.

Findings

Most known translations are derived through the proposed simplification process

A uniform approach to proof translations is developed

Extensions of intuitionistic linear logic correspond to classical and intuitionistic systems

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.