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

https://hal.inria.fr/inria-00481815
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

File

herbelin.LICS2010.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : inria-00481815, version 1

Collections

Citation

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

Share

Metrics

Record views

455

Files downloads

285