10 Negation

Each logical connective considered in the previous chapter was implemented using a datatype holding information about the arguments of the connective. This seems a tall order for negation. How can we build a proof of ¬ A ("not A") out of a proof for A, when we expect A to have no proof?

In a nutshell, the proof that something is impossible involves getting from it to something else known to be impossible. The one thing we know to be impossible is finding a value in the empty type. Consider a function with type (A → ⊥). If there were a value of type A, we could apply this function and get a value of type ⊥. Thus A must be empty, that is, there is no proof of A. This will be our definition of ¬ A.

Working with negation definitely takes some getting used to, but you’ll soon get the hang of it (practice is essential). If your goal is a negation, you need to construct a function, and you can do so with a lambda or by adding an argument to the left-hand side. In either case you should choose a variable name that reminds you of the impossible thing that its type represents, and then use that variable to construct ⊥. If your goal is unprovable and you can see a contradiction in the context, then apply ⊥-elim to make the goal be ⊥, and then set about constructing that from the context. Going in the other direction, if your goal is ⊥, and you have a negation in the context, you can apply that negation to make the goal be what is negated.

10.1 Intuitive and Classical Logic

Certain ways you might be used to reasoning classically cannot be done intuitionistically. Defining ¬ A as (A → ⊥) corresponds to the following pattern of reasoning: "Assume A, use that in reasoning, get a contradiction, conclude ¬ A." But you don’t get the similar classical pattern that goes like this: "Assume ¬ A, use that in reasoning, get a contradiction, conclude A." That pattern, when formalized, is double negation elimination (¬ ¬ A → A) and it cannot be proved in intuitionistic logic.

Because there is so much explicit manipulation of proof objects in Agda, it seems to be easier to avoid thinking in classical patterns (as opposed to working in Coq, which is typically at a higher level). But you should be aware of some other patterns that won’t work. In this chapter we see a proof of contraposition, (A → B) → (¬ B → ¬ A). But the converse, (¬ B → ¬ A) → (A → B), cannot be proved. Later in the chapter, we see that one of deMorgan’s laws cannot be proved (though others can). Actually proving (metamathematically) that these cannot be proved is a fascinating exercise, but beyond the scope of this course. One can sometimes get a sense of why, particularly when disjunction is involved, since proving an intuitionistic disjunction requires definitely injecting a value from one side or the other. One cannot say, "Oh, there’s a value in one of these two, I just don’t know which."

The most significant absence is the law of the excluded middle (LEM): ∀ {A : Set} → A ⊎ ¬ A. (On Twitter, someone I follow expressed disdain for the name of this law, and I suggested as an alternative "There is no try.") It’s important to realize that it may hold for specific A, or if A is replaced by some more complicated function of A. But in full generality, it cannot be proved.

All is not lost, however; these laws can be added as axioms without rendering Agda inconsistent. For LEM, this can be shown with a short proof (called em-irrefutable in 842Negation). I almost wish this had not been done in PLFA, because the proof feels impossible at first, and like a magic trick when completed. I have used it as an assignment question in an undergraduate class.

But an even better exercise is left to us at the end of the file. The "Classical" exercise (I call it "Classical five") gives five laws that hold in classical logic but not in intuitionistic logic. The exercise is to show them all equivalent, that is, each one implies all of the others. This would be twenty implications, but by invoking transitivity, it is possible to do it in as little as five proofs. This exercise appeared in the "Coq’Art" book, formally titled "Interactive Theorem Proving and Program Development", by Bertot and Casteran (2004), though it is much older than that. It also appears in SF.

I have solved the Classical five exercise twice in Coq (two years apart) and twice in Agda (one year apart). It’s definitely easier and more fun in Agda. I have not assigned it as an exercise, to give you the pleasure of solving it without being required to solve it. (Also it is a pain to mark.) I managed (by reusing earlier theorems) to refine my Agda solution to five proofs, each of which has one type signature line and one equational line. But you don’t have to go this far. Six, or seven, or ten proofs are fine, and use as many equational lines as you wish. Just relax and enjoy yourself.

Since we can add any of these as an axiom, and prove more things, why not add them? The price we would pay is that there are no computational interpretations of axioms. In fact, the second half of PLFA uses this lack of computational interpretation as a way to signal an error. There is a fairly simple translation involving double negations that will convert any statement provable in classical logic into one provable in intuitionistic logic. Sticking with intuitionistic logic also lets us discern finer metamathematical structure, just as we did by working with isomorphisms and embeddings instead of just propositional equivalence.