The Peirce translation

DOI10.1016/J.APAL.2011.11.002zbMath1251.03068OpenAlexW2047094534MaRDI QIDQ408162

Paulo Oliva, Martín Hötzel Escardó

Publication date: 29 March 2012

Published in: Annals of Pure and Applied Logic (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.apal.2011.11.002

zbMATH Keywords

countable choiceminimal logiccomputational extraction of witnesses from proofs in classical analysisdependent choicefunctional interpretationmodified realizabilitynegative translationPeirce lawselection functions

Mathematics Subject Classification ID

Structure of proofs (03F07) Functionals in proof theory (03F10) Second- and higher-order arithmetic and fragments (03F35) Proof theory in general (including proof-theoretic semantics) (03F03)

Related Items (3)

The equivalence of bar recursion and open recursion ⋮ Smart Choices and the Selection Monad ⋮ A Kuroda-style \(j\)-translation

Cites Work

• Metamathematical investigation of intuitionistic arithmetic and analysis. With contributions by C. A. Smorynski, J. I. Zucker and W. A. Howard
• Programs from proofs using classical dependent choice
• The Russell–Prawitz modality
• Sequential games and optimal strategies
• Exhaustible sets in higher-type computation
• Selection functions, bar recursion and backward induction
• Computational Interpretations of Analysis via Products of Selection Functions
• The Peirce Translation and the Double Negation Shift
• On the computational content of the axiom of choice
• A proof of strong normalisation using domain theory
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: The Peirce translation