--------------------------------------------------------- A Gentzen-style monadic translation of Gödel's System T --------------------------------------------------------- Chuangjie Xu, August 2019 Updated in February 2020 We introduce a syntactic translation of Gödel’s System T parametrized by a weak notion of a monad, and prove a corresponding fundamental theorem of logical relation. Our translation structurally corresponds to Gentzen’s negative translation of classical logic. By instantiating the monad and the base case of the logical relation, we reveal various properties and structures of T-definable functionals such as majorizability, continuity and bar recursion. This Agda development is organized as follow: 1. Gödel's system T (extended with products) 2. A Gentzen-style monadic translation of System T 3. Fundamental theorem of logical relation 4. Examples of nuclei and their applications 5. Other monadic translations of System T The source files are available at https://github.com/cj-xu/GentzenTrans All the files are tested in the safe mode of Agda version 2.6.1. \begin{code} {-# OPTIONS --safe #-} \end{code} ■ Gödel's system T we work with the lambda-calculus version of System T. \begin{code} import T import TAuxiliaries \end{code} ■ A Gentzen-style monadic translation We define a syntactic translation of T into itself, parametrized by a nucleus (Jι, η, κ) which is given as module parameters. \begin{code} import GentzenTranslation \end{code} ■ Fundamental theorem of logical relation We show that every term is related to its translation w.r.t. the logical relation extending a given relation on natural numbers. \begin{code} import LogicalRelation \end{code} ■ Example I: majorizability The translation of any term t of T majorizes t itself. \begin{code} import Majorizability \end{code} ■ Example II: lifting to higher-order functionals We lift natural numbers to functions of type X → ℕ for type X of T. This allows us to apply the usual syntactic method to prove properties of functions of type X → ℕ. \begin{code} import Lifting \end{code} ■ Example III: pointwise continuity Given a term f : ℕᴺ → ℕ in T, we obtain a term M : ℕᴺ → ℕ which is a modulus of continuity of f from the translation of f. \begin{code} import Continuity \end{code} ■ Example IV: uniform continuity Given a term f : ℕᴺ → ℕ in T, we obtain from the translation of f a function M : ℕᴺ → ℕ such that, for any θ : ℕᴺ, M(θ) is a modulus of uniform continuity of f restricted to inputs pointwise bounded by θ. \begin{code} import UniformContinuity \end{code} ■ Example V: bar recursion Given Y : ℕᴺ → ℕ in T, we obtain a general-bar-recursion functional form the translation of Y. \begin{code} import BarRecursion \end{code} ■ Other monadic translations We implement another two monadic translations, corresponding to the negative translations due to Kuroda and Kolmogorov. \begin{code} import KurodaTranslation import KolmogorovTranslation \end{code}