Back to Coq Main Page Abstract: Our first Lab Exercise contains a few samples, which require so called 'classical axioms'. This document explains, how to use them.

What is Intuitionistic logic

Propositional logic expressions that are straightforward to prove using Coq tactics are part of the Intuitionistic (Constructive) logic. It does not allow existence proofs 'from the contrary'. In such proofs we first assume that some object does not exist, get a contradiction and conclude that the object therefore must exist. Such proofs are problematic, because they do not provide even a totally impractical method allowing the construct the objects that presumably should exist. Most contemporary mathematicians do not care about this difference, they simply use classical logic. Computer scientists should at least understand the difference, because non-constructive proofs cannot yield any algorithms.

Classical proofs in 'real' mathematics

Classical (non-constructive) proofs may appear in answering various natural-looking questions. For example,

• Can an irrational number raised to an irrational power be a rational number?
• Intermediate Value Theorem: If a continuous real-valued function defined on a closed interval [a;b] has two different values f(a) and f(b), then it also takes all the intermediate values on that segment.
• Consider game 'Chomp' where cookies are laid out in a rectangular grid, and the cookie in the upper left corner is poisoned. Even though there must exist a (constructive) winning strategy for one of the players, it is possible to provide a nonconstructive proof that the 1st player always wins without any deep analysis. (See Example 12, p.102, in Chapter 1.8 of the K.Rosen's textbook).

Many of these results can be stated and proved in a constructive way as well. Sometimes though, there is a deeper reason, why some math result is not constructive.

Classical proofs in Coq

All the non-constructive things can be imported from Coq library Classical_Prop Furthermore, if you wish to try non-constructive things in Coq and see some proofs, there is a chapter in the Software Foundations textbook: Classical vs. Constructive Logic. At the very end of this chapter, it is stated, that there are multiple possible formulations of 'nonconstructive' (i.e. classical) axiom. They are all logically equivalent. Assuming any one of them immediately means that you can prove all the others. Therefore, there is only one 'flavor' of nonconstructive mathematics. The textbook leaves as an exercise to prove that from any statement you can prove any other one. Here are the five main nonconstructive statements. Any one of them can be picked as an 'Axiom' (something you want to assume without any proof), the remaining four can be 'Lemmas' - they can be proven using that axiom and the proof tactics from Coq.

Excluded Middle

In the Coq library Classical_Prop this is the only axiom, but if you assume another axiom, this can also become Lemma. This is the rule known in the Ancient logic textbooks - either 'P' or 'not P' must be true. (Also known with the Latin name: 'Tertium Non Datur')

  Axiom excluded_middle: forall P: Prop,
    P \/ ~P.

Pierce Lemma

Here is another result (written without negations, which surprisingly, also allows you to prove all kinds of nonconstructive proofs 'from the contrary'. It happens to be also sample1_3 in our lab exercise.

  Lemma peirce: forall P Q: Prop,
    ((P -> Q) -> P) -> P.

Double Negation Lemma

This lemma tells that we can always drop two negations, and the proposition will stay valid.

  Lemma double_negation_elimination: forall P:Prop,
    ~~P -> P.

De Morgan's Law

This is just one variant; other De Morgan's laws can be written by switching the order in the implication or changing disjunction to conjunction and vice versa. Some of these laws can be proven constructively, but this one cannot.

  Lemma de_morgan_not_and_not: forall P Q:Prop,
    ~(~P /\ ¬Q) -> P \/ Q.

Implication expressed as disjunction

  Lemma implies_to_or: forall P Q:Prop,
    (P -> Q) -> (~P \/ Q).

Sample Proofs

Any non-constructive proofs start by importing this external library. If you want to see what's inside this library, you can do one of the following:

• Read HTML documentation: Classical_Prop.html
• Inspect the same source code in GitHub: Classical_Prop.v
• Import and then print the definitions in that library.

  Require Import Classical_Prop.
  Print Classical_Prop.

The above two commands will display all the available definitions in a compact, readable format.

Double Negation Proofs

This can be verified by truth tables:

  forall a: Prop, a <-> ~~a.

It means an obvious thing: Every proposition is equivalent to the double negation of that proposition. As it turns out, a half of this statement is not constructive. In the Coq library Classical_Prop this lemma is called NNPP

Next, let us consider 'a -> ~~a' The opposite implication is intuitionist, it does not need any classical lemmas:

• Peel off the 'forall' variable. Write 'intros a' to avoid renaming the variable.
• Rewrite not: '~~a' becomes 'a -> ((a -> False) -> False)'.
• Assume that 'a' is true (introduce hypothesis 'a'
• Next assume that 'a' is false (introduce hypothesis 'a->False'.
• Now both hypotheses are contradictory.
• Therefore any goal (False in our case) is proven: 'a'

and 'a->False' imply anything. In Coq this proof looks like this:

Once we have both negation manipulation lemmas, we can prove some variations. In this example we proceed like this:

• Peel of the forall a variable.
• .Apply the double_negation_rev lemma to get

rid of two negations in the beginning: ~ ~ (~ ~ a -> a) becomes ~ ~ a -> a.

• Next, use the double_negation_elimination to get exactly

the same result we have to prove.

Contrapositive lemmas

Same as before: it turns out that contrapositive law is 'classical' (non-constructive) in one direction, but is constructive/intuitionist in the opposite direction. This result uses double_negation_elimination, which in turn relies on the classic axiom.

In contrast to the previous example, which used earlier (non-constructive/classical) This does not require to import any external libraries:

Some proofs of Peirce lemmas

This proof uses double_negation_elimination also known as NNPP lemma to prepend two negations.

Now the same lemma is proven using the classic axiom. It is named Peirce2 since the names of lemmas must not be conflicting.

De Morgan's laws

As we already saw in other lemmas, one direction of a lemma may be 'classic' (requiring the law of excluded middle).

And the other direction does not need any classical things. This proof is intuitionist.

Rewrite implication as a disjunction

Such manipulations also need the 'classic' axioms.