# Why might you not accept ¬(¬A) = A?

What motivates intuitionism's rejection of double negation:

If A exists, then ¬(¬A) = A.

I can't see what's wrong this statement or why someone would reject it.

• I've made some edits to make it more about why someone would use intuitionism rather than as if intuitionism has a will. I've also cleaned up the tag choices. Oct 8 '15 at 12:20
• They don't accept negation of a true statement Oct 8 '15 at 14:23
• There are lots of similar "real life example" you would reject too I'm sure. Take, for example, "being tall" or "being small", or "being good" and "being bad". Do you believe that LEM holds there?
– sure
Oct 8 '15 at 14:26

Another way to understand it is that intuisionism is naturally interpreted as the logic of proof rather than the logic of truth. To the intuitionist, A means "I can prove A". ¬A means "I can prove there is no proof of A". A ∨ B means "I can prove A or I can prove B". A ∧ B means "I can prove A and I can prove B". This is why A ∨ ¬A (LEM) is not a theorem of intuitionistic logic, because in general there might be no proof of either. Thus ¬(¬A) means "I can prove that there is no proof that there is no proof of A" but clearly this is a weaker claim than I can prove A, so this is why intuitionistic logic lacks the rule of double negation elimination.

Because it is equivalent to Law of Excluded Middle and to Reductio ad absurdum :

Intuitionistically, Reductio ad absurdum only proves negative statements, since ¬¬A → A does not hold in general. (If it did, LEM would follow by modus ponens from the intuitionistically provable ¬¬(A ∨ ¬A).)

The rejection of LEM by Brouwer is motivated by his view that :

the general LEM was equivalent to the a priori assumption that every mathematical problem has a solution — an assumption he rejected, anticipating Gödel's incompleteness theorem by a quarter of a century.

In general, for Intutionism the ground for asserting a statement is to have a proof of it. This implies that the negation of a statement must be "grounded" by its refutatuion, i.e. by the proof that there is a counterexample. This fact introduces an asymmetry between an affirmative statement and a negative one.

If a statement P is provable, then for sure we cannot find a counterexample, i.e. a case showing ¬P, i.e. it is impossible to prove that there is no proof of P. And this license the inference P → ¬¬P.

But the vice versa does not hold : even if it can be shown that no disproof of P is possible, we cannot conclude from this absence that we have a proof of P. Thus P is a "stronger" statement than ¬¬ P and the inference ¬¬P → P does not hold.

See this post for some reason about the constructive rejection of LEM.

From a classical perspective... I am fond of examples where one adopts things like this not for any philosophical or dogmatic reason, but simply because it captures something of classical interest.

There are contexts in classical mathematics where one can interpret logic in a geometric way, equating "truth value" with "open set of a topological space" or similar. In this translation, "not U" becomes "the exterior of U", and the exterior of the exterior of an open set can indeed be something different than the open set itself. (e.g. consider the open set consisting of the entire plane minus a single point)

In fact, I am under the impression that some intuitionistic ideas (e.g. choice sequences) already have a direct geometric interpretation; e.g. for choice sequences, `P(s)` implies `P(x)` for all `x` in an open set containing `s`. (where a basis for the topology is given by the sets defined by initial sequences)

This probably happens when you stop talking in the mathematical sense and think of it more literally.

If you have proven that you cannot prove (¬) that, say, "god does not exist" (¬A), (feel free to edit in a better/less controversial sentence), have you proven that "god does exist" (A)? In literal terms, no.

One rather important point to understand is that as a practical matter, a logic is only useful to the extent that it faithfully models the (possibly real-world) system that you are trying to analyse. Logic is a hard-nosed engineering discipline these days, and there are far too many practical formal systems where double negation simply doesn't hold.

As Mauro Allegranza pointed out, intuitionistic logic is the logic behind constructive proofs. A constructive proof is a procedure for constructing a conclusion from a collection of premises. What do we mean by "procedure"? Well, think of it as something that can be implemented as a computer program. In fact, a constructive proof is the same thing a computer program in a deep sense, but I digress.)

That is an extremely useful property! In most practical situations, it's not enough to be confident that an answer exists to some question. More likely, you want to find out what the answer (or an answer) actually is.

Formal systems based on intuitionistic logic are typically decidable, in that they have effective computation procedures which will give you an answer to any question. Similarly, they are typically complete, in the Gödel sense; the proofs of Gödel's incompleteness theorems or Cantor diagonalisation arguments are inherently non-constructive, so they don't apply to formal systems which only allow constructive proofs.

So it's not really a question of not accepting it. It's more that there are a formal systems where it's not correct, and formal systems where it would make the system useless for various practical purposes.

Well, how do you resolve Russel's paradox? (Does the set of all those sets that do not contain themselves, contain itself?)

If you decompose the language, you find there are only three ways: You can question the meaning of 'all sets'. You can question whether negation applies to all propositions equally. Or you can question whether self-reference should be allowed in general.

The solutions that involve avoiding inappropriate self-reference, or limiting what 'all sets' mean quickly become elaborate and confusing, in ways that make one lose confidence in their ultimate consistency. It is easiest to limit negation, instead.

We know negation works when we use it in 'constructive' situations where we can trace all the steps involved in all the definitions. But even in day-to-day life, once we generalize negation to everything, we get confused. We have to ponder whether 'nothing' actually exists or not, or we have to agree that it makes no sense to say "nothing does not exist" because double negation sometimes just is not meaningful.

If double negation sometimes results in meaningless statements, it is impossible to believe "A = not not A" in general, because a statement like 'everything exists' is not meaningless in the same way as its double negative 'nothing doesn't exist'.

• I'm unclear on your final paragraph. Why is "nothing doesn't exist" a double negative of "everything exists"? Isn't that just the first negation of it? And why would "nothing doesn't exist" be a meaningless statement? Dec 16 '15 at 4:32
• There are two negations there -- one that converts everything to nothing, and the other that converts 'exists' into "doesn't exist".
– user9166
Dec 16 '15 at 17:41