A Gentzen-style monadic translation of G\"odel's System T

arXiv1908.05979MaRDI QIDQ6323766FDOQ6323766

Publication date: 16 August 2019

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.

This page was built for publication: A Gentzen-style monadic translation of G\"odel's System T

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6323766)