Pith. sign in

REVIEW 3 major objections 3 minor 27 references

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

T0 review · 3 major / 3 minor · reviewed 2026-08-14 · deepseek-v4-flash

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗ Review JSON

Pith's one-line read One translation yields continuity, majorizability, and bar recursion

desk verdict A genuinely unifying monadic-translation framework for System T; the continuity theorems rest on an omitted proof of condition (†) that the author defers to the reader, so the paper needs one revision pass to be self-contained. read the letter →

arxiv 1908.05979 v2 pith:V54KEF2K submitted 2019-08-16 cs.LO cs.PLmath.LO

Chuangjie Xu This is my paper · ORCID
classification cs.LOcs.PLmath.LO MSC 03B4003F10
keywords monadictranslationGödel'sSystemTlogicalrelationnegativemajorizabilitycontinuitybarrecursionAgda
verification ladder T0 review T1 audit T2 compute T3 formal

The pith

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The reading

The paper sets out a single mechanical translation of Gödel's System T into itself, controlled by a monad-like structure called a nucleus: a type $J\mathbb{N}$ and two System T terms $\eta$ and $\kappa$. For any nucleus whose base logical relation satisfies two conditions labelled (†), every closed term is related to its translation; that is the fundamental theorem of logical relation (Theorem 3). Choosing different nuclei turns the same theorem into the classical majorizability theorem, moduli of pointwise and uniform continuity for every T-definable functional $\mathbb{N}^{\mathbb{N}}\to\mathbb{N}$, and the construction of general bar recursion. The translation is the term-level analogue of Gentzen's negative translation, with the nucleus playing the role of double negation.

What carries the argument

The carrier of the argument is the nucleus: a pair of System T terms $\eta:\mathbb{N}\to J\mathbb{N}$ and $\kappa:(\mathbb{N}\to J\mathbb{N})\to J\mathbb{N}\to J\mathbb{N}$ attached to a type $J\mathbb{N}$, with no requirement that the monad laws hold. The paper extends $\kappa$ to higher types via $ke_\sigma$, which is what makes the translation of the recursor type-correct. The logical relation $R_\rho$, defined by lifting a base relation $R_\mathbb{N}$ across function types, is the instrument that connects syntax to semantics: condition (†) is exactly the statement that $\eta$ and $\kappa$ are related, and the fundamental theorem propagates relatedness from constants to all closed terms.

What would settle it

Formalize the omitted (†) checks for the nuclei of Sections 3.3.2 and 3.3.3; if either condition fails, the corresponding theorem (7 or 10) has no proof. A direct operational test: take a closed term $f:\mathbb{N}^{\mathbb{N}}\to\mathbb{N}$ with a known modulus (for example the constant zero functional), compute $M_{f^J}(\Omega)$ from the translation, and check whether it is actually a modulus of continuity; a wrong answer would refute the construction.

Watch

Extended reading notes

Core claim

On the paper's own formulation, the central contribution is the $J$-translation together with its soundness theorem. Given a nucleus $(J\mathbb{N},\eta,\kappa)$, the translation sends the base type to $J\mathbb{N}$, keeps function types as function types, and translates the recursor by extending $\kappa$ to a family $ke_\sigma : (\mathbb{N}\to\sigma^J)\to J\mathbb{N}\to\sigma^J$ defined inductively on $\sigma$. Theorem 3 states that if a binary relation $R_\mathbb{N}\subseteq \mathbb{N}\times J\mathbb{N}$ satisfies (†)—every $n$ is related to $\eta n$, and $\kappa$ preserves pointwise related sequences—then every closed term $t$ satisfies $t\,R\,t^J$. The applications are instantiations: a running-maximum $\kappa$ on $\mathbb{N}$ recovers majorizability; the value-plus-modulus nucleus $J\mathbb{N}=(\mathbb{N}^{\mathbb{N}}\to\mathbb{N})\times(\mathbb{N}^{\mathbb{N}}\to\mathbb{N})$ gives pointwise continuity moduli (Theorem 7); the same structure with the uniform-continuity machinery of Lemma 9 gives uniform moduli (Theorem 10); and a triple value/securing-predicate/bar-recursion nucleus gives general bar recursion (Theorem 11). For the two continuity nuclei the proof of (†) is left to the reader.

Load-bearing premise

The load-bearing premise is that the two technical conditions (†) for the pointwise- and uniform-continuity nuclei really hold; the text says the proof is left to the reader, so Theorems 7 and 10 rest on a check the paper does not display.

Editorial extensions

If this is right

  • Every closed term of System T is majorized by its own translation under the running-maximum nucleus, so the classical majorizability theorem is a direct corollary of Theorem 3.
  • Every T-definable functional $\mathbb{N}^{\mathbb{N}}\to\mathbb{N}$ has a modulus of pointwise continuity that is itself a closed System T term, namely $M_{f^J}(\Omega)$ from Theorem 7.
  • Every T-definable functional $\mathbb{N}^{\mathbb{N}}\to\mathbb{N}$ has a modulus of uniform continuity on each compact set $\{\alpha : \alpha\le_1\delta\}$, computed by the same scheme (Theorem 10).
  • Every closed term $Y:\mathbb{N}^{\mathbb{N}}\to\mathbb{N}$ admits a monotone predicate that secures it and a functional of general bar recursion for that predicate; together with the reduction from general to Spector bar recursion proved in [17], this yields the bar-recursion closure theorem for types 0 and 1.
  • The translation is call-by-name, so its computed moduli can be smaller than those of call-by-value monadic translations; the paper's constant-functional example gives modulus $0$ rather than $1$.

Reading between the lines

Editorial extensions of the paper, not claims the author makes directly.

  • The same scheme should extend, as the paper sketches, to sums by translating $\sigma+\tau$ to $J(\sigma^J+\tau^J)$; the missing piece is a fundamental theorem covering that clause, which the paper names as future work.
  • Because the majorizability nucleus deliberately violates the monad laws, the framework does not need monadic coherence; other non-monadic structures beyond the three examples could be plugged in as nuclei to extract further T-definable witnesses.
  • The unproved (†) checks in the continuity sections are the natural place to look first: a formal proof or a counterexample for those two nuclei would either complete Theorems 7 and 10 or bound the framework's reach.
  • The paper's call-by-name moduli can be smaller than call-by-value ones, so a systematic comparison of extracted witnesses across the three negative-translation variants it discusses could be practical guidance for proof mining.
Share X Bluesky LinkedIn Reddit HN

Signed reviews

No signed human review yet.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, and a circularity audit.

Referee Report

3 major / 3 minor

Summary. The paper introduces a syntactic translation of Gödel's System T into itself, parameterized by a weak monad-like structure called a nucleus (JN, η, κ). It proves a fundamental theorem of logical relations (Theorem 3) stating that, when the base relation satisfies condition (†), every closed System T term is related to its J-translation. The framework is then instantiated with four nuclei: the majorizability nucleus (Section 3.1), a lifting nucleus (Section 3.2), continuity nuclei (Sections 3.3.2 and 3.3.3), and a general bar recursion nucleus (Section 3.4), yielding Theorems 7, 10, and 11. The paper also sketches generalizations to sums and compares the translation with Kolmogorov- and Kuroda-style monadic translations. The main proof is standard, and the author states that the development is formalized in Agda.

Significance. If the missing verification of condition (†) for the continuity nuclei is supplied, the paper provides an elegant and genuinely unifying account of several well-known properties of T-definable functionals: majorizability, pointwise and uniform continuity, and general bar recursion all arise as instantiations of the same fundamental theorem. The majorizability and bar recursion applications are self-contained in the text, and the availability of an Agda formalization is a real strength. However, the two continuity theorems are not self-contained as written: their correctness depends on an unproved condition, which weakens the paper's central claim of deriving these results in a single framework.

major comments (3)
  1. [§3.3.2] The proof of condition (†) for the pointwise continuity nucleus is omitted: immediately after defining R^α_N, the paper states "We leave the proof of (†) to the reader," yet Theorem 7 is obtained by instantiating Theorem 3, so its correctness depends entirely on this condition. The κ case of (†) requires a genuine argument: given f n R^α_N g n for all n, one must show that λβ. V_{g(Vw(β))}(β) has modulus of continuity max(M_{g(Vw(α))}(α), Mw(α)) at α, composing the modulus of w at α with the modulus of g(Vw(α)) at α. This is routine but not immediate; the text should include the proof or give a precise pointer to the corresponding lemma in the Agda development.
  2. [§3.3.3] The same omitted condition (†) occurs for the uniform continuity nucleus, and here the missing argument is more substantial. After defining R^δ_N, the paper again says "We leave the proof of (†) to the reader," and Theorem 10 depends on it. The κ case requires proving that M_{κ(g,w)}(δ) = max(Φ(λi. M_{g(i)}(δ), Θ(Mw(δ), Vw, δ)), Mw(δ)) is a modulus of uniform continuity of V_{κ(g,w)} on {α | α ≤₁ δ}. This involves using Lemma 9's Θ to bound the index Vw(α) by Θ(Mw(δ), Vw, δ), then showing that agreement up to the Φ-computed maximum suffices to compare V_{g(i)}(α) and V_{g(i)}(β). The text gives no proof of this composition argument, so Theorem 10 is not self-contained.
  3. [Supplement Material / Agda link] The introduction and abstract state that all results are formalized in Agda, but for the two continuity applications no module names, lemma names, or file locations are given for the proofs of (†). A reader who wants to check the omitted condition must search the entire repository. If the formalization indeed contains these proofs, the paper should cite them concretely; if it does not, the statement "all the results in the paper are formalized" is an overclaim. In either case, the printed proofs of the two (†) conditions should be included or precisely located.
minor comments (3)
  1. [§3.3.3] There is a typo: "The ieda is exactly the same" should read "The idea is exactly the same."
  2. [§3.3.3] In the definition of κ, the notation Mgi(δ) is ambiguous; writing M_{g(i)}(δ) would make the typing of g : N → JN explicit.
  3. [§3.3] The extension of System T with products is introduced in Section 3.3.1, but the reader is not told whether the Agda formalization works with the product extension or with the sequence-based encoding mentioned there; a short remark would clarify the relationship between the paper's presentation and the formalization.

Circularity Check

0 steps flagged · score 1.0 of 10

No significant circularity: the logical-relations derivation is self-contained, though two continuity theorems rest on an unproved (†) condition left to the reader.

full rationale

The paper's central derivation is not circular. Theorem 3 is a standard fundamental theorem of logical relations: for any nucleus (JN, η, κ), if the base relation satisfies condition (†), then every closed System T term is related to its J-translation; the proof is a structural induction and is given in the text. The applications then instantiate the theorem by choosing explicit nuclei and logical relations. For majorizability and bar recursion, the paper verifies (†) directly (Corollary 6 and the proof of Theorem 11). For pointwise and uniform continuity, Sections 3.3.2 and 3.3.3 define the nucleus and the relation and state 'We leave the proof of (†) to the reader' before deriving Theorems 7 and 10. This is a genuine omission: the soundness of those two theorems depends on an unstated preservation property of η and κ. But it is not circularity, because (†) is a local condition about the chosen nucleus, not the target theorem, and the paper does not assume the conclusion it is trying to prove. The self-citation to the author's prior work [27] is contextual and motivational, and the bar-recursion construction is explicitly described as a restructuring of Oliva and Steila [17]; those are not load-bearing self-citations in the derivation. No target result is used as an input, and no fitted parameter is renamed as a prediction. The framework therefore has no circular step, only an incompleteness in the written exposition of two applications.

Assumptions & free parameters 0 free parameters · 1 assumptions · 0 invented entities

No free parameters are fitted to data; the nuclei are chosen constructs, not fitted values. The central theorem is conditional on the logical-relation condition (†). The paper supplies incomplete proofs for the continuity instances, making the unproved (†) conditions a load-bearing assumption for those applications. No new physical or mathematical entities are invented; the nucleus is a structure within System T.

assumptions (1)
  • ad hoc to paper The logical relation condition (†) holds for the pointwise and uniform continuity nuclei defined in Sections 3.3.2 and 3.3.3.
    The paper explicitly leaves the proof of (†) to the reader in both sections. Theorems 7 and 10 rely on this condition. The companion Agda development is claimed to verify it, but the paper itself does not provide the derivation.

how reviews work

0 comments
Cite this review

Pith. "Pith review of A Gentzen-style monadic translation of G\"odel's System T." pith.science (2026). https://pith.science/paper/V54KEF2K

@misc{pith2026190805979,
  author       = {Pith},
  title        = {Pith review of: A Gentzen-style monadic translation of G\"odel's System T},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/V54KEF2K}},
  note         = {Machine review of arXiv:1908.05979}
}
read the original 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.

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

27 extracted references · 19 canonical work pages

  1. [1]

    The R ussell-- P rawitz modality

    Peter Aczel. The R ussell-- P rawitz modality. Mathematical Structures in Computer Science , 11(4):541--554, 2001. http://dx.doi.org/10.1017/S0960129501003309 doi:10.1017/S0960129501003309

    work page doi:10.1017/s0960129501003309 2001

  2. [2]

    The A gda W iki

    Agda community . The A gda W iki. https://wiki.portal.chalmers.se/agda/pmwiki.php

    work page

  3. [3]

    On Affine Logic and {\L}ukasiewicz Logic

    Rob Arthan and Paulo Oliva. On affine logic and ukasiewicz logic, 2014. arXiv:1404.0570 https://arxiv.org/abs/1404.0570 [cs.LO]

    work page Pith review arXiv 2014

  4. [4]

    CPS translating inductive and coinductive types

    Gilles Barthe and Tarmo Uustalu. CPS translating inductive and coinductive types. In 2002 ACM SIGPLAN Workshop on Partial Evaluation and Semantics-Based Program Manipulation (PEPM'02) , volume 37 of SIGPLAN Notices , pages 131--142. ACM Press, New York, 2002. http://dx.doi.org/10.1145/503032.503043 doi:10.1145/503032.503043

    work page arXiv 2002

  5. [5]

    Michael J. Beeson. F oundations of C onstructive M athematics . Springer, 1985. http://dx.doi.org/10.1007/978-3-642-68952-9 doi:10.1007/978-3-642-68952-9

    doi:10.1007/978-3-642-68952-9 1985

  6. [6]

    A note on forcing and type theory

    Thierry Coquand and Guilhem Jaber. A note on forcing and type theory. Fundamenta Informaticae , 100(1-4):43--52, 2010. http://dx.doi.org/10.3233/FI-2010-262 doi:10.3233/FI-2010-262

    doi:10.3233/fi-2010-262 2010

  7. [7]

    Escard\'o

    Mart\'in H. Escard\'o. Continuity of G \"odel's system T functionals via effectful forcing. In Proceedings of the Twenty-ninth Conference on the Mathematical Foundations of Programming Semantics (MFPS'2013) , volume 298 of Electronic Notes in Theoretical Computer Science , pages 119--141. Elsevier, 2013. http://dx.doi.org/10.1016/j.entcs.2013.09.010 doi:1...

    doi:10.1016/j.entcs.2013.09.010 2013

  8. [8]

    Escard \'o and Paulo Oliva

    Mart \'i n H. Escard \'o and Paulo Oliva. The P eirce translation. Annals of Pure and Applied Logic , 163(6):681--692, 2012. http://dx.doi.org/10.1016/j.apal.2011.11.002 doi:10.1016/j.apal.2011.11.002

    work page doi:10.1016/j.apal.2011.11.002 2012

Show all 27 references
  1. [9]

    Escard \'o and Chuangjie Xu

    Mart \'i n H. Escard \'o and Chuangjie Xu. A constructive manifestation of the K leene-- K reisel continuous functionals. Annals of Pure and Applied Logic , 167(9):770--793, 2016. Fourth Workshop on Formal Topology (4WFTop). http://dx.doi.org/10.1016/j.apal.2016.04.011 doi:10....

    2016 doi

  2. [10]

    Michael P. Fourman. Notions of choice sequence. In The L .\ E .\ J .\ B rouwer C entenary S ymposium , volume 110 of Studies in Logic and the Foundations of Mathematics , pages 91--105. Elsevier, 1982. http://dx.doi.org/10.1016/S0049-237X(09)70125-9 doi:10.1016/S0049-237X(09)70125-9

    1982 doi

  3. [11]

    William A. Howard. Hereditarily majorizable functionals of finite type. In Metamathematical investigation of intuitionistic Arithmetic and Analysis , volume 344 of Lecture Notes in Mathematics , pages 454--461. Springer, Berlin, Heidelberg, 1973. http://dx.doi.org/10.1007/BFb0...

    1973 doi

  4. [12]

    A note on the G \"odel- G entzen translation

    Hajime Ishihara. A note on the G \"odel- G entzen translation. Mathematical Logic Quarterly , 46(1):135--137, 2000. http://dx.doi.org/10.1002/(SICI)1521-3870(200001)46:1<135::AID-MALQ135>3.0.CO;2-R doi:10.1002/(SICI)1521-3870(200001)46:1<135::AID-MALQ135>3.0.CO;2-R

    2000 doi

  5. [13]

    Pointwise hereditary majorization and some applications

    Ulrich Kohlenbach. Pointwise hereditary majorization and some applications. Archive for Mathematical Logic , 31(4):227--241, 1992. http://dx.doi.org/10.1007/BF01794980 doi:10.1007/BF01794980

    1992 doi

  6. [14]

    Applied Proof Theory: Proof Interpretations and their Use in Mathematics

    Ulrich Kohlenbach. Applied Proof Theory: Proof Interpretations and their Use in Mathematics . Springer Monographs in Mathematics. Springer, 2008. http://dx.doi.org/10.1007/978-3-540-77533-1 doi:10.1007/978-3-540-77533-1

    2008 doi

  7. [15]

    Unifying functional interpretations

    Paulo Oliva. Unifying functional interpretations. Notre Dame Journal of Formal Logic , 47(2):263--290, 2006. http://dx.doi.org/10.1305/ndjfl/1153858651 doi:10.1305/ndjfl/1153858651

    2006

  8. [16]

    On the relation between various negative translations

    Paulo Oliva and Gilda Ferreira. On the relation between various negative translations. In Logic, Construction, Computation , volume 3 of Mathematical Logic Series , pages 227--258. Ontos-Verlag, 2012. http://dx.doi.org/10.1515/9783110324921 doi:10.1515/9783110324921

    2012 doi

  9. [17]

    A direct proof of S chwichtenberg's bar recursion closure theorem

    Paulo Oliva and Silvia Steila. A direct proof of S chwichtenberg's bar recursion closure theorem. The Journal of Symbolic Logic , 83(1):70--83, 2018. http://dx.doi.org/10.1017/jsl.2017.33 doi:10.1017/jsl.2017.33

    2018 doi

  10. [18]

    A functional interpretation with state

    Thomas Powell. A functional interpretation with state. In Proceedings of the Thirty third Annual IEEE Symposium on Logic in Computer Science (LICS 2018) , pages 839--848. IEEE Computer Society Press, July 2018. http://dx.doi.org/10.1145/3209108.3209134 doi:10.1145/3209108.3209134

    2018

  11. [19]

    A unifying framework for continuity and complexity in higher types, 2019

    Thomas Powell. A unifying framework for continuity and complexity in higher types, 2019. arXiv:1906.10719 https://arxiv.org/abs/1906.10719 [cs.LO]

    2019 arXiv

  12. [20]

    On bar recursion of types 0 and 1

    Helmut Schwichtenberg. On bar recursion of types 0 and 1. The Journal of Symbolic Logic , 44(3):325--329, 1979. http://dx.doi.org/10.2307/2273126 doi:10.2307/2273126

    1979 doi

  13. [21]

    Logical relations and the typed lambda-calculus

    Richard Statman. Logical relations and the typed lambda-calculus. Information and Control , 65(2/3):85--97, 1985. http://dx.doi.org/10.1016/S0019-9958(85)80001-2 doi:10.1016/S0019-9958(85)80001-2

    1985 doi

  14. [22]

    Basic Proof Theory , volume 43 of Cambridge tracts in theoretical computer science

    Anne Sjerp Troelstra and Helmut Schwichtenberg. Basic Proof Theory , volume 43 of Cambridge tracts in theoretical computer science . Cambridge University Press, 2nd edition, 2000

    2000

  15. [23]

    Constructivism in mathematics, Vol.\ II , volume 123 of Studies in Logic and the Foundations of Mathematics

    Anne Sjerp Troelstra and Dirk van Dalen. Constructivism in mathematics, Vol.\ II , volume 123 of Studies in Logic and the Foundations of Mathematics . North-Holland Publishing Co., Amsterdam, 1988

    1988

  16. [24]

    Monad translating inductive and coinductive types

    Tarmo Uustalu. Monad translating inductive and coinductive types. In Types for Proofs and Programs (TYPES 2002) , volume 2646 of Lecture Notes in Computer Science , pages 299--315. Springer, 2002. http://dx.doi.org/10.1007/3-540-39185-1_17 doi:10.1007/3-540-39185-1_17

    2002 doi

  17. [25]

    A K uroda-style j-translation

    Benno van den Berg. A K uroda-style j-translation. Archive for Mathematical Logic , 58(5-6):627--634, 2019. http://dx.doi.org/10.1007/s00153-018-0656-x doi:10.1007/s00153-018-0656-x

    2019 doi

  18. [26]

    Sheaf models for choice sequences

    Gerrit van der Hoeven and Ieke Moerdijk. Sheaf models for choice sequences. Annals of Pure and Applied Logic , 27(1):63--107, 1984. http://dx.doi.org/10.1016/0168-0072(84)90035-6 doi:10.1016/0168-0072(84)90035-6

    1984 doi

  19. [27]

    A syntactic approach to continuity of T -definable functionals

    Chuangjie Xu. A syntactic approach to continuity of T -definable functionals. Logical Methods in Computer Science , 16(1):22:1--22:11, 2020. URL: https://lmcs.episciences.org/6130

    2020

Pith tools

Reviewed August 14, 2026 · model on record in the stance chip above.