Logic and Formal Verification

This home page was used to support the second week of the Carnegie Mellon Summer School in Logic and Formal Epistemology in the summer of 2008. 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. And here is Henry's handy Isabelle "cheat sheet": 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.

Beyond the natural numbers

• Higher-order logic, simple type theory and set theory: see the tutorial, and Brucker et al. lectures.
• Inductively defined sets: see the tutorial, and Brucker et al. lectures.

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.

Interlude: decision procedures

• Yiannis Moschovakis' guest lecture, "Solving Equations in Algebra and Arithmetic": pdf.
• A graduate level seminar on decision procedures: html.
• A lecture for last year's summer school: pdf.

Interlude: an analysis of Euclidean diagrammatic reasoning

• A talk for philosophers and historians of mathematics: pdf.
• A talk for computer scientists: pdf.

Miscellaneous

• An overview of a formalization of the prime number theorem: pdf.
• References for proof theory: html.
• Some fun logic puzzles from Smullyan, The Lady or the Tiger: pdf.