24
$\begingroup$

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.

Improve this question
$\endgroup$
  • 5
    $\begingroup$ Intuitionistic logic doesn't disallow proofs that go "Assume $\phi$, derive a contradiction, therefore $\lnot\phi$". You can do that by definition of $\lnot\phi$, as $\phi\to\bot$. What you can't do is "Assume $\lnot\phi$, derive a contradiction, therefore $\phi$." $\endgroup$ – Miles Rout Sep 12 '16 at 22:37
  • 2
    $\begingroup$ Your edit to the question about "but still allows proof of negative statements by contradiction" makes my answer look like I'm only repeating what the asker already knew :( $\endgroup$ – gelisam Sep 29 '16 at 17:28
  • 3
    $\begingroup$ Instead of modifying this already-answered question so that it asks a slightly more difficult question, how about creating (and answering) a separate question? $\endgroup$ – gelisam Sep 29 '16 at 17:31
  • 1
    $\begingroup$ @gelisam Yeah, as the asker, I definitely don't support the edit. I'll revert it. $\endgroup$ – jmite Sep 29 '16 at 17:59
18
$\begingroup$

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

Improve this answer
$\endgroup$
  • $\begingroup$ In my opinion your answer doesn't clearly distinguish between the law of excluded middle ($P \lor \lnot P$) and the principle of noncontradiction ($\lnot(P \land \lnot P)$). The latter does hold in constructive/intuitionistic logic. $\endgroup$ – Miles Rout Sep 28 '16 at 12:36
9
$\begingroup$

When talking about provability of classical statements constructively it often matters how we formulate them. Classically equivalent formulations do not need to be equivalent constructively. Also it matters what you exactly mean by a constructive proof, there are various schools of constructivism.

For example, a statement stating that there is an uncomputable total function would not be true in those flavors of constructive mathematics which presume the Church-Turing Thesis (i.e. every function is computable) as an axiom.

On the other hand, if you are careful you can formulate it such that it is provable: for any computable enumeration of total computable functions, there is a total computable function which is not in the enumeration.

You may found this post by Andrej Bauer interesting.

ps: We can also look at diagonalization from category theoretic perspective. See

Improve this answer
$\endgroup$
4
$\begingroup$

I think that the cardinality proof still holds, demonstrating the existence of languages that aren't computable languages (so definitely undecidable).

The immediate proof is pretty straight forward, it simply observes that Turing Machines are encoded in some finite alphabet (might as well be binary), so there's countably many, and the set of all languages over a fixed alphabet (might as well be binary again) is the set of all subsets of the set of strings over that alphabet - i.e. the power set of a countable set, and must be uncountable. Therefore there's less Turing Machines than there are languages, so something is not computable.

This seems to me to be constructive enough (although it would be impossible to pursue physically, it gives you a way of pointing at some set of languages and knowing one is not computable).

We might then ask whether it's possible to show that countable and uncountable sets have different cardinality, in particular, avoided diagonalisation. I think this is still possible. Cantor's original argument seems to also be suitably constructive.

Of course, this really needs to be checked by someone who knows much more about constructivist logic.

Improve this answer
$\endgroup$
3
$\begingroup$

I think I agree with others that the diagonalization argument is constructive, although from what I can tell there is some disagreement about this in some circles.

I mean, assume that we're looking at the set of all decidable languages. I can construct an undecidable language using diagonalization. It's worth noting that I don't consider "constructivism" and "finitism" to be the same thing at all, although historically I think these were related arcs.

First, I think everybody - even constructivists - agree that the set of decidable languages is countable. Since the set of Turing machines is countable (we can encode all valid TMs using finite strings), this agreement follows pretty easily.

Since the set of decidable languages is countable, we can assume some enumeration of these languages: $L_1, L_2, ..., L_k, ...$. Here's a procedure that will generate a language not in the set:

  1. Consider the string $0^i$.
  2. If $0^i \in L_i$, then our language should not contain $0^i$.
  3. If $0^i \notin L_i$, then our language should contain $0^i$.

After the $n$th step, our language cannot be any of the languages $L_1, L_2, ..., L_n$. After an arbitrary (or potentially infinite) number of steps, we can't have found a language in the set to match the one we've just constructed.

So technically, we've constructed a language that is "not decidable"; whether a constructivist would argue that "not decidable" shouldn't be confused with "undecidable" is an interesting question, but one which I am ill-equipped to answer.

To clarify, what I think this demonstrates is the following: we can constructively prove that there exist languages not decided by Turing machines. How you choose to interpret that within a particular framework is a harder question.

Improve this answer
$\endgroup$

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.