1
$\begingroup$

I am recently thinking about proving the undecidability of some problem. This problem has been formalized in Coq and by staring at it, people including me think "for sure" this is undecidable. "For sure" is a good source for surprises so I think I should try to prove it, probably formally.

But then I recall MLTT is compatible with LEM, and now my brain is in a loop:

To prove that theory is undecidable, I have to show that

forall x y ... z, ~({P x y ... z} + {~P x y ... z})

where x y ... z are the parameters. Namely, it's not true that we can decide the problem for all inputs.

On the other hand, LEM claims that for all P x y ... z we can obtain either witness or refutation, and its compatibility with type theory just says the falsehood is not provable. This means MLTT and others are just not able to express computability problems. Therefore, I am wondering can formal systems encode computability at all, or it's just I am mistaken? Is there anyone actually tried to formally prove undecidability in formal systems like Coq?

Even though I am using Coq, but since the compatibility is from MLTT, so I guess LEM does not have to live in Prop.

Apologies if I am being stupid for the moment but I think my brain is in a serious loop now.

| cite | improve this question | |
$\endgroup$
3
$\begingroup$

You have your quantifiers wrong. The ~ should be on the outermost level. That is:

~(forall x y z, {P x y z} + ~{P x y z})

i.e. to prove it's undecidable, you assert that there's no function which decides every instance. There may be functions which decide particular instances, which your type would rule out.

If you add LEM to MLTT, you can still have a perfectly good logic system, but provability in this logic no longer implies decidability.

Moreover, even the type I've listed above isn't sufficient: just because a problem isnt' expressible in MLTT or COC or any other non-Turing-complete logic, doesn't mean that it's undecidable.

A better approach would be model Turing Machines or (even better) a Turing Complete Lambda Calculus in your language, and assert that there are no functions in this model that always halt and answer your problem. This way, you're not trying to use your logic to reason about decidability within that logic, but an external model.

If you want an easier way, you could provide a function that takes as a parameter a function of type forall x y z . {P x y z} + ~{P x y z}, and returns a decision procedure deciding a commonly undecidable problem. (My favorite is Post's Correspondence, simulating a 2-counter machine is also an easy one). This reduces the trusted base of your proof: now the reader only needs to believe that PCP or 2CM is undecidable in order to see that your problem is.

| cite | improve this answer | |
$\endgroup$
  • $\begingroup$ hmm... i see, so undecidability isn't "not decidable". do you have an established example so that i can follow? $\endgroup$ – Jason Hu Oct 9 '18 at 2:31
  • $\begingroup$ @HuStmpHrrr that's not quite right. It's that "expressibility in MLTT or COC is sufficient, but not necessary, for decidability". i.e. there are problems which are not expressible in MLTT or COC (such as self-interpreters or self-type-checkers) which are decidable (using Turing Machines or untyped lambda calculus). $\endgroup$ – jmite Oct 9 '18 at 2:34
  • $\begingroup$ i see. it seems i am having some misunderstandings on certain concepts. $\endgroup$ – Jason Hu Oct 9 '18 at 2:59
  • $\begingroup$ $¬(∀ x y z. (P x y z) + ¬(P x y z))$ is not really appropriate for other reasons. It means there is a refutation of the universal statement, but MLTT does not automatically refute such things merely because they correspond to undecidable problems. It's possible you could add anti-classical principles that would allow you to do so, but there are also cases where this won't work. Consider LPO + ¬LPO from Andrej's answer. It's not a theorem, but also not refutable. You could add ¬LPO (I think) to be anti-classical, but that makes LPO decidable (it's false). $\endgroup$ – Dan Doel Oct 10 '18 at 2:58
1
$\begingroup$

One way to show that a predicate $P : A \to \mathsf{Type}$ is not decidable is to demonstrate, using intuitionistic reasoning, that decidability of $P$ implies decidability of a statement $S$ which is known not to be decidable. Since you are working in Coq, it helps to target a statement $S$ which is easily expressible in Coq.

For instance, we might use the principle LPO, $$\textstyle \mathsf{LPO} \equiv \prod_{f : \mathbb{N} \to \mathsf{bool}} (\sum_{n : \mathbb{N}} \mathsf{Id}(f n, \mathsf{true})) + \lnot (\sum_{n : \mathbb{N}} \mathsf{Id}(f n, \mathsf{true})). $$ Ths is an instance of excluded middle, but is sometimes easier to reduce than general excluded middle. If you tell us a little bit about your problem, we might be able to suggest a good candidate $S$.

| cite | improve this answer | |
$\endgroup$
  • $\begingroup$ thanks for you suggestion. The problem is a calculus with subtype relation. it would be hard to present the concrete problem without showing the whole definitions. but I guess one easy way to say it is that it's a calculus with bounded quantifications. it's a richer language than F-sub, which Pierce showed two counter machine reduces to. that's why people tend to cross fingers and claim it's for sure undecidable. $\endgroup$ – Jason Hu Oct 9 '18 at 15:49
  • 1
    $\begingroup$ If you can just adapt Pierce's result then that's that. If you'd also like to formalize the proof in Coq, that's a different kind of problem that might require a lot of work. $\endgroup$ – Andrej Bauer Oct 9 '18 at 16:43
  • $\begingroup$ right. that's why i am asking. i want to see how to formally prove undecidability and if there is someone has done similar things before. $\endgroup$ – Jason Hu Oct 9 '18 at 16:45
  • $\begingroup$ As a first step, I'd show formally that Pierce's calculus embeds into yours, that will be easier than the non-decidability result. After that it's "just" formalization of a previously known result, so there's going to be less pressure and motivation to do it. $\endgroup$ – Andrej Bauer Oct 11 '18 at 6:23

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.