Affordable Access

Publisher Website

The Peirce translation

Authors
Journal
Annals of Pure and Applied Logic
0168-0072
Publisher
Elsevier
Volume
163
Issue
6
Identifiers
DOI: 10.1016/j.apal.2011.11.002
Keywords
  • The Peirce Law
  • Negative Translation
  • Countable Choice
  • Dependent Choice
Disciplines
  • Computer Science
  • Logic
  • Mathematics

Abstract

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 minimal logic plus Peirce law into minimal logic, which we refer to as Peirce translation, as it eliminates uses of Peirce law. When combined with modified realizability, this translation applies to full classical analysis, i.e. Peano arithmetic in the language of finite types extended with countable choice and dependent choice. A fundamental step in the interpretation is the realizability of a strengthening of the double-negation shift via the iterated product of selection functions. In a separate paper, we have shown that such a product of selection functions is equivalent, over system T, to modified bar recursion.

There are no comments yet on this publication. Be the first to share your thoughts.