Incorporating Markov's principle in various proof assistants

Question

The Markov's principle states that if a Turing machine does not run forever, then it halts. Equivalently, if I have a function $f : \mathbb N \to \mathrm{Bool}$, such that I have proved that $\neg\neg \exists n. f(n)=\mathrm{true}$, then I can find $\exists n. f(n)=\mathrm{true}$.

This principle is sometimes considered as constructively valid, since we can give a program that just enumerates $\mathbb N$ and searches for the solution, and if our meta-logic is classical, we can see that this program halts, which means that it is constructively true for each concrete function $f$.

What are the best practices to incorporate this principle into various proof assistants? The most naïve approach is, of course, assume it as an axiom. But I would also like to have computational properties. So for each concrete function $f$, I can do this in Agda:

f : Nat -> Bool
f = blah blah

f-good : ¬ ¬ ∃[ x ∈ Nat ] f x ≡ true
f-good = blah blah

private
  {-# TERMINATING #-}
  helper : Nat -> ∃[ x ∈ Nat ] f x ≡ true
  helper n with f n in eq
  ... | true = n , eq
  ... | false = helper (suc n)

magic : ∃[ x ∈ Nat ] f x ≡ true
magic = helper 0

I have to seal helper as private, because it indeed does not terminate on some input. But given f-good, we can be (meta-classically) sure that magic will halt.

However, this has some drawbacks:

• If the normalization strategy is wrong, then this program will not terminate. For instance, if Agda chose to first fully expand all the branches before picking one, then it will keep entering the false branch.
• If I try to state the general Markov's principle instead of on concrete $f$'s, then Agda will indeed loop in certain cases.
• I might accidentally make some unsafe leaks.

Is there any better way of doing this? Also, is there any proof assistant that actually supports this with a flag or something?

Answer 1

There are different ways to implement Markov's principle, and they're not equivalent. I know of at least three techniques to implement MP.

MP as a loop

I personally find this to be a hack inherited from untyped realizability. As you observed already, it breaks the good metatheoretical properties of your system, in particular strong normalization. It also requires some form of MP in the metatheory, which is not a blocker but not great either. I guess that if your favourite proof assistant is some variant of PRL this is not so much a problem, but if you only swear by MLTT this is not going to do the job.

MP via Dialectica

It is well-known that the Dialectica interpretation realizes MP. The underlying implementation is very different from an unbounded loop. Morally you can picture it as some form of delimited continuations triggered by the access to bound variables in the calculus. I wrote a Dialectica model of CoC in my PhD, and we have an unpublished account of a Dialectica model of MLTT with Andrej Bauer, but it's not very implementable. It relies on a structure of finite multisets that enjoy definitional equations and it is not even clear we can get a decidable type system out of it.

MP by static exceptions

The third technique is, I believe, a simplification of the Dialectica approach that is easy to explain computationally and implement. Essentially, it consists in adding a special kind of exceptions to the ambient type theory. In order to preserve consistency you have to forbid exceptions at toplevel though, and ensure that they are always statically caught.

There are two ways to understand this, either in direct style or through a program translation. These two papers only handle a weak logical system, but the technique can actually be lifted to MLTT.

The resulting theory can be described as the composition of an exceptional model with a strict presheaf model. Both processes are relatively simple compilation phases so in the end you can just compile away MLTT + MP into a reasonable variant of MLTT. The result is described in this paper.

Since the presentation is synthetic, you can actually dump the syntactic model phase altogether and simply add the corresponding combinators with the reduction rules inherited from the underlying computational model. Dynamic exceptions are fairly easy to add through rewrite rules so I guess it is only a matter of correctly implementing the static try-catch handlers.