Abstract
We develop applications of selection functions to proof theory and computational extraction of witnesses from proofs in classical analysis. The main novelty is a translation of classical minimal logic into minimal logic, which we refer to as the Peirce translation, and which we apply to interpret both a strengthening of the double-negation shift and the axioms of countable and dependent choice, via infinite products of selection functions. © 2010 Springer-Verlag Berlin Heidelberg.
Cite
CITATION STYLE
Escardó, M., & Oliva, P. (2010). The Peirce translation and the double negation shift. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 6158 LNCS, pp. 151–161). https://doi.org/10.1007/978-3-642-13962-8_17
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
