32
$\begingroup$

A friend of mine asked me if I could explain this statement: "It's not logically possible to prove that something can't be done". The actual reason is the understanding of this strip:

enter image description here

Since I'm not an expert on logic, but at least know the basics, I told him that the statement is false. To prove it I gave him the counterexample of the impossibility of trisecting an angle by using only straightedge and compass, which was proved by Pierre Wantzel. This shows clearly that it's possible to prove that something can't be done.

When I told him this, he explained to me that this is sort of naive because Asok, the guy who makes the statement, is a graduate from IIT and also I read that he's always a brilliant character in the strip.

Can you guys please tell me what you think about this? Also I'd like to know how you would interpret this dialog.

$\endgroup$
  • 7
    $\begingroup$ Maybe a reference to the Halting problem solved by Turing? $\endgroup$ – karvens Sep 25 '14 at 0:15
  • 6
    $\begingroup$ If "this dialog" means the dialog between you and your friend, my interpretation is that your friend would prefer to believe that it's impossible for anyone to prove he is wrong. Calling it "naive" is just a cheap debating trick. $\endgroup$ – David Sep 25 '14 at 0:17
  • 49
    $\begingroup$ By the way, the argument "It must be true because a smart person said it" is even weaker than usual when that smart person is a cartoon character. $\endgroup$ – Slade Sep 25 '14 at 0:18
  • 13
    $\begingroup$ Asok may be a graduate from IIT and a brilliant character, but he is written by Scott Adams, who is (arguably) neither. $\endgroup$ – Rahul Sep 25 '14 at 6:45
  • 5
    $\begingroup$ If it's not possible to prove that something can't be done then it would also not be possible to prove that is was not possible to prove that something can't be done... and so on! $\endgroup$ – JamesRyan Sep 25 '14 at 11:36

15 Answers 15

29
$\begingroup$

What the strip most likely was (awkwardly) referring to is not that it's impossible to prove something can't be done, but rather that it's impossible to prove within a (sufficiently powerful) formal system that something can't be proven in that system — in other words, letting $P(\phi)$ be the statement 'there exists a proof of $\phi$', then it's impossible to prove any statement of the form $\neg P(\phi)$ (i.e., the statement $P(\neg P(\phi))$ can't be true).

The reason behind this has to do with Godel's second incompleteness theorem that no formal system can prove its own consistency - in other words, the system can't prove the statement $\neg P(\bot)$ (or equivalently, $P(\neg P(\bot))$ is false). The logical chain follows from the statement 'false implies anything': $\bot\implies\phi$ for any proposition $\phi$. By the rules of deduction, this gives that $P(\bot)\implies P(\phi)$, and then taking the contrapositive, $\neg P(\phi)\implies\neg P(\bot)$ for any proposition $\phi$; using deduction once more, this gives $P(\neg P(\phi))\implies P(\neg P(\bot))$ — if the system can prove the unprovability of any statement, then it can prove its own consistency, which would violate Godel's second incompleteness theorem.

Note the keyword 'sufficiently powerful' here - and also that we're referring to a formal system talking about proofs within itself. This is what allows statements like the impossibility of angle trisection off the hook: the axioms of ruler-and-compass geometry aren't sufficiently strong for Godel's theorem to apply to the system, so that geometry itself can't talk about the notion of proof, and our statements of proofs of impossibility within that system are proofs from outside of that system.

$\endgroup$
  • 3
    $\begingroup$ I am not sure that I agree with your interpretation of the strip (although really I don't know). If your interpretation were correct then would Dan not be saying "and I can prove it using a computer"? (Although computer's are Turing machines...perhaps human minds are just Turing machines? Thus my earlier disclaimer: really I don't know...) $\endgroup$ – user1729 Sep 25 '14 at 12:35
  • 1
    $\begingroup$ @user1729 'Sufficiently powerful formal system' was referring to the formal system of logic being used to construct the proof, not a computer system. $\endgroup$ – reirab Sep 25 '14 at 14:26
  • 3
    $\begingroup$ It looks like you're interpreting Asok's "can't be done" as "can't be proved within a formal system". I don't see any evidence that Asok is talking about formal systems; what's your reasoning? $\endgroup$ – Tanner Swett Sep 25 '14 at 16:32
  • 5
    $\begingroup$ @TannerSwett I'm Working under the perhaps-generous assumption that the strip was trying to be mathematically accurate at some level, and offering up an interpretation of the statement that makes mathematical sense. $\endgroup$ – Steven Stadnicki Sep 25 '14 at 16:55
  • 1
    $\begingroup$ @MatthijsWessels I said it was true; I didn't say I'd proved it! More accurately (and I may revise my answer to reflect this), I've shown that if the system is consistent, it can't prove any statement of the form $\neg P(\phi)$, and in fact the system can prove that if it could prove a statement of the form $\neg P(\phi)$ it could prove its own consistency. But it doesn't know that it can't prove its own consistency, either! (It knows that if it could prove its own consistency it would be consistent, buuuuut...) $\endgroup$ – Steven Stadnicki Sep 26 '14 at 15:40
26
$\begingroup$

Scott Adams may have intended something different, but in the given context and with the given wording, Dan is right and Asok is wrong.

Imagine Asok writing a piece of software that crucially depends on deciding the halting problem (or any other property covered by Rice's theorem), then Dan is right: The halting problem is not decidable and therefore the software will never work. And Dan can indeed prove it, because the undecidability of the halting problem is provable.

$\endgroup$
  • 3
    $\begingroup$ It's more about a rude scientist claiming his superiority, and Asok making fun of him. $\endgroup$ – gnasher729 Sep 25 '14 at 16:46
  • 3
    $\begingroup$ @gnasher729 True. That's what this strip is supposed to convey. Asok is still wrong, though :) $\endgroup$ – Sebastian Negraszus Sep 25 '14 at 17:47
  • 1
    $\begingroup$ A professor of mine used to say, "I'd rather be rude than wrong". Needless to say it, wasn't the most enjoyable class to attend! $\endgroup$ – crypton480 Sep 25 '14 at 21:38
  • 8
    $\begingroup$ @crypton480 In my experience, people who say 'I'd rather be rude than wrong' are often both. $\endgroup$ – Steven Stadnicki Sep 25 '14 at 23:07
  • $\begingroup$ @Steven Stadnicki - Well said! $\endgroup$ – crypton480 Sep 25 '14 at 23:11
11
$\begingroup$

It's a paradox: by saying "it's not logically possible to do X", Asok is, in effect, claiming that there must exist a proof that X is impossible. Which is impossible, if Asok is right.

Hence Asok must be wrong!

$\endgroup$
  • $\begingroup$ Asok is not claiming that it's possible to prove that its impossible to prove that something is impossible. He is just claiming that it's actually impossible, and leaves the reason for this proof in the air. $\endgroup$ – Taemyr Sep 25 '14 at 10:10
  • $\begingroup$ Similar problem with people saying "It's not possible to prove a negative." :P $\endgroup$ – yters Sep 25 '14 at 19:25
6
$\begingroup$

Basically the strip is about the scientist being a smartass and not about logic, possiblity of proving something etc. What he says is "software you're writing will never work" (and not "software you wrote"), so at this point it's really impossible to prove anything. It's not possible to prove the software will never work, once it's written. So your friend's conclusion misses the point, he is rather siding with Dan (trying to outsmart you, not understanding the core problem) than with Asok.

$\endgroup$
5
$\begingroup$

"That software you are writing will never work" is not a claim within a formal system.

Trying to cast it into a propositional statement can only ruin the joke (and I can prove it).

$\endgroup$
4
$\begingroup$

Every proof is a proof that something cannot happen, if you phrase it in a particular way.

"There is $X$ such that so on and so forth holds" can be stated as "It is impossible that there is no $X$ such that so on and so forth holds".

For example:

If $\{x_n\}_{n=1}^\infty$ is a bounded sequence of real numbers, then it has a convergent subsequence.

Can be rephrased as:

There is no bounded sequences of reals with no convergent subsequences.

Or using the words "impossible to" we can state it as:

It is impossible to have a bounded sequence of real numbers without a convergent subsequence.


Many concept in mathematics are inherently "impossible". Infinite means "not finite", uncountable means "not countable" and irrational means "not rational". So when we prove that something is infinite we prove that it is impossible to put it into bijection with any finite set; or when we prove that $\sqrt2$ is irrational we prove that it is impossible to write it as a ratio of two integers.

So again, many proofs throughout mathematics are "impossible to do that" sort of proofs, and saying that you cannot logically prove that something is impossible cannot possibly refer to a mathematical proof seriously. But it's important to remember that the word "proof" has a completely more rigid meaning in mathematics than it has in other fields of science and life.

$\endgroup$
3
$\begingroup$

I think what the author means is that it is impossible to prove that a software "will never work": you can observe it isn't working by now. But does that mean it will ever work? (excluding trivial scenarios in which the software cease to exist, etc). I think he kind of wants to get in the impossibility of proving absolute existence or absolute nonexistence. Just my thoughts on it... Having said that, your argument about Wantzel seems to be right, just not what the author was pointing out.

$\endgroup$
  • 2
    $\begingroup$ Of course it's possible to prove that software will never work. If the software is trying to solve a problem that has been proven to be unsolvable, then it will never work. $\endgroup$ – reirab Sep 25 '14 at 14:29
3
$\begingroup$

I think the confusion is caused by mixing a technical meaning of "proof" (deriving a result from some axioms and rules) with an informal meaning (showing that something can/cannot 'exist' in the 'real world').

One of the assumptions in Wantzel's proofs is the use of Euclidean geometry. However, general relativity says that space is non-Euclidean, so that proof doesn't apply to the 'real world'.

Every proof can be defeated in this way, using "what if" questions. These kinds of questions, about what is 'real' or 'true', caused a lot of debate before the 20th century. For example, Hilbert sought a single, consistent set of rules which could prove every true statement and disprove every false statement. Many Mathematicians didn't believe Cantor's proofs regarding infinities were 'real'. Kronecker claimed that "God created the Integers, all else is the work of man". There are many more such examples.

These questions are still unresolved, but now fall into the realm of philosophy. Mathematics avoids these issues by accepting that some assumptions are always necessary, that "truth" is an ill-defined concept and we should instead focus on provability.

$\endgroup$
2
$\begingroup$

Graph theory and complexity are a two interesting and applicable fields if you want to get a picture of impossibility. Color the areas of any map with no more than 3 colors is proven impossible by the 4-color theorem since the theorem proves that some graphs take 4 colors. Sorting in linear or constant time is also mostly or always impossible since mostly or always sort takes longer time than linear. A trivial good example could be

  • Software project 1. Software to analytically solve 2nd degree polynomials can be done.

  • Software project 2. Software to analytically solve 3nd degree polynomials can be done.

  • Software project 3. Software to analytically solve 4th degree polynomials can be done.

  • Software project 4. Software to analytically solve 5th degree polynomials can't be done and you can prove it can't be done.

I think the question deals with feasibility and can apply to problems where you trick the engineer working towards goals that are not feasible e.g. DRM rights to "protect" an analog audio stream that can't be physically protected from being recorded.

$\endgroup$
2
$\begingroup$

The strip is talking about the scientific method, not about mathematics. It's perfectly possible to prove something impossible in mathematics. Turing's proof of the undecidability of the halting problem has been mentioned in several answers above but there are plenty of trivial answers: for example, it's impossible to find a nontrivial factor of a prime number.

$\endgroup$
1
$\begingroup$

I agree with your initial response. There exist some tasks T for which it is possible to prove that T cannot be achieved.

$\endgroup$
1
$\begingroup$

Technically, you can prove that something can't be done, provided that you choose an appropriate "something" to prove impossible. Several examples have been cited in answers.

On the other hand, the illogical scientist says Asok's software will not work. How does he define that claim? Does he mean that there is a pathological sequence of events that is at least remotely possible and that will cause Asok's software not to deliver the desired result in that case? He may be right, but there are plenty of very successful software systems that have that characteristic.

Suppose Asok is writing a program to analyze the company's other programs and tell which of the functions will halt on what input. We know Asok's program cannot produce a "yes" or "no" answer in $100\%$ of all possible cases, but even if Asok's program produces a "yes" or "no" answer for only $90\%$ of the cases on which it is actually tried, it can be very useful, so to say "it does not work" in nonsense.

Taken word for word without any additional context, Asok's statement is overly broad, and you have (I think) a valid counterexample. In the context of software engineering, however, where something "works" or "does not work" depending on whether it exhibits suitable behaviors over finite periods of time and finite amounts of input, at least the well-known "impossibility" proofs say only that the software will not always work. This is not at all the same thing as proving it never can work.

$\endgroup$
0
$\begingroup$

I'd say that their both correct but under different domains. Dan is clearly an illogical scientist, which implies that he's not bound to the laws of logic. Unfortunately, in an illogical domain of discourse, every predicate or statement is true.

$\endgroup$
  • $\begingroup$ Non necessarily true, because in an illogical domain of discourse the principle of explosion might be broken ☺ $\endgroup$ – Incnis Mrsi Oct 23 '14 at 15:03
-1
$\begingroup$

To put it simply, it is considered illogical to say that something will never happen.

$\endgroup$
-2
$\begingroup$

By Godel's theorem maths is incomplete or inconsistent, logically. Since we can't accept proofs that are inconsistent we must accept that maths cannot be proven, logically. We need more axioms. If we can't prove maths we certainly can't prove programming.

The halting problem is algorithmic and so has more implicit axioms related to achievability rather than logic. Compare: "it is impossible for me to count to infinity" and "it is logically impossible for me to count to infinity".

$\endgroup$
  • 1
    $\begingroup$ That is not what Goedel's theorem says. $\endgroup$ – Asaf Karagila Sep 26 '14 at 9:08
  • $\begingroup$ Any effectively generated theory capable of expressing elementary arithmetic cannot be both consistent and complete. In particular, for any consistent, effectively generated formal theory that proves certain basic arithmetic truths, there is an arithmetical statement that is true,[1] but not provable in the theory (wikipedia) $\endgroup$ – nicebutdim Sep 26 '14 at 18:13
  • $\begingroup$ Is the wikipedia entry a better statement? $\endgroup$ – nicebutdim Sep 26 '14 at 18:14
  • $\begingroup$ This is not the same as you wrote. $\endgroup$ – Asaf Karagila Sep 26 '14 at 18:22
  • $\begingroup$ Oh I didn't mean that maths is incomplete (although in a sense if you take a constructive point of view it always will be) I mean it is not a complete logical system. $\endgroup$ – nicebutdim Sep 26 '14 at 18:24

protected by Asaf Karagila Sep 26 '14 at 9:07

Thank you for your interest in this question. Because it has attracted low-quality or spam answers that had to be removed, posting an answer now requires 10 reputation on this site (the association bonus does not count).

Would you like to answer one of these unanswered questions instead?

Not the answer you're looking for? Browse other questions tagged or ask your own question.