A few days ago I found a video on YouTube explaining how to use CoqIde, the IDE for the Coq proof assistant. The proof that was used to illustrate the IDE was the equivalence between *Peirce’s law* and the *excluded middle law*, that is, the equivalence between the two following laws:

$\mleq{(0)}

{((p{\Rightarrow}q){\Rightarrow}p)\Rightarrow p}

$

and

$\mleq{(1)}

{\neg{p} \vee p}

$

After watching the video, I wrote a *goal-oriented, calculational* proof of the equivalence between (0) and (1). In this short note, I describe the design of my proof.

## A calculational proof

A useful rule of thumb is to start with the most complicated side, for it is usually easier to simplify expressions than to complicate them. With this in mind, let us try to manipulate (0) so that it becomes (1).

Looking at the shapes of (0) and (1), we immediately see that $q$ occurs in (0), but not in (1). So, if we start with (0), we will have to eliminate the occurence of $q$. This suggests that we have to use laws that involve the elimination of variables. Two elementary rules that are of this kind are the so-called absorption rules for conjunction and disjunction:

$\mleq{(2)}{(p \wedge q) \vee p ~\equiv~ p}$

$\mleq{(3)}{(p \vee q) \wedge p ~\equiv~ p}$

At a first sight, these rules may not seem very useful, because they involve only conjunction and disjunction and we want to eliminate a variable from a formula involving implication. But we know that implication can be written in terms of negation and disjunction:

$\mleq{(4)}

{{p{\Rightarrow}q} ~\equiv~ {\neg{p} \vee q}}

$

These observations, together with the De Morgan rule, allow us to write a *goal-oriented, calculational* proof of the equivalence between (0) and (1):

\[

\beginproof

\pexp{((p{\Rightarrow}q){\Rightarrow}p)\Rightarrow p}

\hint{=}{rewrite the two leftmost $\Rightarrow$ using (4)}

\pexp{{\neg{(\neg{p} \vee q)} \vee p} ~\Rightarrow~ p}

\hint{=}{De Morgan rule, that is, $\neg{(\neg{p} \vee q)} ~\equiv~ (p \wedge \neg{q})$}

\pexp{{(p \wedge \neg{q}) \vee p} ~\Rightarrow~ p}

\hint{=}{absorption (2)}

\pexp{p{\Rightarrow}p}

\hint{=}{rewrite $\Rightarrow$ using (4)}

\pexp{\neg{p} \vee p ~~.}

\endproof

\]

## The video

The video that I mentioned is shown below. It would be unfair to compare the proofs, since the main goal of the video is to illustrate Coq’s IDE and not to show how to design proofs. Nevertheless, I would like to invite the reader to comment on the use of automated/interactive theorem provers to design proofs. Thanks for reading.

Peirce’s law and LEM are two characterizations of classical logic: the point of the Coq proof is to show that they are equivalent in intuitionistic logic. That is, if either one was added as an axiom on top of intuitionistic logic, it would be possible to derive the other. Your proof uses classical logic; both the equivalence of p -> q to ~p \/ q and also the version of De Morgan’s law you use (which involves double negation elimination) are only valid in a classical setting. Proving that Peirce’s law and LEM are equivalent using classical logic is not very interesting, because both are independently derivable from the axioms — it’s like proving “true iff true”.

I would, however, be interested in seeing a calculational presentation of the intuitionistic proof, which is notoriously tricky to grok. The video doesn’t really give much insight into how the proof actually goes since it uses some high-powered Coq automation.

Hi Brent, thanks for your comment. Perhaps I should have made it clear that my proof uses only classical logic. For me, this was an exercise on formulae manipulation: how to get from one formula to another by syntactic manipulation. Of course that the result by itself is not very interesting; I could have just proved that Peirce’s law is a theorem in classical logic and then conclude that it must be the same as any other theorem. (By the way, I wouldn’t use the proof above to show that it is a theorem; I would rather use the connecting lemma and the fact that distributivity distributes over equality.)

If I have time, I’ll think about calculational approaches to the intuitionistic proof.

Hello! I gave this proof a try today, also as an experiment in symbol manipulation. (For the record, I came up with a very different proof.)

But Brent’s point is quite valid: ~p \/ q == p => q is equivalent to the law of the excluded middle. (Actually, if I remember correctly, only one half of the equivalence is.)

I would like to attempt a different proof, but I’m not sure which laws to avoid!