User loginNavigation 
An intuitionistic logic that proves Markov's principleâ€œAn intuitionistic logic that proves Markov's principleâ€, Hugo Herbelin, LICS 2010.
Markov's principle is an axiom of "Russian constructivism". It says that if P is a decidable predicate (i.e., the formula ∀x. P(x) or ¬P(x) is constructively provable), then if we know that P is not always false (ie ¬(∀x. ¬P(x))), then there exists an x such that P holds (ie ∃x. P(x)). One operational way of understanding this axiom is that it says is that if we know P is not always false (on, say, the natural numbers), we can find an element for which it is true with a whileloop: check to see if 1 is true, and then check to see if 2 is true, and so on, stopping when you hit a number for which it holds. This means that Markov's principle is a principle of unbounded search, and as a result it has controversial status in intuitionistic mathematics  should we regard a program with a nonconstructive termination proof as a constructively terminating program? (The answer is, as usual, "it depends": in different applications you can want it or not.) However, just chucking an axiom like ¬(∀x. ¬P(x)) → ∃x. P(x) into your proof rules is not very nice from a prooftheoretic perspective. It mixes up a bunch of different logical connectives, and adding it as an axiom will break things like the cutelimination theorem for sequent calculus. In this paper, Herbelin exploits (a) the fact that Markov's principle is a (mildly) classical principle of reasoning, and (b) the fact that classical logic is connected with control operators like continuations, to give a logic which is prooftheoretically wellbehaved, but which supports Markov's principle. The trick is to add firstclass continuations, but only for value types (ie, you can throw products and sums, but not functions). What I find surprising is that this same class of restriction also arises in another paper on control operators at LICS  Noam Zeilberger's paper "Polarity and the Logic of Delimited Continuations" uses it too. (This paper deserves a post here too.) 
Browse archives
Active forum topics

Recent comments
19 weeks 5 days ago
24 weeks 18 hours ago
25 weeks 4 days ago
25 weeks 4 days ago
28 weeks 2 days ago
33 weeks 4 hours ago
33 weeks 5 hours ago
33 weeks 3 days ago
33 weeks 3 days ago
36 weeks 1 day ago