The Peirce Translation and the Double Negation Shift

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.

• Type: Conference
• Year: 2010
• Where: CIE
• Authors: Martín Hötzel Escardó, Paulo Oliva
• Keywords: Applied Computing, CIE 2010, Classical Minimal Logic, Minimal Logic, Selection Functions