Ok, by popular demand, here’s a list of the books in the new banner image:

Ramsey, The Foundations of Mathematics
Hilbert and Bernays, Grundlagen der Mathematik I & II (2nd ed)
Carnap, Logical Syntax of Language
Kneale and Kneale, The Development of Logic
Tarski, Einführung in die mathematische Logik
Russell, Introduction to Mathematical Philosophy
Russell, Logic and Knowledge
Boolos, Logic, Logic, and Logic
Peano, Selected Works
Frege, The Basic Laws of Arithmetic
Gödel, Collected Works I
Dummett, Elements of Intuitionism
van Heijenoort, From Frege to Gödel
Whitehead and Russell, Principia Mathematica I
Feferman, In the Light of Logic
Shoenfield, Mathematical Logic
Kleene, Introduction to Metamathematics
Girard, Proofs and Types
Fraenkel, Einleitung in die Mengenlehre, 2nd ed.
Hilbert and Ackermann, Einführung in die theoretische Logik (1st ed)
Lewis, Parts of Classes
Mancosu, From Brouwer to Hilbert
Gentzen, Collected Papers
Wittgenstein, Tractatus
Herbrand, Logical Writings
Quine, The Ways of Paradox

Selection and order was dictated in part by the color of the spine, so you shouldn’t really draw any conclusions from the fact that some books/authors are included and others aren’t. And just in case you were wondering, I do have the other volumes of Gödel’s works and PM.

Changes II

Ok, it looks like the move worked. Please let me know if you notice anything broken. And, if you’re reading this on a feed reader, check out the new site design for a second.


The University of Calgary is moving its websites to a Content Management System (Drupal, to be specific). My homepage is scheduled to be migrated tonight. Now, I’ve tried very hard to not break any URLs or links (the IT people probably hate me by now), but there will be some changes. For instance, all the PDFs of my papers will be in But maybe something goes wrong, and my site and LogBlog won’t be accessible tomorrow. If that happens, rest assured that I will do my best to fix it ASAP.

TYPES Summer School 2007

TYPES Summer School 2007
Proofs of Programs and Formalisation of Mathematics

August 19-31 2007, Bertinoro, Italy

During the last ten years major achievements have been made in using computers for interactive proof developments to produce secure software and to show interesting mathematical results. Recent major results are, for instance, the complete formalisation of a proof of the four colour theorem, and a formalisation of the prime number theorem.

The summer school is a two weeks’ course for postgraduate students, researchers and industrials who want to learn about interactive proof development. The present school follows the format of previous TYPES summer school (in Baastad 1993, Giens 1999, Giens 2002 and Goteborg 2005). There will be introductory and advanced lectures on lambda calculus, type theory, logical frameworks, program extraction, proof carrying code, formal topology and models, with relevant theoretical background. Several talks will be devoted to applications.

During the two weeks, participants will get extensive opportunities to use and compare most of the current tools for the automation of formal reasoning, comprising Agda, Coq, Epigram, Matita, Mizar and Isabelle/Isar.

The school is organised by the TYPES working group “Types for Proofs and Programs”, which is a project in the IST (Information Society Technologies) program of the European Union. A limited number of grants covering part of travel, fees and ackommodation are available. Neither participation nor grants are restricted to TYPES participants.


A large amount of money is available to offer travel grants. To apply for a grant you must provide a recommendation letter and a CV or a similar short description of yourself. All information/documentation concerning a grant applications must reach us by June 4.

Both the recommendation letter and the CV must be sent to Please use the subject: “grant application”. The recommendation letter must be sent to us directly by the person that writes it. We will confirm by email each CV and recommendation letter we receive.

Important dates and figures

  • June 4: deadline for grant applications (travel only).
  • June 25: deadline for inscription
    • With double room accomodation: 1100 Euros.
    • With single room accomodation: 1300 Euros.
    • The fee is all inclusive (accomodation, meals, school participation fees, and social activities).

Confirmed Lecturers

Andrea Asperti, Bologna
Stefano Berardi, Torino
Thierry Coquand, Chalmers
Jean-Christophe Fillitre, Paris Sud
Herman Geuvers, Nijmegen
Benjamin Gregoire, INRIA Sophia
Tobias Nipkow, TU Munich
Christine Paulin-Mohring, Paris Sud
Giovanni Sambin, Padova
Andrzej Trybulek, Bialystok
Markus Wenzel, TU Munich


Introduction to Type Theory:
Inductive sets and families of sets
Predicative and non-predicative theories
Model Theory

Introduction to Systems:

Advanced topics:
Program extraction
Proving properties of Java programs
Reasoning about Programming Languages
Proof Carrying Code
Dependently typed programming languages
Formal Topology


Andrea Asperti, Claudio Sacerdoti Coen, Enrico Tassi

Any question concerning the school may be sent to

Paul Cohen, 1934-2007

Paul Cohen died on Friday of a rare lung disease. This came over FOM today:

We are very sorry to tell you that Paul Cohen has suddenly passed away.

He has had a rare lung disease for maybe two years now, but symptoms only began to really manifest about a year ago. We did not know that the disease had progressed nearly as much as it clearly had.

On Monday Paul had a bad attack and was taken to the emergency room, and we were told then that the situation was very grave. But after receiving medication he stabilized and seemed fine and was actually going to be released this Friday morning. But Thursday morning his lungs failed and he became unconscious and did not awaken. So this whole thing has been a total shock to us (twice).

Overall he had not been in pain at all and was only on relatively low levels of oxygen. Just this Sunday he and my mother went out to dinner and the movie theater. And on Wednesday night when we last saw him conscious he was happy and completely alert.

There will most likely be a small service for friends and family and then a larger one afterwards hosted by the Stanford math department. As of now we have not made definite plans

Philosophy Spin-offs

Mark Lance posted this insightful message to FOM yesterday, in response to this thread on “progress in philosophy”:

“The aim of philosophy, abstractly formulated, is to understand how things in the broadest possible sense of the term hang together in the broadest possible sense of the term. Under “things in the broadest possible sense” I include such radically different items as not only ‘cabbages and kings’, but numbers and duties, possibilities and finger snaps, aesthetic experience and death. To achieve success in philosophy would be, to use a contemporary turn of phrase, to ‘know one’s way around’ with respect to all these things, not in that unreflective way in which the centipede of the story knew its way around before it faced the question, ‘how do I walk’, but in that reflective way which means that no intellectual holds are barred.”

Wilfrid Sellars (“Philosophy and the Scientific Image of Man“)

Sellars, I think, is basically correct. Philosophy seeks understanding in the broadest sense. As such it is the generator of new ways of thinking, new things to think about, new ideas about what goes in various regions of reality, and how regions relate. When something gets well enough developed philosophically that it amounts to a detailed substantive view of something, of some region of everything, others who are not interested in the synoptic vision take this specific bit up and run with it. Philosophers let them, happily, and move on to what remains obscure, speculative, or just hard. (And then smile to themselves when technicians make snarky comments about the lack of precision in philosophical thinking about undeveloped and previously undreamt of connections.)

Progress in philosophy? Here are a few inventions: democratic theory, political science generally, sociology, logic, cognitive science, psychology generally, natural science, physics in particular, decision theory, linguistics, …

More or less everything — interestingly with the possible, and arguable, exception of non-foundational mathematics.

The interesting question here is what the next big spin-off will be. (I have a couple guesses, but that’s for a book more than a post.)

Any guesses from readers? (And: where do we get the venture capital?)

Icosidodecahedral prismatohexacosihecatonicosachoron

Alasdair Urquhart was nice enough to identify the model that’s dominating the lounge at BIRS. It’s an icosidodecahedral prismatohexacosihecatonicosachoron, and is made of 120 icosidodecahedra, 600 cuboctahedra, 720 pentagonal prisms, its faces are 3600 triangles, 3600 squares, 1440 pentagons, and it has 10,800 edges. I’m sure it’s got something to do with E8 (the mapping of which was announced yesterday) but I have no idea what.

Species/the Reasoner

My colleague Marc has updated his SEP entry on Species. Jon Willimason is starting a new online thing called The Reasoner.

The Reasoner is a monthly digest highlighting exciting new research on reasoning and interesting new arguments. It is interdisciplinary, covering research in, e.g., philosophy, logic, AI, statistics, cognitive science, law, psychology, mathematics and the sciences.

The Reasoner welcomes submissions:

  • Submitted articles should concern some exciting new research on reasoning, or an interesting new argument (concerning anything), or a new perspective on a topic or historical figure connected with reasoning. Submissions should be 100-1000 words, should be comprehensible and of interest to those in other disciplines, and should be positive in outlook. Any mathematical symbols should be formatted using LaTeX.
  • Submitted items of news can be of any length, though shorter pieces are more likely to be published.
  • Conference announcements should be kept brief, and should include a title, dates, location and url.

Submissions should be sent to The deadline for text is 15th of each month, to appear in the subsequent edition to be released on the 1st of the following month. All publication decisions will be taken by the editorial team. The editorial team reserves the right to edit submissions before publication. The copyright of each submission belongs to its author.

Hey, 100 words. That shouldn’t be too hard. Deadline for #1 is April 15. He writes, by way of clarification,

Articles can be on anything connected to reasoning, but need to be of interest and understandable to an interdisciplinary audience, so not too technical and not too focussed on minutiae. For example an article might report on an interesting new line of work (providing links to the papers), might give an interview with someone working on reasoning, or might report back from a conference. The aim of the gazette is to increase awareness of what is going on in this area.