Georg Moser and I finally got our paper done for the Studia Logica special issue on cut elimination. It’s on the complexity of the epsilon elimination procedure in the first epsilon theorem. (If you don’t know what the epsilon theorem or the epsilon calculus is, see here.) It’s a consequence of the cut-elimination theorem that if you can prove an existential sentence ∃x A(x) then you can prove a disjunction A(t₁) ∨ … ∨ A(t_n). Moreover, the length and cut-rank of the proof of ∃x A(x) gives a bound on n, which is hyperexponential. Orevkov and Statman showed that this bound is optimal. The first epsilon theorem is like the cut-elimination theorem, just for the epsilon calculus, in that it also yields the above version of (one direction of) Herbrand’s Theorem. We show that it has essentially the same upper and lower bounds. Our paper is also the only place, I believe, were you can find Bernays’ original proof of the first epsilon theorem in English.

The paper is up at arxiv.

Via the PT list, I hear about a new open-access, online journal on computational logic, entitled Logical Methods in Computer Science. It’s run by Dana Scott, Gordon Plotkin, Moshe Vardi, and Jirí Adamek. In addition to regular papers, they will publish special issuse, e.g., containing selected papers from LICS. Here’s the email they sent advertising it:

Dear Colleague:

We are writing to inform you about the progress of the open-access, online journal “Logical Methods in Computer Science,” which has recently benefited from a freshly designed web site, see:

http://www.lmcs-online.org

In the first year of its existence, the journal received 75 submissions: 21 were accepted and 22 declined (the rest are still in the editorial process). The first issue is complete, and we anticipate that will be three in all by the end of the calendar year. Our eventual aim is to publish four issues per year. We also publish Special Issues: to date, three are in progress, devoted to selected papers from LICS 2004, CAV 2005 and LICS 2005.

The average turn-around from submission to publication has been 7 months. This comprises a thorough refereeing and revision process: every submission is refereed in the normal way by two or more referees, who apply high standards of quality.

We would encourage you to submit your best papers to Logical Methods in Computer Science, and to encourage your colleagues to do so too. There is a flier and a leaflet containing basic information about the new journal on the homepage; we would appreciate your posting and distributing them, or otherwise publicising the journal. We would also appreciate any suggestions you may have on how we may improve the journal.

Yours Sincerely,

Dana S. Scott (editor-in-chief)
Gordon D. Plotkin and Moshe Y. Vardi (managing editors)
Jiri Adamek (executive editor)

If you’re not on our mailing list:

The Department of Philosophy at the University of Calgary is pleased to announce a

Minisymposium on Logic

All talks will take place in 1253 Social Sciences Building

***

Friday, November 4, 4:00 pm

Alasdair Urquhart
University of Toronto

The Unnameable

Frege has a puzzling doctrine that functions are unsaturated entities. This paper is devoted to an attempted elucidation of the dark and mysterious metaphors surrounding this doctrine. I advocate a minimalistic interpretation of Frege’s doctrine, namely that unsaturated things are entities of higher type, no more, no less. Further aspects of the Fregean doctrine, particularly those which give a stronger reading to the notion of incomplete entities, are rejected as irrelevant excrescences. In particular, the idea that functions are unnameable is consigned to the flames as both unnecessary and incoherent.

***

Saturday, November 5, 10:00 am

John P. Burgess
Princeton University

Nominal Essence and Verbal Necessity

Some views of Peter Geach on proper names will be examined, partially defended against the criticisms of Saul Kripke, and applied in an attempt to demystify metaphysical modality.

***

Saturday, November 5, 2:00 pm

Kit Fine
New York University

Variables, Knowledge and Semantics

I will talk about some connections between a nonstandard relational treatment of variables and the development of a more adequate semantics for proper names and quantified epistemic logic.

***

Prof. Urquhart has provided a copy of the paper his talk will be based on. Prof. Fine recommends his paper “The Role of Variables” (Journal of Philosophy 50 (2003) 605-631) as background reading. Both will be available in the Department’s reading room shortly.

Prof. Urquhart will also speak to the Calgary Peripatetic Research Group on Logic and Category Theory on Thursday, November 3, at 4:00 pm, on “Ideas and Problems in Resolution Theorem Proving”.

The Department of Philosophy and the Speakers Committee gratefully acknowledge the support of the Faculty of Humanities and the University of Calgary Research Grants Committee for these events.

www.phil.ucalgary.ca

Via Varia, I see that the French-Canadian journal Philosophiques is actually freely avaliable online since 1999. There are some online issues that are interesting for the logic/history of analytic/philosophy of math crowd, e.g., the special issue on Bolzano edited by Sandra Lapointe, and the issue on Poincaré’s epistemology (the latter includes a short piece by yours truly, although not on Poincaré).

Just came across the OpenChoice program of Springer Verlag:

Springer Open Choice gives you the power to choose how you want your research published. As an author-focused publishing company, Springer believes that authors should have the right to determine what publication model best meets their needs.

Springer Open Choice is exactly what it says: a choice. What works best for you? If free publication, supporting a pressure-free editorial process, and free online availability are important to you, then you need only submit your article to any Springer journal. Springer’s ‘green’ self-archiving policy lets authors post their own versions of their accepted article on an institution’s public server, and subscription-based publication ensures that authors all over the world have equal opportunity at publication and a peer review process free from commercial pressure.

If making the published version of your article freely available is your most important publication concern, then Springer Open Choice is the solution for you. Springer Open Choice makes the final, published version of the article available for free directly from SpringerLink. You still receive all the benefits of publication with Springer (see “Details” for a full listing), including print distribution, and your work will be available for free from Springer to anyone, anywhere in the world.

Sounds good. Let’s make the published version of my paper available for free to anyone. Oh, you say you’re going to charge me a whopping $3,000 for that? Never mind then. I’ll just take advantage of the ‘green’ self-archiving policy, thank you very much.

Why would anyone do that? And what is it with all that talk about commerical pressure on the peer review process? Is Springer going to only accept papers that they get enough copyright fee revenue from? Are they going to ditch their low-impact journals? What gives?

Varia is a French blog on philosophy, including a sizeable section on logic run by Mickaël Simon. There I found a link to Vann McGee‘s online lectures for his Logic I course at MIT, on the OpenCourseWare server.

M. Simon also pointed me to Théorème, a group blog run by a bunch of people from Paris (IHPST, Paris I as far as I can tell).

Skip this if you’re not interested in techie stuff; we’ll return to our regularly scheduled logic programming soon.

Yesterday I got some fancy new equipment: A Dell Optiplex GX620 desktop, with a stunning Dell 2405FPW 24″ screen. Then I was lucky enough to find a North American mirror which already had the brand-new SUSE Linux 10.0, released day before yesterday, and installed it. Went almost without a hitch (see below).

More specs: The thing is running on an Intel Pentium 4-640 (3.2 GHz, 2 MB L2 cache, and an 800 MHz front-side bus, and Extended Memory 64-bit Technology). That’s not anything super-fast, but plenty of computing power for me. It came loaded with 1 GB of RAM, a 160 GB harddrive, ATI Radeon 600SE video card with DVI connector, and a DVD-ROM and a DVD+/-RW drive.

To install SUSE 10.0, I downloaded the 64-bit version of the install DVD image (SUSE-10.0-EvalDVD-x86_64-GM.iso), burned it to a DVD, and started the install process. YaST recognized all the hardware without difficulty. Everything was set up in less than an hour. The only problem came when I booted for the first time, when the machine became unresponsive just after starting X. The screen goes blank like it’s making to switch from VGA to the fancy video driver, but then instead of a cursor it just stays blank and the system hangs. Seems the stock “radeon” driver for X.org doesn’t like my card or my monitor. So I installed the proprietary ATI driver.

If you’re reading this because you have the same problem and you’re wondering “How do I download the driver if I can’t even run Firefox?” then: (a) Boot in “Linux (failsafe)” mode to get a console. (b) Tell X to use the vesa driver instead of the radeon:

# sax2 -m 0=vesa

and save your new X configuration. Now you can start X (or reboot into graphical mode). (c) Then download the driver from the ATI website (fglrx64_6_8_0-8.16.20-1.x86_64.rpm). (d) Install the driver. (c) Tell sax to use it by starting it with

# sax2 -m 0=fglrx

I obviously haven’t tried it all out yet. The CompactFlash/Secure Digital/Memory Stick/SMC reader in the monitor works at least; Nautilus even automatically mounts it and asks me what I want to do with the photos from the digital camera! SUSE 10.0 comes with a bunch of new features that need exploring, such as Xen (a VM sorta like vmware, except it doesn’t do Windows, which is unfortunate, because if it did, I could finally run Language Proof and Logic software without having to reboot!) and Beagle (the Gnome version of Spotlight).

Two greats of German logic turned 60 not too long ago: Helmut Schwichtenberg in 2002 and Wolfram Pohlers in 2003. Both had birthday conferences held in their honor, and the proceedings thereof appear in the Annals of Pure and Applied Logic this year, the Schwichtenberg Festschrift in the May and the Pohlers Festschrift in the October issue. If proof theory is your thing, check out these issues—both are jam-packed with exciting papers on various topics, from explicit mathematics (Jäger and Strahm) to proof theoretic ordinals (Weiermann), from strong normalization in second-order natural deduction (Tatsuta and Mints) to complexity and propositional proof systems (Beckmann and Buss), epsilon substitution (Arai) to elementary arithmetic (Ostrin and Wainer), plus a bunch of computer-sciency logic by the likes of Stärk and Abramsky.