Logic and Formal Verification

This is home page was used to support the second week of the Carnegie Mellon Summer School in Logic and Formal Epistemology in the summer of 2007. Due to copyright restrictions, some of the materials are in a password protected directory.

Background on logic and axiomatic reasoning

For the session on formal verification, you may wish to review the basics of symbolic logic. Here are some good references:

• Barwise, Jon, and John Etchemendy, Language, Proof, and Logic. Amazon: html.
• Enderton, Herbert, A Mathematical Introduction to Logic. Amazon: html.
• Goldfarb, Warren, Deductive Logic. Amazon: html.

The following is a good introduction to axiomatic reasoning in mathematics:

• Stewart, Ian, and David Tall, The Foundations of Mathematics. Amazon: html.

Background on the Isabelle proof assistant

We will experiment with an interactive proof system called Isabelle.

• The Isabelle home page: html.
• The Isabelle documentation page: html.
• See especially the tutorial: pdf.

The Linux installation of Isabelle is quick and easy. Those of you who use Windows can try a live CD version: html.

We will use "Isabelle/HOL," an instantiation of higher-order logic. You can browse the library of theorems and definitions here:

• The Isabelle/HOL library: html.

I will do a good deal of "borrowing" from the course material page: html. See especially:

• The Isabelle/HOL exercises: html.
• The interactive course by Brucker et al.: html. Slides: html. Exercises: html.

Lecture notes

There are sketchy lecture notes for the first three topics: pdf.

Propositional logic

• See Sections 5.1-5.7 of the tutorial.
• See also the relevant lectures and exercises in the Brucker et al. course: pdf, pdf.
• An exercise involving the rules of propositional logic: pdf.
• An exercise on eliminationg connectives: pdf.

First-order logic with equality

• See Section 5.9 of the tutorial.
• See also the relevant lectures and exercises in the Brucker et al. course: pdf, pdf, pdf.
• An exercise using the quantifiers: pdf.
• An exercise, the "Rich Grandfather" riddle: pdf.

Induction and recursion on the natural numbers

• An excerpt from Stewart and Tall on the natural numbers: pdf.
• See Sections 2.5 and 3.5 of the tutorial.
• See also the relevant lecturesand exercises from the Brucker et al. course: pdf.
• An exercise involving powers and sums: pdf.
• An exercise involving "magical methods": pdf.

Interlude: formal verification and understanding

For a short, sweeping overview of the philosophy of mathematics, see

• Avigad, "Philosophy of Mathematics": pdf.

For a look a discussion of some new philosophical issues related to the use of computers in mathematics, see:

• Avigad, "Mathematical Method and Proof": pdf.
• Avigad, "Computers in mathematical inquiry": pdf.
• Avigad, "Understanding proofs": pdf.

The last of these adopts a Wittgensteinian perspective on the nature of mathematical understanding. See the following excerpt from the Philosophical Investigations:

• Wittgenstein on rule following: pdf.

Types and sets

• See the tutorial, and Brucker et al. lectures.

Inductively defined datatypes

• See the tutorial, and Brucker et al. lectures.

Decision procedures

• See the web page for a graduate level seminar: html.

Other information

• An overview of a formalization of the prime number theorem: pdf.
• A lecture for last year's summer school: pdf.
• A talk on decision and heuristic procedures for the real numbers: pdf.

Fun

Here are some fun logic puzzles:

• Excerpt from Smullyan, The Lady or the Tiger: pdf.