Coding of real-valued continuous functions under WKL$\mathsf {WKL}$ |
| |
Authors: | Tatsuji Kawai |
| |
Institution: | Department of Information Science, Kochi University, Kochi, Japan |
| |
Abstract: | In the context of constructive reverse mathematics, we show that weak K?nig's lemma () implies that every pointwise continuous function is induced by a code in the sense of reverse mathematics. This, combined with the fact that implies the Fan theorem, shows that implies the uniform continuity theorem: every pointwise continuous function has a modulus of uniform continuity. Our results are obtained in Heyting arithmetic in all finite types with quantifier-free axiom of choice. |
| |
Keywords: | |
|
|