How can MLTT etc encode computability?
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.