A syntactic approach to continuity of T-definable functionals
We give a new proof of the well-known fact that all functions $(\mathbb{N} \to \mathbb{N}) \to \mathbb{N}$ which are definable in G\"odel's System T are continuous via a syntactic approach. Differing from the usual syntactic method, we firstly perform a translation of System T into itself...
| Main Author: | |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
Logical Methods in Computer Science e.V.
2020-02-01
|
| Series: | Logical Methods in Computer Science |
| Subjects: | |
| Online Access: | https://lmcs.episciences.org/5394/pdf |
| _version_ | 1797268557441007616 |
|---|---|
| author | Chuangjie Xu |
| author_facet | Chuangjie Xu |
| author_sort | Chuangjie Xu |
| collection | DOAJ |
| description | We give a new proof of the well-known fact that all functions $(\mathbb{N}
\to \mathbb{N}) \to \mathbb{N}$ which are definable in G\"odel's System T are
continuous via a syntactic approach. Differing from the usual syntactic method,
we firstly perform a translation of System T into itself in which natural
numbers are translated to functions $(\mathbb{N} \to \mathbb{N}) \to
\mathbb{N}$. Then we inductively define a continuity predicate on the
translated elements and show that the translation of any term in System T
satisfies the continuity predicate. We obtain the desired result by relating
terms and their translations via a parametrized logical relation. Our
constructions and proofs have been formalized in the Agda proof assistant.
Because Agda is also a programming language, we can execute our proof to
compute moduli of continuity of T-definable functions. |
| first_indexed | 2024-04-25T01:34:22Z |
| format | Article |
| id | doaj.art-50af18b499ff4f1a9800a6182663179c |
| institution | Directory Open Access Journal |
| issn | 1860-5974 |
| language | English |
| last_indexed | 2024-04-25T01:34:22Z |
| publishDate | 2020-02-01 |
| publisher | Logical Methods in Computer Science e.V. |
| record_format | Article |
| series | Logical Methods in Computer Science |
| spelling | doaj.art-50af18b499ff4f1a9800a6182663179c2024-03-08T10:29:27ZengLogical Methods in Computer Science e.V.Logical Methods in Computer Science1860-59742020-02-01Volume 16, Issue 110.23638/LMCS-16(1:22)20205394A syntactic approach to continuity of T-definable functionalsChuangjie XuWe give a new proof of the well-known fact that all functions $(\mathbb{N} \to \mathbb{N}) \to \mathbb{N}$ which are definable in G\"odel's System T are continuous via a syntactic approach. Differing from the usual syntactic method, we firstly perform a translation of System T into itself in which natural numbers are translated to functions $(\mathbb{N} \to \mathbb{N}) \to \mathbb{N}$. Then we inductively define a continuity predicate on the translated elements and show that the translation of any term in System T satisfies the continuity predicate. We obtain the desired result by relating terms and their translations via a parametrized logical relation. Our constructions and proofs have been formalized in the Agda proof assistant. Because Agda is also a programming language, we can execute our proof to compute moduli of continuity of T-definable functions.https://lmcs.episciences.org/5394/pdfmathematics - logiccomputer science - logic in computer sciencef.4.1 |
| spellingShingle | Chuangjie Xu A syntactic approach to continuity of T-definable functionals Logical Methods in Computer Science mathematics - logic computer science - logic in computer science f.4.1 |
| title | A syntactic approach to continuity of T-definable functionals |
| title_full | A syntactic approach to continuity of T-definable functionals |
| title_fullStr | A syntactic approach to continuity of T-definable functionals |
| title_full_unstemmed | A syntactic approach to continuity of T-definable functionals |
| title_short | A syntactic approach to continuity of T-definable functionals |
| title_sort | syntactic approach to continuity of t definable functionals |
| topic | mathematics - logic computer science - logic in computer science f.4.1 |
| url | https://lmcs.episciences.org/5394/pdf |
| work_keys_str_mv | AT chuangjiexu asyntacticapproachtocontinuityoftdefinablefunctionals AT chuangjiexu syntacticapproachtocontinuityoftdefinablefunctionals |