Four Color Theorem Verified in Coq

Georges Gonthier (MS Research, Cambridge) has a paper up entitled “A computer-checked proof of the Four Colour Theorem.” The original proof of the theorem by Appel and Haken relied on computer programs checking a very large number of cases, and raised some important conceptual and philosophical issues (see Tymoczko, “The four-color theorem and its philosophical significance,” Journal of Philosophy 76 (1979) 57-83 and reprinted in his collection New Directions in the Philosophy of Mathematics). The new work has formalized a more recent version of the proof and verified it in the proof checker Coq. Here’s how Gonthier describes the contribution this is making:

Our work can be seen as an ultimate step in this clarification effort, completely removing the two weakest links of the proof: the manual verification of combinatorial arguments, and the manual verification that custom computer programs correctly fill in parts of those arguments. To achieve this, we have written a formal proof script that covers both the mathematical and computational parts of the proof. We have run this script through the Coq proof checking system [13,9], which mechanically verified its correctness in all respects. Hence, even though the correctness of our proof still depends on the correct operation of several computer hardware and software components (the processor, its operating system, the Coq proof checker, and the Ocaml compiler that compiled it), none of these components are specific to the proof of the Four Colour Theorem. All of them come off-the-shelf, fulfill a more general purpose, and can be (and are) tested extensively on numerous other jobs, probably much more than the mind of an individual mathematician reviewing a proof manuscript could ever be. In addition, the most specific component we use the Coq system, to which the script is tuned can output a proof witness, i.e., a longhand detailed description of the chain of formal logical steps that was used in the proof. This witness can, in principle, be checked independently (technically, it is a term in a higher-order lambda calculus). Because this witness records only logical steps, and not computation steps, its size remains reasonable, despite the large amount of computation needed for actually checking the proof.

Formalizing and verifying theorems (by computer) seems to be a hot topic, and might raise interesting questions for the philosophy of mathematics; see Jeremy Avigad’s work on formalizing mathematics in Isabelle.

(Via Lambda the Ultimate)

UPDATE: More links here and see also Brian’s post.

Course on Logical Positivism

I committed to teach a course on Logical Positivism next year, and I have to figure out which books I should order. Here’s a list; if you have any comments or ideas, please let me know.

Thats approx. 80 bucks. Plus some copies of Mach and Hilbert on geometry, passages from the Tractatus, Carnap and Quine on logical truth and convention, Two Dogmas, stuff like that. Sarkar, Logical Empiricism at Its Peak: Schlick, Carnap, and Neurath might be a good resource, but too expensive to make a required text.

Motivating Intro Logic for Philosophy majors (and others)

Lillian sent me an email today about the APA Session on Logic Instruction where she asked:

Was there any discussion about incorporating philosophical issues in logic @ the intro course level? I’m teaching a logic for philosophers course this semester. Most of my students haven’t had any formal logic, so I’m teaching it like an intro to philosophy course. Now, I’m thinking one should bring in the philosophical issues behind the formal stuff to make an intro course fun and interesting. That would be one reason to teach grad students this material.

There was some discussion here regarding an idea Branden brought up in the discussion; Gillian suggested in the comments that this idea might also work for intro courses, and Marc pointed out that Hughes’ Philosophical Companion to First-Order Logic has some stuff relevant to the philosophical underpinnings of things you might teach in an intro course. The book that Lillian uses (Stephen Read, Thinking about Logic: An Introduction to the Philosophy of Logic) is a good source as well. It’s another question entirely how to motivate intro logic for CS majors. A good place to start is “On the Unusual Effectiveness of Logic in Computer Science,” by Halpern, Harper, Immerman, Kolaitis, Vardi, and Vianu. It outlines the uses of logic in descriptive complexity theory, database query languages, type-theory and programming languages, reasoning about knowledge, and circuit verification. For math majors, I don’t know anything quite so nice and compact. Make them read the Principia?

Inference vs. Implication

Gillian linked* to a paper by Gil Harman and Sanjeev Kulkarni, which contains this nice explanation of the distiction between inference (reasoning) and implication (what follows from what):

A related problem with the traditional picture is its treatment of deductive principles like (D) as rules of inference. In fact they are rules of about what follows from what. Recall what (D) says:

(D) From premises of the form “all F are G” and “a is F” the corresponding conclusion of the form “a is G” follows.

(D) says that a certain conclusion follows from certain premises. It is not a rule of inference. It does not say, for example, that if you believe “All F are G” and also believe “a is F” you may or must infer “a is G.” That putative rule of inference is not generally correct, whereas the rule about what follows from what holds necessarily and universally. The alleged rule of inference is not generally correct because, for example, you might already believe “a is not G” or have good reason to believe it. In that case, it is not generally true that you may or must also infer and come to believe “a is G.

Perhaps you should instead stop believing “All F are G” or “a is F.” Perhaps you should put all your energy into trying to figure out the best response to this problem, which may involve getting more data. Or perhaps you should go have lunch and work out how to resolve this problem later!

From inconsistent beliefs, everything follows. But it is not the case that from inconsistent beliefs you can infer everything.

Deductive logic is a theory of what follows from what, not a theory of reasoning. It is a theory of deductive consequence. Deductive rules like (D) are absolutely universal rules, not default rules, they apply to any subject matter at all, and are not specifically principles about a certain process. Principles of reasoning are specifically principles about a particular process, namely reasoning. If there is a principle of reasoning that corresponds to (D), it holds only as a default principle, other things being equal.

Another thing to be careful about in logic class. It took a while to train myself to avoid pronouncing “pq” as “p implies q,” which is a very common thing to do in math/CS logic circles. I’m now very careful to distinguish the conditional from implication, and try to get my students to do the same.

* Gillian’s post happened a while ago, I know. I’m slow. Do go and read it and the comments.

Logic Instruction and Philosophy Graduate Training

I’ve put up materials from the panel discussion on Logic in Philosophy Graduate Training at the ASL Spring Meeting, which featured Michael Glanzberg, Ted Sider, and Brian Weatherson, and which Andy Arana and I organized. The materials include slides for Michael’s and my talks, notes for Ted’s talk, and Andy’s paper, as well as MP3’s of the talks. I didn’t record Andy’s, since he read his paper and it’s available online, and I cut out the discussion since most of it was inaudible.

If you have any comments, queries, suggestions, etc., to contribute to the discussion, please leave a comment here.

(Geek note: talks recorded on an iPod with the Griffin iTalk, post production using Audacity).

Modal Logic Textbooks

I’m scheduled to teach a course on modal logic in the Fall. So I’ll have to think about a textbook choice pretty soon. Last time I’ve used Fitting and Mendelsohn’s First-order Modal Logic (Kluwer, 1999), which I quite like. It’s accessible, which is important, since many of the students will be philosophy majors with little formal background beyond an introductory logic course. Fitting and Mendelsohn include a bunch of philosophical material, and, as the title indicates, focus on first-order logics. So you get into a lot of interesting material about possibilism versus actualism, you get to discuss abstraction (which is important for intensional semantics), and also non-alethic logics (deontic, epistemic, time), although not in as much depth as I’d like. Proofs and metatheory are done via trees. But it’s not terribly interesting for computer science students, who also make up a good chunk of the audience. So something like Blackburn, de Rijke, and Venema’s Modal Logic (Cambridge, 2002) would be more interesting to them (and me, I guess), but is probably too technical. Chellas’s Modal Logic (Cambridge, 1980) is nice, but probably also too technical, a little outdated, and doesn’t cover first-order systems. Hughes and Cresswell’s New Introduction to Modal Logic (Routledge, 1996), like Chellas’s book, does everything Hilbert-style (my students might kill me if I make them do exercises in that), and doesn’t have a lot of discussion of applications (philosophical or computer science). Plus, I prefer boxes and diamonds to L and M. Beall and van Fraassen’s Possibilities and Paradox (Oxford, 2003) and Priest’s Introduction to Non-Classical Logic (Cambridge, 2001) don’t cover enough modal logic for my purposes (e.g., no first-order logic). Girle’s Modal Logic and Philosophy (McGill-Queens, 2000) might be interesting, but I haven’t looked at it. He does discuss many applications of modal logic in philosophy, but I don’t know how in-depth. Anyone used it? Other ideas?

UPDATE: Two more textbooks worth noting: Chagrov and Zakharyaschev’s Modal Logic, and Bell, DeVidi and Solomon, Logical Options. As I said in the comments, the former may be somewhat expensive. The latter is not only affordable, but covers non-standard logics more broadly (second order, modal, intuitionistic, and many-valued logics).

Logic in Montego Bay

This year’s LPAR will be held in Montego Bay, Jamaica–in early December. I missed the meetings in Havana and Reunion (Had papers and didn’t go! What was I thinking?) so it’s probably time to put on my computer science hat and write something.