Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

On the Various Translations between Classical, Intuitionistic and Linear Logic

Gilda Ferreira, Paulo Oliva, Clarence Lewis Protin

TL;DR

The paper provides a unified, modular framework to study translations between classical, intuitionistic, and linear logics by grounding all of them in Intuitionistic Linear Logic ($ILL$). It introduces structured extensions ${IL}_{b}$, ${CL}_{b}$, and ${CLL}_{b}$ as targets of translations and develops a theory of modular inner/outer transforms and simplifications, showing how well-known translations (Kolmogorov, Gödel–Gentzen, Kuroda, and Girard variants) arise as systematic reductions. It demonstrates that several translations are sound and equivalent under appropriate extensions, and identifies precise outer/inner simplifications (e.g., Gödel–Gentzen from Kolmogorov ${K_o}$ and Kuroda from ${K_i}$), also extending to linear variants ${lG}$ and ${lKu}$ in the absence of promotion. The work thereby clarifies why certain translations are “canonical” within this modular framework and provides a roadmap for generating new, simpler translations by targeted reductions. The results have significance for proof theory by offering a uniform method to derive, compare, and simplify translations across the classical–intuitionistic–linear spectrum, with potential applications in automated reasoning and formal embeddings between logical 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.

On the Various Translations between Classical, Intuitionistic and Linear Logic

TL;DR

The paper provides a unified, modular framework to study translations between classical, intuitionistic, and linear logics by grounding all of them in Intuitionistic Linear Logic (). It introduces structured extensions , , and as targets of translations and develops a theory of modular inner/outer transforms and simplifications, showing how well-known translations (Kolmogorov, Gödel–Gentzen, Kuroda, and Girard variants) arise as systematic reductions. It demonstrates that several translations are sound and equivalent under appropriate extensions, and identifies precise outer/inner simplifications (e.g., Gödel–Gentzen from Kolmogorov and Kuroda from ), also extending to linear variants and in the absence of promotion. The work thereby clarifies why certain translations are “canonical” within this modular framework and provides a roadmap for generating new, simpler translations by targeted reductions. The results have significance for proof theory by offering a uniform method to derive, compare, and simplify translations across the classical–intuitionistic–linear spectrum, with potential applications in automated reasoning and formal embeddings between logical 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.
Paper Structure (23 sections, 21 theorems, 80 equations, 2 tables)

This paper contains 23 sections, 21 theorems, 80 equations, 2 tables.

Table of Contents

  1. Introduction
  2. ${\sf ILL}$ as a common base system
  3. Intuitionistic Logic ${\sf IL}$ as ${\sf ILL} + {\sf PRO}$
  4. Intuitionistic Logic ${\sf IL}$ as ${\sf ILL} + {\sf PRO}$
  5. Classical Linear Logic ${\sf CLL}$ as ${\sf ILL}_\bot + {\sf DNE}$
  6. Classical Logic ${\sf CL}$ as ${\sf ILL}_\bot + {\sf PRO} + {\sf DNE}$ (or ${\sf ILL} + {\sf PRO} + {\sf DNE}$)
  7. On some equivalences
  8. Modular Translations and Simplifications
  9. Modular translations
  10. Simplifying translations (from inside and outside)
  11. Translations from ${\sf CL}_{\rm b}$ to ${\sf IL}_\bot$
  12. Kolmogorov, Gödel-Gentzen and Kuroda translations
  13. ${(\cdot)}^{\textup{G}}$ is a simplification from outside of ${(\cdot)}^{{\textup{K}}_{o}}$
  14. ${(\cdot)}^{\textup{Ku}}$ is a simplification from inside of ${(\cdot)}^{{\textup{K}}_{i}}$
  15. Translations from ${\sf IL}_{\rm b}$ to ${\sf ILL}$
  16. ...and 8 more sections

Key Result

Lemma 1

Let ${\sf IL}_{\rm b} := {\sf ILL} + {\sf PRO}$. The following are provable in ${\sf IL}_{\rm b}$:

Theorems & Definitions (60)

  • Definition 1: Translating ${\mathcal{L}}({\sf IL})$ into ${\mathcal{L}}({\sf ILL})$
  • Lemma 1
  • proof
  • Proposition 1: ${\sf IL}$ as an extension of ${\sf ILL}$
  • proof
  • Remark 1
  • Definition 2: Translating ${\mathcal{L}}({\sf CLL})$ into ${\mathcal{L}}({\sf ILL}_\bot)$
  • Proposition 2: ${\sf CLL}$ as an extension of ${\sf ILL}_\bot$
  • proof
  • Proposition 3: ${\sf CL}$ as an extension of ${\sf ILL}$
  • ...and 50 more