On the Various Translations between Classical, Intuitionistic and Linear Logic
Logic
2025-11-11 v3
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.
Keywords
Cite
@article{arxiv.2409.02249,
title = {On the Various Translations between Classical, Intuitionistic and Linear Logic},
author = {Gilda Ferreira and Paulo Oliva and Clarence Lewis Protin},
journal= {arXiv preprint arXiv:2409.02249},
year = {2025}
}