An intuitionistic logic that proves Markov's principle

Hugo Herbelin 1, 2
2 PI.R2 - Design, study and implementation of languages for proofs and programs
PPS - Preuves, Programmes et Systèmes, Inria Paris-Rocquencourt, UPD7 - Université Paris Diderot - Paris 7, CNRS - Centre National de la Recherche Scientifique : UMR7126
Abstract : We design an intuitionistic predicate logic that supports a limited amount of classical reasoning, just enough to prove a variant of Markov's principle suited for predicate logic. At the computational level, the extraction of an existential witness out of a proof of its double negation is done by using a form of statically-bound exception mechanism, what can be seen as a direct-style variant of Friedman's A-translation.
Complete list of metadatas

Cited literature [27 references]  Display  Hide  Download
Contributor : Hugo Herbelin <>
Submitted on : Friday, May 7, 2010 - 1:35:25 PM
Last modification on : Friday, January 4, 2019 - 5:33:25 PM
Long-term archiving on : Friday, October 19, 2012 - 2:30:51 PM


Files produced by the author(s)


  • HAL Id : inria-00481815, version 1



Hugo Herbelin. An intuitionistic logic that proves Markov's principle. Logic In Computer Science, Jul 2010, Edinburgh, United Kingdom. pp.50-56. ⟨inria-00481815⟩



Record views


Files downloads