While everyone else is blogging from the NDC, I’m in Turin at the European Summer Meeting of the Association of Symbolic Logic, aka LC’04. Highlights so far: Grisha Mints’ opening talk on Monday, in which he presented a result showing that all intuitionistic Frege systems polynomially simulate each other. It uses some interesting recent work by Rosalie Iemhoff (Vienna), who showed that all intuitionistically admissible inference rules can be generated from a finite set of rules; Grisha’s result means that superexponential lower bounds on proof lengths for one intuitionistic Frege system extend to all others. Michael Möllerfeld presented his recent work on systems equivalent to Π12-CA. Π12-CA is the cutting edge of ordinal analysis (work of Rathjen and Arai). One of the systems Michael showed is equivalent to Π12-CA is the μ-calculus, which is a formalism with a fixpoint operator which is really important in theoretical computer science. Also interesting were the talks by Anton Setzer on extensions of Martin-Löf type theory, and by Andrea Cantini on constructive set theories with operators. Not much on the more philosophical side, but I should mention the talks by Phil Ehrlich on the pre-Robinson history of infinitesimals in mathematics (a long paper forthcoming in the Archive for the History of the Exact Sciences), by Luca Belotti on consistency of large cardinals, and the panel discussion on “Kant’s legacy for the philosophy of logic.” It was mostly on Kant, and not on the legacy. I wished there was more on Frege vis-a-vis Kant or something like that; in particular I thought it was a shame that no-one discussed John MacFarlane’s recent work on Kant and logic. Today is sight-seeing day, more proof theory tomorrow (as well as a talk by yours truly on Gödel logics). Oh, and thanks to Greg Restall for pointing to the beamer class a few weeks ago. They don’t have projectors here for the contributed talks, but as it turns out, beamer also makes very nice overhead transparencies. I recommend the “lined” template.