A while back, a number of us had the thought that we ought to do something in Cambridge to mark the centenary of Principia. But organizing blockbuster conferences is always a real pain; and to hold them here you need arrange everything years in advance; and in any case, to be frank, big conferences are very often just not worth the effort. So we thought, well, let’s perhaps organize something small and relatively informal nearer the time. Then time passed and the centenary date got nearer. And more time passed. And in fact the occasion would in the end have gone unmarked, except that Nik Sultana — a grad student in Comp. Sci.– took up the idea late in the day and made it all happen. All credit to him. Here’s the programme, some abstracts, and links to some short papers.
Given Nik’s roots in computer science, there was a somewhat different spin to this symposium than it would have had if organized just by a logic-minded philosopher or a philosophy-minded logician. Though, truth to tell, I’m not sure I learnt a great deal from the comp. sci. orientated talks. Formal proof checkers are developing apace, and this work on formal proofs is beginning to impact on ‘mainstream’ mathematics. But I basically knew that, though I got to hear about a few interesting details.
Three random thoughts. (1) When people talk about “type theories” they tend to really mean theories-with-type-disciplines or theories-about-theories-with-type-disciplines: I wonder why “typed theories” didn’t catch on? Anyway I do plan though to go off and have a look at the history of type theories co-written by Fairouz Kamareddine, from which Fairouz extracted a lighting tour for the symposium. (2) Like others who have learnt from Great Uncle Frege, I did find the wobbling between talk of functions and talk of expressions-for-functions by some people rather uncomfortable. (3) [Arising from some responses to Byeong-uk Yi’s talk], people are typically really unhappy with the idea that plural terms might refer, plurally, to several things rather than being disguised singular reference to a set: singularist prejudice goes deep.
The paper I enjoyed most, though, was my colleague Michael Potter’s talk about two ideas of ambiguity in Principia — the idea of “real” (i.e. unbound) variables as being ambiguous or variable names, and the idea of (most) “theorems” of PM in fact being type-ambiguous. The first evidences a step back from Frege’s clarity about the role of “variables” as anaphoric pronouns. The second has the authors of Principia struggling towards the idea of using schemas in the modern sense. Michael had some interesting quotes from correspondence between Whitehead and Russell, in which Whitehead is pressing towards the idea of a generalization using a metalanguistic schema, in using which you stand outside the given formalized language, and Russell (more wedded to a logical monism?) resisting. This was interesting stuff, with some nice historical detail, and I hope Michael works it up further.