On the contrapositive of countable choice |
| |
| Authors: | Hajime Ishihara Peter Schuster |
| |
| Affiliation: | 1. School of Information Science, Japan Advanced Institute of Science and Technology, 1-1 Asahidai, Nomi, Ishikawa, 923-1292, Japan
2. Department of Pure Mathematics, University of Leeds, Leeds, LS2 9JT, UK
|
| |
| Abstract: | We show that in elementary analysis (EL) the contrapositive of countable choice is equivalent to double negation elimination for ${Sigma_{2}^{0}}$ -formulas. By also proving a recursive adaptation of this equivalence in Heyting arithmetic (HA), we give an instance of the conservativity of EL over HA with respect to recursive functions and predicates. As a complement, we prove in HA enriched with the (extended) Church thesis that every decidable predicate is recursive. |
| |
| Keywords: | |
| 本文献已被 SpringerLink 等数据库收录！ |
|
