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.