Difference between proof of negation vs proof by contradiction in practice?

Question

This article explains the difference between proof of negation and proof by contradiction, and this question has asked for a clarification.

I understand the difference in the abstract. If we don't assume the law of excluded middle, i.e. we are in intuitionist logic, then there is a difference between

proof of negation. Assume $Q$, derive absurd, hence $\neg Q$.

proof by contradiction. Assume $\neg Q$, derive absurd, hence $Q$.

However, it is unclear to me how to know in practice which one of these we are dealing with. The author explains this with some examples, but I don't understand the explanations, despite reading carefully. How do I recognize for a proof "in the wild", whether it's using proof of negation or proof by contradiction?

In particular, the following confuses me:

• Is there really an "objective" way of determining whether a proposition is of the form $Q$ or of the form $\neg Q$? For example, the statements "function $f$ is continuous" and "function $f$ is discontinuous". Which of these is of the form $Q$ and which is $\neg Q$? As soon as we've made a choice which of the two is "more fundamental", then the difference between proof of negation and proof by contradiction becomes well defined.

• Note that my question is about intuitionist logic, not constructive mathematics. I don't fully understand the exact relation between the two, but my question assumes classical interpretation of propositions. (e.g. in my example above, "continuous" means what it means classically, not what Brouwer means by it).

Answer 1

In formal logic, statements are just strings of symbols, so which one is which is not just "objective," it is trivial. One of the statements is $Q$ and the other one is $Q$ with a "$\lnot$" in front of it. You recognize a proof of negation cause it starts with an assumption of some statement $Q,$ derives a contradiction and then concludes $\lnot Q,$ whereas the other kind starts with a statement of the form $\lnot Q$ for some statement $Q$ and then derives a contradiction and then concludes $Q.$ Again, it is plain which is which because in a proof of negation, the conclusion is the initial assumption with a "$\lnot$" attached on the front whereas in a proof by contradiction, the conclusion is the initial assumption with a "$\lnot$" chopped off the front.

Notice that we can do a proof of negation starting with a statement of the form $\lnot Q,$ in which we assume $\lnot Q,$ derive a contradiction and then conclude $\lnot\lnot Q.$ The key is of course that in classical logic, this is equivalent to $Q$ (so this is really the same thing as a proof by contradiction) whereas in intuitionistic logic it is not (so proof by contradiction does not follow).

But mathematics isn't as simple as syntax (so I'd argue, your question is actually about constructive math, and not just intuitionistic logic).

About whether "f is continuous" or "f is discontinuous" is a negated statement, that really depends how each is defined. If we take "f is continuous at $x_0$" to mean "for all $\epsilon>0$ there is a $\delta > 0$ such that for any $x,$ $|x-x_0|<\delta$ implies $|f(x)-f(x_0)|<\epsilon$" and convert that into formal logic, we see that it doesn't begin with a negation. Now we can take two routes to defining "$f$ is discontinuous at $x_0$". For the first we can simply plop a "$\lnot$" in front of the sentence "f is continuous." But in classical math we will usually pass to a (classically) equivalent form "there exists an $\epsilon>0$ such that for all $\delta > 0$ there exists an $x$ such that $|x-x_0|<\delta$ and $|f(x)-f(x_0)|\ge \epsilon$" and we could just as well define "$f$ is discontinuous at $x_0$" by this sentence. This is not a negation, and in intuitionistic, logic is not equivalent the "$f$ is not continuous."

Since intuitionistic logic is weaker than classical logic, it proves fewer equivalences between statements, and so we should expect to have to juggle more definitions. (Man on laptop gives an example of "apartness" in the comments.)

There is a question we could ask as to whether a given sentence (regardless of its syntactic form) is provably equivalent to a sentence of the form $\lnot Q.$ In classical logic, every sentence is, since any sentence $P$ is equivalent to $\lnot\lnot P.$ In intuitionistic logic, on the other hand, this is not necessarily the case but it can happen: one example is that $\lnot A\land \lnot B\leftrightarrow \lnot(A\lor B).$

But I think the main point is we just need to be more careful about thinking about the formal versions of mathematical statements in constructive contexts, to make sure we distinguish between classically equivalent statements that aren't constructively equivalent.