A Gentzen-style monadic translation of Gödel's System T

2019/08/16 by Chuangjie Xu, Xu, Chuangjie · 1 citation
Computer Science · #F.4.1 #FOS: Computer and information sciences #FOS: Mathematics #Formal Methods in Verification #Logic (math.LO) #Logic in Computer Science (cs.LO) #Logic, Reasoning, and Knowledge #Logic, programming, and type systems #Programming Languages (cs.PL)

paper · pdf · doi:10.48550/arxiv.1908.05979

openalex publication_date 2019/08/16 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28

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.

Citations

• On Affine Logic and Łukasiewicz Logic

Cited by

• Internal Effectful Forcing in System T

Related

• From translations to non-collapsing logic combinations
• Monadic Intuitionistic and Modal Logics Admitting Provability Interpretations
• The Craig Interpolation Property in First-order Gödel Logic
• Some abstract versions of Gödel's second incompleteness theorem based on non-classical logics
• Relational Semantics for the Turing Schmerl Calculus