How can MLTT etc encode computability?

Question

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.

Answer 1

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.

Answer 2

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$.