(where A, B, C are propositional formulas and C(A) means C with the variable X replaced everywhere by A). Add this to a complete Hilbert-type system for propositional logic, and you can prove all propositional tautologies with n variables in number of steps linear in n. Without Eq, you can’t do this.

• Matthias Baaz and Richard Zach, Short proofs of tautologies using the schema of equivalence. Computer Science Logic. 7th Workshop, CSL’93. Swansea. Selected Papers (Springer, Berlin, 1994) 33-35

Can you help the ASL Committee on Logic Education? Please take this survey.

Dear Members of the ASL,

One of the responsibilities of the ASL Education Committee is to help its membership tackle pedagogical difficulties in teaching logic courses. In order to properly do this, we need to fully understand the goals such courses are intended to achieve. The focus of a logic class can be very different depending on whether it is in a mathematics, philosophy, or computer science department.

Logic courses in philosophy departments pose a particular challenge because they have so much variability – both in audience and in focus. In order that we may better understand them, Wilfried Sieg of Carnegie Mellon has developed an online survey regarding introductory logic classes. This survey may be accessed at

http://logic.lrdc.pitt.edu/

If you teach such a class, I ask that you take the time to fill this survey out. Furthermore, if you have colleagues who teach such classes but are not members of the ASL, please forward this information on to them. Any information that we gather will help us serve our membership better.

Thank you for your attention.

Yours truly,
Walker White
Chair, ASL Committee on Education

Peter and Ole were faster than me, so I’ll just link to their posts:

Peter Smith on Mathematical Logic by Chiswell and Hodges and The Mathematics of Logic by Kaye.

Ole Thomassen Hjortland on Logic’s Lost Genius: The Life of Gerhardt Gentzen by Mentzler-Trott.

Below the funding statistics for grants in the Philosophy Committee for SSHRC Standard Research Grants. The explanation for why so few grants were awarded this year is pretty clear: rather than cut grants across the board, SSHRC decided to respond to the 23% cut in overall funding for the program over last year by making fewer awards. The overall success rate for all SRG’s is down to 33% from last year’s 40%. So it’s not just philosophy that has suffered.

EDIT: This is the result of an overall $2m cut to SSHRC’s budget at the hands of the Conservative government in the Fall of 2006. Thanks, Mr. Harper! Actually, it looks like SSHRC decided to cut the pie differently and spend less of its $90m budget for research grants on SRGs and the rest on–what? Also, see this post.

The Social Sciences and Humanities Research Council of Canada has posted a list of new Standard Research Grants for 2007. (Last year’s projects were discussed here.) This year’s stats: 88 applications (2006: 85, 2005: 96, 2004: 92), 26 grants, for a success rate of 29% (2006: 37%, 2005: 38%, 2004: 48%). This year, new scholars (≤ 5 years beyond PhD) had a success rate of only 22% (2006: 29%, 2005: 38%, 2004: 29%). Full stats here.

If someone knowledgeable about SSHRC funding policies, procedures, and politics reads this, I would be really interested to know why the success rate has been declining so sharply–it’s gotten almost twice as hard to get a project compared with 3 years ago! And contrary to what they said in their big SSHRC Transformation report they hdon’t seem to have increased funding to new researchers. But maybe just in philosophy?

An incomplete list of successful SRG proposals follows. I’ve included the total dollar figures over the 3-year duration of the grants (in CAD), but these shouldn’t be taken as an indication of the quality of the project. The funding rate depends on the requirements of the project (travel, research support) and on the amount of graduate student funding, not just on the ranking of the proposal. One may guess that the biggest awards (over $70,000) include Research Time Stipends, i.e., teaching relief, which is very hard to get. The grants aren’t broken down by specialty or department in the full (71-page) list, so I had to guess the philosophy projects from the titles and/or researchers. Please email me or comment if you notice an omission.

1. Berryman, Sylvia A., The University of British Columbia. The philosophical reception of mechanics in ancient Greece. $41,000
2. Dyzenhaus, David L., University of Toronto. The rule of law in the new normal. $24,398
3. Demopoulos, William G., The University of Western Ontario. Methodological and metaphysical aspects of the applicability of mathematics. $83,375
4. Ereshefsky, Marc F., University of Calgary. A Philosophical study of biological homology. $74,103
5. Hellie, Benjamin, University of Toronto. The slightest philosophy. $38,350
6. Larivée, Annie, Brock University. Vers une éthique du souci de soi : réappropriation contemporaine d’un concept philosophique ancien. $45,990
7. Marion, Mathieu, Université du Québec à Montréal. Fondements philosophiques de la sémantique des jeux : rationalité et connaissance. $44,638
8. Matthen, Mohan P., University of Toronto. How we see things. $101,300
9. Morton, Adam, University of Alberta. Intellectual virtues of limitation-management $66,546
10. Myrvold, Wayne C. and Harper, William L., The University of Western Ontario. Scientific inference: enriching the probabilistic framework. $54,608
11. Nadeau, Robert, Université du Québec à Montréal. Économie et connaissance : sur l’épistémologie de Friedrich Hayek. $53,671
12. Parsons, Glenn G., Ryerson University. A philosophical study of human beauty. $19,260
13. Piché, Claude, Université de Montréal. Kant et Reinhold, la portée philosophique de deux conceptions divergentes des lumières. $49,700
14. Piché, David, Université de Montréal. La théorie de la connaissance d’Hervé de Nédellec : édition critique de Quodlibeta, traduction et étude historico-philosophique. $71,924
15. Schlimm, Dirk and Hallett, Michael, McGill University. Geometry and logic from Pasch to Hilbert. $54,280
16. Weisberg, Jonathan J., University of Toronto. Synthesizing formal epistemologies. $33,825
17. Wilson, Jessica M., University of Toronto. Hume’s Dictum and the causal connection. $31,400
18. Yi, Byeong-Uk, University of Toronto. Plurals: their logic and semantics. $61,570
19. Weinstein, Steven, University of Waterloo. Multiple time dimensions. $49,615

Two out of the five new Strategic Research Clusters are philosophy-related: “Clustering the humanist and social studies of science in Canada” includes Canadian philosophy/ers of science, and the “Canadian business ethics research network” is, well, applied ethics.

The Natural Sciences and Engineering Research Council of Canada also sometimes funds research projects by philosophers. This year there are (at least) two new 5-year discovery grants (with per-year figures) to people in philosophy departments:

1. Pelletier, F. Jeffry, Simon Fraser University. Inference: Theories and computation. $34,000
2. Zach, Richard, University of Calgary. Computational aspects of the epsilon calculus. $14,000

John Carpenter’s Dark Star is a masterpiece!

[youtube=http://www.youtube.com/watch?v=qjGRySVyTDk]

New and improved SEP entry on dynamic logic by Philippe Balbiani is now up.

Skolemization is the familiar procedure by which you replace strong quantifiers in a formula by function symbols in such a way that A is provable iff A^S is provable. This doesn’t work in intuitionistic logic: the “only if” works, but the “if” doesn’t. E.g., ¬¬(A(c) ∨ ¬ A(c)) is provable intuitionistically, but not ¬¬(∀x)(A(x) ∨ ¬ A(x)). (If you also have =, it doesn’t even work for prenex formulas.) Rosalie Iemhoff is reporting on joint work with Matthias Baaz on new results on how to get Skolemization to work in constructive extensions of intuitionistic logic. The key is to add an existence predicate to intuitionistic (a logic proposed by Dana Scott¹). Rosalie and Matthias showed that there’s a way to Skolemize strong existential quantifiers in this system.² Now they have some ideas on how to also deal with strong universal quantifiers.

¹ Dana S. Scott, Identity and existence in intuitionistic logic. In: Fourman et al., (ed.), Applications of Sheaves , LNM 753 (Springer, 1979) 660–696.
² Matthias Baaz and Rosalie Iemhoff. On the Skolemization of existential quantifiers in intuitionistic logic. Annals of Pure and Applied Logic 142 (2006) 269-295.

I’m at the Moscow-Vienna Workshop on Logic and Computation. We’re on the second day. Yesterday was started off with a way-over-my-head talk by Sergei Adian on his and Novikov’s solution to the Burnside problem. Today, Michel Parigot just gave a very interesting talk on a constructive, but classical proof system. His aim is to develop a system in which you can reason classically but still have nice properties like the disjunction property and the witness property. Of course, you don’t have those in general. So the aim is to have a classical proof system in which you have constructive disjunction and existential quantifiers as well. Then you can get the properties you’re looking for: if you can prove A ∨ B (where ∨ is constructive), then you have a constructive classical proof, and you either get a proof of A or a proof of B. I’m looking forward to the paper.

Now I’ll have to pay attention to Lev Beklemishev talking about provability logic.