Do undecidable languages exist in constructivist logic?

Problem Detail: 

Constructivist logic is a system which removes the Law of the Excluded Middle, as well as Double Negation, as axioms. It's described on Wikipedia here and here. In particular, the system doesn't allow for proof by contradiction.

I'm wondering, is anyone familiar with how this affects results regarding Turing Machines and formal languages? I notice that almost every proof that a language is undecidable relies on proof by contradiction. Both the Diagonalization argument and the concept of a reduction work this way. Can there ever be a "constructive" proof of the existence of an undecidable language, and if so, what would it look like?

EDIT: To be clear, my understanding of proof by contradiction in constructivist logic was wrong, and the answers have clarified this.

Asked By : jmite

Answered By : gelisam

Yes. You don't need the excluded middle to derive a contradiction. In particular, diagonalisation still works.

Here is a typical diagonalisation argument by Conor McBride. This particular diagonalisation is about incompleteness, not undecidability, but the idea is the same. The important point to notice is that the contradiction he derives is not of the form "P and not P", but of the form "x = x + 1".

Of course, now you might be wondering whether constructive logic admits "x = x + 1" as a contradiction. It does. The main property of a contradiction is that anything follows from a contradiction, and using "x = x + 1", I can indeed constructively prove "x = y" for any two natural numbers.

One thing which might be different about a constructive proof is the way in which "undecidable" is defined. In classical logic, every language must either be decidable or undecidable; so "undecidable" simply means "not decidable". In constructive logic, however, "not" isn't a primitive logical operation, so we cannot express undecidability this way. Instead, we say that a language is undecidable if assuming that it is decidable leads to a contradiction.

In fact, even though "not" isn't a primitive in constructive logic, we typically define "not P" as syntactic sugar for "P can be used to construct a contradiction", so a proof by contradiction is actually the only way to constructively prove a statement of the form "not P" such as "language L is undecidable".

Best Answer from StackOverflow

Question Source : http://cs.stackexchange.com/questions/12492