The Peirce Translation and the Double Negation Shift

DOI10.1007/978-3-642-13962-8_17zbMath1251.03065OpenAlexW1517302412MaRDI QIDQ3576201

Paulo Oliva, Martín Hötzel Escardó

Publication date: 29 July 2010

Published in: Programs, Proofs, Processes (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-642-13962-8_17

zbMATH Keywords

countable choiceminimal logiccomputational extraction of witnesses from proofs in classical analysisdependent choicefunctional interpretationmodified realizabilitynegative translationselection functionsdouble-negation shiftPeirce translation

Mathematics Subject Classification ID

Structure of proofs (03F07) Functionals in proof theory (03F10) Proof theory in general (including proof-theoretic semantics) (03F03)

Related Items (5)

Higher-order games with dependent types ⋮ The Peirce translation ⋮ Unnamed Item ⋮ Double negation semantics for generalisations of Heyting algebras ⋮ Unnamed Item

This page was built for publication: The Peirce Translation and the Double Negation Shift