Question: 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](https://i.stack.imgur.com/YtHMp.gif)

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.

Answer: 
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.
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.