On Various Translations Between Classical, Intuitionistic, and Linear Logic

Ferreira, G., Oliva, P. & Protin, C.L. On Various Translations Between Classical, Intuitionistic, and Linear Logic. Stud Logica (2026). https://doi.org/10.1007/s11225-026-10251-y

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 corresponding to each of these systems, and (2) using this common logical basis, to develop a uniform approach to devising and simplifying proof translations. Through this process of “simplification” we recover most of the well-known translations in the literature.

Foundationalism and Logic

The point in question concerns the problems of foundationalism involving type theory or term-rewriting systems. In the final part of my Kantian-oriented paper "Analyticity, Computability and the A Priori" I attempt to tackle with this problem (as well as presenting in greater detail my analysis of term-rewriting systems, Turing completeness, the Curry-Howard correspondence and the limits of logic-like formal systems in representing all computable functions and extracts on Hilbert's philosophy taken from a paper by Claire Ortiz Hill). I propose in the end a methodology inspired Piaget's genetic epistemology in which one must effect a sort of regression to relive in a conscious way the stages since early childhood whereby one progressively gained computational competency - centered around the ability to understand, carry out and check the following of rules - and to compare the cognitive structures involved to formal systems and computational models at our disposal. While this cannot lead to the enthroning of any single formal system or model it can, I believe, nevertheless bring to light groups of specific systems and models which are "structurally akin" and "cognitively natural" to consciousness itself. While we cannot enthrone a single system, I believe we can use the language of a given system to express what are in the Kantian terms synthetic a priori principles of the human understanding. For instance when we find a finite derivation in one formal system (the metasystem) and conclude that this derivation "shows" that a certain goal cannot be derived in another system (the object system), which is something that we cannot directly show in the object system because it would require an infinite amount of time. Gödel's incompleteness theorem is (and has to be) formalizable and corresponds to a finite derivation in a system M. But it must be assumed that this finite derivation is sufficient epistemic grounds to conclude something about the infinite set of derivations in Peano Arithmetic, that the sentence G cannot be derived.