On Peirce’s law and the law of the excluded middle

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.

Related Posts:

An improved proof of the handshaking lemma

In 2009, I posted a calculational proof of the handshaking lemma, a well-known elementary result on undirected graphs. I was very pleased about my proof because the amount of guessing involved was very small (especially when compared with conventional proofs). However, one of the steps was too complicated and I did not know how to improve it.

In June, Jeremy Weissmann read my proof and he proposed a different development. His argument was well structured, but it wasn’t as goal-oriented as I’d hoped for. Gladly, after a brief discussion, we realised that we were missing a great opportunity to use the trading rule (details below)!

I was so pleased with the final outcome that I decided to record and share the new proof.

Problem statement

In graph theory, the degree of a vertex $A$, $\fapp{d}{A}$, is the number of edges incident with the vertex $A$, counting loops twice. So, considering Graph 0 below, we have $\fapp{d}{A}=3$, $\fapp{d}{B}=3$, $\fapp{d}{C}=1$, $\fapp{d}{D}=3$, and $\fapp{d}{E}=2$.

Example of an undirected graph with five vertices

Graph 0: Example of an undirected graph with five vertices

A well-known property is that every undirected graph contains an even number of vertices with odd degree. The result first appeared in Euler’s 1736 paper on the Seven Bridges of Königsberg and is also known as the handshaking lemma (that’s because another way of formulating the property is that the number of people that have shaken hands an odd number of times is even).

As we can easily verify, Graph 0 satisfies this property. There are four vertices with odd degree ($A$,$B$, $C$, and $D$), and 4, of course, is an even number.

Although the proof of this property is simple, all the conventional proofs that I know of are not goal-oriented. My goal is to show you a development of a goal-oriented proof. Also, my proof is completely guided by the shape of the formulae involved, which helps reducing the amount of guessing involved.

Continue reading

Related Posts:

Principles and Applications of Algorithmic Problem Solving

I am currently in Salamanca (Spain), attending the conference Tools for Teaching Logic III. My talk was on teaching logic through algorithmic problem solving and it went quite well, I think. In particular, it seems that the audience enjoyed the examples that I have used and the teaching scenarios that I have shown. As a result, I have promised that I would upload my PhD thesis into this website. Since the thesis can also be useful for other people, I have decided to write a new blog post. I hope you enjoy!

Abstract

Algorithmic problem solving provides a radically new way of approaching and solving problems in general by using the advances that have been made in the basic principles of correct-by-construction algorithm design. The aim of this thesis is to provide educational material that shows how these advances can be used to support the teaching of mathematics and computing.

We rewrite material on elementary number theory and we show how the focus on the algorithmic content of the theory allows the systematisation of existing proofs and, more importantly, the construction of new knowledge in a practical and elegant way. For example, based on Euclid’s algorithm, we derive a new and efficient algorithm to enumerate the positive rational numbers in two different ways, and we develop a new and constructive proof of the two-squares theorem.

Because the teaching of any subject can only be effective if the teacher has access to abundant and sufficiently varied educational material, we also include a catalogue of teaching scenarios. Teaching scenarios are fully worked out solutions to algorithmic problems together with detailed guidelines on the principles captured by the problem, how the problem is tackled, and how it is solved. Most of the scenarios have a recreational flavour and are designed to promote self-discovery by the students.

Based on the material developed, we are convinced that goal-oriented, calculational algorithmic skills can be used to enrich and reinvigorate the teaching of mathematics and computing.

Download the PDF

Principles and Applications of Algorithmic Problem Solving (PhD Thesis, João F. Ferreira, 345 pages)

Related Posts:

Sir Tony Hoare on the future of Computing Science

Sir Tony Hoare on the future of Computing Science (CACM, March 2009):

I expect the future to be as wonderful as the past has been. There’s still an enormous amount of interesting work to do. As far as the fundamental science is concerned, we still certainly do not know how to prove programs correct. We need a lot of steady progress in this area, which one can foresee, and a lot of breakthroughs where people suddenly find there’s a simple way to do something that everybody hitherto has thought to be far too difficult.

Related Posts:

A Calculational Proof of the Handshaking Lemma

UPDATE (2011/09/20): This post was superseded by An improved proof of the handshaking lemma.

In graph theory, the degree of a vertex $A$, $\fapp{d}{A}$, is the number of edges incident with the vertex $A$, counting loops twice. So, considering Graph 0 below, we have $\fapp{d}{A}=3$, $\fapp{d}{B}=3$, $\fapp{d}{C}=1$, $\fapp{d}{D}=3$, and $\fapp{d}{E}=2$.

Example of an undirected graph with five nodes

Graph 0: Example of an undirected graph with five nodes

A well-known property is that every undirected graph contains an even number of vertices with odd degree. The result first appeared in Euler’s 1736 paper on the Seven Bridges of Königsberg and is also known as the handshaking lemma (that’s because another way of formulating the property is that the number of people that have shaken hands an odd number of times is even).

As we can easily verify, Graph 0 satisfies this property. There are four vertices with odd degree ($A$,$B$, $C$, and $D$), and 4, of course, is an even number.

Although the proof of this property is simple, I have never seen it proved in a calculational and goal-oriented way. My aim with this post is to show you a development of a goal-oriented proof.
Continue reading

Related Posts: