Home > Uncategorized > An intuitionistic logic that proves Markov’s principle

An intuitionistic logic that proves Markov’s principle

July 2nd, 2010 07:36 admin Leave a comment Go to comments

“An intuitionistic logic that proves Markov’s principle”, Hugo Herbelin, LICS 2010.

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.

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 while-loop: 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 non-constructive 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 proof-theoretic perspective. It mixes up a bunch of different logical connectives, and adding it as an axiom will break things like the cut-elimination 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 proof-theoretically well-behaved, but which supports Markov’s principle. The trick is to add first-class 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.)

Source: An intuitionistic logic that proves Markov’s principle

Related Articles:

  1. Milawa: A Self-Verifying Theorem Prover for an ACL2-Like Logic
  2. Conservative Logic
  3. Imperative Programs as Proofs via Game Semantics
  4. Proof Mooted For Heisenberg’s Uncertainty Principle
  5. Researchers Create Logic Circuits From DNA
blog comments powered by Disqus