Natural language examples for failure of double negation elimination

Question

I am trying to explain why double negation elimination $\neg \neg \phi \vdash \phi$ is invalid in intuitionistic logic, but introduction $\phi \vdash \neg \neg \phi$ is valid.

The latter is easy: if I can prove $\phi$, then I can prove that '$\phi$ is contradictory' is contradictory. I might explain this by saying that "if I can see that your coat is blue, then I can immediately construct a contradiction from (your coat is not blue)".

For elimination, one can see how having a proof that `$\phi$ is contradictory' is contradictory doesn't furnish you with a proof of $\phi$ itself, but in my experience people don't find examples like "'(your coat is not blue) is contradictory' does not give a proof that your coat is blue" very convincing.

What I would like is a similar simple natural language example that makes it clear that elimination is not straightforwardly valid.

Answer 1

Even in intuitionistic logic, double negation elimination holds for statements that have to be true or false, in this sense: there is an intuitionistic proof that $$ (\phi \lor \lnot \phi) \to (\lnot \lnot \phi \to \phi). $$ The proof is as follows, by cases: First, if $\phi$, then $\lnot \lnot \phi \to \phi$ trivially. Second, if $\lnot \phi$, then $\lnot \lnot \phi$ implies $\bot$, and $\bot$ implies $\phi$. So overall we would conclude $\lnot \lnot \phi \to \phi$ in each case.

This has an informal consequence for natural language examples: it is necessary to avoid statements for which the audience already believes $\phi \lor \lnot\phi$.

One possibility is to use a modal interpretation of intuitionistic logic instead. So asserting $\phi$ means that $\phi$ is certain, and asserting $\lnot \phi$ means that $\phi$ is impossible.

In this interpretation, we see that $\phi \to \lnot \lnot \phi$ holds because, if $\phi$ is certain, then it is impossible for $\phi$ to be impossible.

But $\lnot \lnot \phi \to \phi$ does not hold in this interpretation because, just because it is impossible for $\phi$ to be impossible, this does not mean that $\phi$ must be certain. Perhaps $\phi$ is only a possibility, neither certain nor impossible.

So, in natural language, if I say: "There is no chance that it is impossible that it will rain tomorrow", this does not imply "It is certain that it will rain tomorrow".

Similarly, DanielV gave a nice example which could be restated as follows. If I say, "It is impossible to say that it is impossible for the defendant to be innocent", this does not allow the jury to conclude that the defendant is innocent.

This relationship between modal logic and intuitionistic logic shows up formally: both of these logics have natural Kripke semantics, and Kripke semantics are one way to verify formally that intuitionistic logic does not prove double negation elimination.

Answer 2

First, I like to formulate classical truth as irrefutability, i.e. some proposition being classically true means that "you cannot refute it". This is essentially the double negation embedding of classical logic into intuitionistic logic.

For constructive logic, the main thing to lean on is constructions or explicit evidence. Changing your wording to something like "can demonstrate" or "have evidence for" helps make what's going on clearer. I'm assuming you want a non-technical "day-to-day" example. It's much easier to make unambiguous technical examples. A non-technical example is going to be less crisp, neveretheless here's one:

Let's say I brought lunch and placed it in the company refrigerator. Come lunch time I find it missing. No one can refute that someone took my lunch, but I have no evidence that some particular person took my lunch. Specifically, I don't know who it was nor do I have evidence that that particular person took my lunch.

This can be tightened by providing a specific definition for "evidence", for example, "video evidence". Maybe I filmed myself placing my lunch in the refrigerator, and, of course, I can film that the refrigerator is now empty, but I have no video evidence of someone taking my lunch. Note how constructively proving $\exists x.\varphi(x)$ requires actually explicitly providing the relevant "$x$", i.e. I can't constructively know $\exists x.\varphi(x)$ and not know a specific $t$ such that $\varphi(t)$ is true.

Again, differentiating between something "being true" versus "having evidence for" something is a key part of understanding constructivism.

Answer 3

Not everyone agrees on conceptualizations of constructive logic, but one way of looking at it is that constructive logic doesn't address true/false, it only addresses provable/not provable. So $\lnot P$ doesn't mean that $P$ is false in material terms, it means that it is not provable in an algorithmic sense.

Prosecutor : "The defense says I can't prove the defendant is guilty. But they can't prove that."
Defense : "This is true."
Prosecutor : "Therefore he is guilty."
Jury: "Agree."

This is one conceptualization of what $\lnot \lnot P \implies P$ means in constructive logic, and why it isn't taken as an axiom.