An intuitionistic logic that proves Markov's principle

Hugo Herbelin (1, 2)

1 PPS - Preuves, Programmes et Systèmes
2 PI.R2 - Design, study and implementation of languages for proofs and programs

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.

Mots clés: Markov's principle; intuitionistic logic; proof-as-program correspondence; exceptions

Domaines: Logique en informatique [cs.LO]; Logique [math.LO]

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