An Intuitionistic Logic that Proves Markov's Principle

—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. Keywords-Markov’s principle; intuitionistic logic; proof-asprogram correspondence; exceptions

• Type: Journal
• Year: 2010
• Where: LICS
• Authors: Hugo Herbelin
• Keywords: Automated Reasoning, Intuitionistic Logic, LICS 2010, Logic, Statically-bound Exception Mechanism