Arché Gone Google

Google has been running a campaign called Gone Google where businesses, schools and organisations switch over to Google Apps, a free, web-based platform for communication and collaboration. The Arché Research Centre in St Andrews has started its move over to Google this semester, introducing Google Groups for different projects, Google Docs for minuting and research collaboration, and a shared Google Calendar for the centre's activity.

How does it make a difference?

(1) Google Calendar: Arché now has a new schedule online. The schedule is based on Google Calendar, and is synchronised with our own calendars. If I update the Arché calendar stream in my private Google Calendar (on my phone or my computer), the public Arché calendar is automatically updated and everyone subscribing to the Calendar stream has their private calendars updated as well. This makes for  a more efficient and accurate schedule. You can subscribe to both Google Calendar and iCal at the bottom of our Calendar page. If you don't need to see the Arché Calendar stream on a daily basis, you can deactivate it while seeing your other events. Note also that there are two different streams, one for weekly seminars, and one for events (e.g., workshops).

(2) Google Docs: Instead of the endless email exchanges with series of updated attachements, collaborative work - either research or admin - can be done in a shared document in Google Docs. It's perfect for writing seminar minutes of Arché's research projects, but also for writing papers together (at the same time) and commenting on papers. It's even got a LaTeX editor that can do a bit of basic logic, fractions, etc. (A more robust LaTeX options might be on its way as well.) Andrew Cullison writes on length about Google Docs for teaching purposes here. You can also share folders, using them for example as repositories for papers that a reading group is working through.

(3) Google Groups: Maybe this isn't universal, but we've had a hard time maintaining email lists on the university servers. Google Groups gives you an easy way to start and manage email lists without going through university bureaucracy. A typical problem with email lists is that one wants to include people without keeping names and addresses that are no longer valid or relevant. With Google Groups the admin is easy and can be shared between the researchers leading the project, seminar or reading group. You can also share documents through the Groups.

Hopefully, this is just the start. Soon we'll use Google Wave for collaborative research, integrating the above features in one interface.

New website

I've migrated over to the google site platform, and I've made a new website. I'll soon start uploading some work in progress. Fortunately, there is an Arché recess for two months in February and March, so I'll have the chance to write up some papers that have been overdue.

Workshop Report: Logic of Denial

Here is a short report from the 2nd FLC workshop on the Logic of Denial.

------

Workshop Report

The Logic of Denial, October 24th - 25th

2nd Foundations of Logical Consequence Workshop

FLC, The Foundations of Logical Consequence, is an AHRC-funded project run by the Arché Research Centre in the University of St Andrews. The four year project is currently in its second phase, The Structure of Logical Consequence. As part of the regular activity, FLC has just hosted its second workshop, entitled The Logic of Denial. 

Since Frege, the analysis of denial as assertion of a negation has been the received view in formal logic. However, recent literature has seen a number of attempts at introducing denial into formal systems as a primitive alongside assertion. The workshop invited its speakers to discuss how one best treats denial in a formal framework. In particular, how does denial correspond to different negations, and what is the relationship between logical consequence and rational demands imposed by the norms of assertion and denial?

The workshop's first day started with Dave Ripley (Institut Jean-Nicod, Paris) on  'Embedding Denial'. He discussed the strategy of introducing a primitive denial operator to address problems with expressive power in paracomplete and paraconsistent approaches to semantic paradoxes. Arguing from broader considerations about the nature of denial, he concludes that these theories ought to include a "complete" and "consistent" denial operator. Heinrich Wansing (Dresden) developed a proof-theoretic semantics for bi-intuitionistic logics with a denial-like negation. BHK (Brouwer-Heyting-Kolmogorov) semantics is extended by applying proofs, disproofs and their duals. In a similar vein, Luca Tranchini (Tübingen) offered a dualisation of proof-theoretic semantics in terms of refutation. For this purpose he developed a natural deduction (single-premise, multiple-conclusion) for dual-intuitionistic logic. Finally, Ian Rumfitt (Birkbeck, London) rounded off the first day by revisiting his bilateralist theory (where content is specified by both assertion- and denial-conditions), and offering arguments for another theory of content-determination: Evidentialism.

Peter Schroeder-Heister (Tübingen) started us off on the second day with an extension of his proof-theoretic semantics, using a denial operator in programming clauses, and developing corresponding harmony principles between assertion and denial rules. Next up was Michael De (Arché, St Andrews), with an investigation into how the norms of denial are affected by falsity-preservation consequence. Colin Caret (Arché, St Andrews) returned to the topic of semantic paradoxes discussed by Ripley the day before. He explored how we can get a denial operator that blocks revenge paradoxes while preserving as many intuitions about denial as possible. Greg Restall (Melbourne) had the honour of closing the workshop. He developed his theory that multiple-conclusion derivations can be interpreted as rational constraints on assertion and denial, extending it to discussing issues such as logicality and tonk.

The workshop had about 30 participants. We hope they all share our opinion that the event created significant impetus to future work with the logic of denial, highlighting common ground for researchers from a number of different fields. If there was one single conclusion from the workshop as a whole it was that formal approaches to denial offer interesting enrichments of expressive power both in theories about semantic paradoxes and in proof-theoretic semantics.

More information about Arché and FLC events can be found at:

http://www.st-andrews.ac.uk/~arche/index.php

The Organisers,

Stephen Read

Colin Caret

Ole Thomassen Hjortland

Gentzen and Normalisation

Recently, Arché and the St Andrews computer science department (with Roy Dyckhoff) jointly organised a one-day symposium celebrating the centennial of Gerhard Gentzen's birth, November 24th, 1909. The event showcased cross-disciplinary work in computer science, philosophy and logic in short instalments. As keynote speaker, we invited Jan von Plato (Helsinki), proof-theorist and Gentzen scholar. Arguably, he was responsible for a rather significant upset in our little logic community.

I'm a huge Gentzen fan, in fact I think he deserves a place together with Gödel and Tarski in the history of 20th century logic. Even more than the two latter, Gentzen's work contributed to the formation of an entirely new discipline in mathematical logic, a discipline that now completely dominates theoretical computer science, and contributes significantly to both philosophy and linguistics. Yet, biographically, I knew a great deal more about Gödel and Tarski. (If you want a Gentzen biography, this is what you need.)

One thing I didn't know about Gentzen was that there are hundreds of unpublished pages, stenographed in Gabelsberger shorthand. The transcription of Gentzen's notes is a substantial task, but hopefully in the near future we'll be able to see the full scope and significance of his Nachlass. One thing that has already been uncovered, however, but which surprised me quite a bit, is that Gentzen proved normalisation for intuitionistic logic in 1932. In other words, over 30 years before the result was published in Dag Prawitz's dissertation!

Of course we knew all along that Gentzen must have been on to something like normalisation: After all, that appears to be part of the motivation for him looking for, and proving, the cut elimination theorem (the Hauptsatz) for classical logic, and there are some revealing remarks indicating that he had looked at conversions for intro- and elim-rule pairs. Yet, it is astonishing to learn that a result that wasn't known to logicians until 1965, was not only proved by Gentzen while working on his dissertation, but also excluded from the final version of his dissertation. One explanation, offered by von Plato, is that Gentzen thought the direct proof of normalisation unnecessary as he had the corresponding proof of cut elimination in the sequent calculus.

It gets worse. Not only had Gentzen already proved normalisation for intuitionistic logic (and probably failed to do the same for classical natural deduction), but his handwritten manuscript was in his supervisor's (Bernay's) possession after the war. In fact, and here is the real killer, Bernays showed the manuscript to M. E. Szabo, the editor of The Collected Papers of Gerhard Gentzen, and the latter proceeded to use a picture of the manuscript on a cover page of the edition. Szabo used page two, but if he had used page nine instead, we would all have been staring at the start of the normalisation proof. From von Plato's paper Gentzen's Proof of Normalization for Natural Deduction:

Remarkably, most of page 2 of Gentzen's manuscript is reproduced photographically among the frontmatter of Gentzen's Collected Papers of 1969. The editor indicates that the source for the manuscript is Bernays. It is astonishing that he did not mention in this connection, say, the complete set of detour convertibilities that stand very prominently on top of page 9 of the manuscript, or the announcement of the proof of normalization in Gentzen's summary of his further results at the end of the first introductory chapter, and its realization in chapter three. (249)

The paper by von Plato also includes a translation of the handwritten manuscript. An obvious question is to ask to which extent Gentzen's had figured out the details of normalisation. The answer is that his proof is as detailed as what you find in standard textbooks today, complete with conversions and examples. He calls the maximum formula of a non-normal proof a 'Hügel' (translated by von Plato as 'hillock'). I leave the reader to marvel at the details in von Plato's translation.

PhilPapers survey: Logic

The PhilPapers survey has generated a lot of discussion lately. I took the survey myself, and thought that answering the question was a nice exercise in thinking about my own views. In some ways, my own answers surprised me more than the general outcome of the survey.

I suspect that my answers fit well with the Karenin effect. Anna Karenina's husband is the type - we are told - that easily and gladly makes judgements about things of which he knows nothing (art and literature, in particular), but who finds it much too hard to be absolute in his own field (Russian law).

The quintessential logic-question was "Logic: classical or non-classical?" An unsurprising 51,5% answered accept or leaning towards classical logic; against a 15.3% accept or leaning towards non-classical. An honest 12% admitted to being insufficiently familiar with the issue. Myself, I'm a fan of the 'Accept both' answer, thus reading the question as an inclusive or. Nothing wrong with that perhaps, but it makes one wonder what the question here really is about. Classical or non-classical logic for what? - we might see the pluralist add. 3.4% found the question too unclear to answer, and although that was a bit tempting, I suspect that if you go down that path, most questions in the survey would need similar treatment.