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.

Statistics

Seen <100 times
0 Comments

More articles like this

F. T. Peirce.

on Nature May 27, 1950

Peirce on signs

Dec 01, 2005

The Elder Peirce's.

on Proceedings of the National Ac... July 1926
More articles like this..