A Gentzen-style monadic translation of G\"odel's System T
Logic in Computer Science
2020-05-06 v2 Programming Languages
Logic
Abstract
We introduce a syntactic translation of Goedel'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 logical relation, we reveal the well-known properties and structures of T-definable functionals including majorizability, continuity and bar recursion. Our development has been formalized in the Agda proof assistant.
Keywords
Cite
@article{arxiv.1908.05979,
title = {A Gentzen-style monadic translation of G\"odel's System T},
author = {Chuangjie Xu},
journal= {arXiv preprint arXiv:1908.05979},
year = {2020}
}
Comments
17 pages. Changes: (1) remove the restriction of satisfying the monad laws in the definition of nuclei, (2) add a unified theorem of logical relation. This paper will appear in FSCD 2020