Saturday, August 30, 2008
Monday, August 25, 2008
Sunday, August 24, 2008
Brings to mind the following tag-line: "Off the record, on the QT, and very hush-hush." Needless to say, you need to go to Estonia to listen to Greg and others talk about logical pluralism, but I'll shamelessly give a sneak preview for those of us who won't have the chance to be there (and for those who're just looking to get a jump on Greg). At any rate, you'll find that it's a paper with great new prospects for pluralism.
As the title gives away ('Pluralism and Proofs') we're finally given some insights on the relationship between Beall-Restall style pluralism (BR-pluralism) and proof-theory. In the book they ended on a note merely saying that these issues deserved more attention. Now the time for more attention has arrived.
Most readers will already be at least superficially familiar with BR-pluralism. Basically, it involves variations over a validity-schema where truth-preservation is a constant, and the type of cases over which truth-preservation holds (or does not hold) can be varied.
V-schema: Γ |= A iff for every case c, whenever c(B) = 1, for every B ∈ Γ, then c(A) =1.
With some suitable constraints on what a case can be (e.g., models, worlds, situations, constructions, etc) we get different output consequence relations. Thus, pluralism.
This is not the place to list up different objections and replies to the BR-approach. In fact, they've already done that for us at the end of the book. Rather, let's look at how one might be a pluralist "in the land of proofs" (to use a Restallian phrase). The aim is the following: making sense of the distinction between One Language-Many Logics and Many Languages-One Logic. This is the familiar distinction between logical pluralism (and BR-pluralism in particular) and Carnapian tolerance. What the BR-pluralist wants is the former without the latter.
On the BR-axis it meant something like there being lots of different consequence relations (all equally good), but still involving the same logical constants. This got them into some trouble because the truth-conditions for the involved logical constants appear to change with shifts in the type of cases one insert into the V-schema (see Graham Priest's Doubt Truth to Be a Liar, ch. 12). Truth-conditions for, say, conjunction can be schematised: A & B is true in a case c iff A is true in c and B is true in c. It is hard to say whether the involved constant is semantically insensitive to shift in the range of cases; and even harder if the constant in question is something more controversial like negation.
Does the proof-theoretic approach offer a better solution? Let's take a look at Greg's example.
Above are the classical sequent rules for negation. By observing some restrictions on the antecedent and succedent contexts, we reach non-classical logics: Intuitionistic logic results from letting the cardinality of Y be 1 or lower for any sequent X |- Y; dual-intuitionistic logic results from letting (yes, you guessed it) X be 1 or lower for any sequent X |- Y. Applied to the above rules we get intuitionistic and dual-intuitionistic negation respectively. Take the following derivations:
Clearly, only by ignoring both constraints will all of the above count as proofs. Needless to say, intuitionistic negation won't give us DNE and LEM; with the dual restriction we do get these, but not the two other derivations.
The suggestion is for us to consider the above rules not as parts of three different calculi, but as a single calculus with three different proof-conditions. That is, there is only one negation (and one set of negation-rules), but the notion of a proof is split up into three. In other words, the inductive definition of a proof is now multifaceted -- a derivation is an intuitionistic proof if it abides by the succedent constraint; a dual-intuitionstic proof if it abides by the antecedent constrain. If the derivation abides by both it is an intuitionistic proof and a dual-intuitionistic proof; if it abides by none it is (merely) a classical proof.
Along the One Language-Many Logics line, we can interpret the mixed calculus as giving form to the idea that there is only one negation, even though there are a multitude of provability relations within the same calculus. Let me start by saying why I think this idea has some important advantages: First of all it frees up some structural binds that haunted the old BR-pluralism. In particular, since the validity schema was formulated as (material) truth-preservation across different types of cases, the resulting consequence relations were invariably reflexive and transitive. (A fact that the authors of course acknowledges.) In the proof-theoretic framework there is scope to devise calculi where the same constant can contribute to different provability relations depending on which structural rules are allowed.
But what I think is the most powerful and promising part of the proposal is also the greatest challenge. Although there is now only one rule for negation at large in the calculus, there are in a sense three different proof-conditions. To use Greg's own metaphor, a derivation can have different "virues": intuitionistic-virtue, dual-intuitionistic virtue, classical virtue (sin?). With the notion of proof differentiated there is a gain of expressive power in the proof-theoretic semantics (in the sense that the meaning of a logical constant is somehow tied to its proof-conditions). Yet, if we allow the semantics to be this sensitive -- i.e., saying that a negation takes different content depending on what proof-conditions we require of it -- seems to come with the cost of pointing away from pluralism. For, if there are three semantically significant proof-conditions in play in the calculus, then it is a stretch to say that we've reached the One Language-Many Logics dream.
I'm looking forward to hearing what other people at the conference will think of the proof-theoretic turn for pluralism. Best of luck to all the participants, and thanks to Greg for the sneak preview!
Friday, August 22, 2008
Monday, August 11, 2008
This includes (not exhaustively) Nils Kurbis (UCL), and Julien Murzi (Sheffield), and Florian Steinberger (Cambridge). In addition, there are people like Michael Gabbay (KCL) and Marcus Rossberg (Arché/UConn) who have also done exciting research on proof-theory and harmony. Close, but not in the UK, we have Pål Fjeldvig Antonsen (TCD) working on harmony in a broader philosophical setting. A bit further away, on the continent, there are Theodora Achourioti (Uni of Amsterdam) also in the process of writing on harmony, and Henri Galinon (IHPST) writing about interrelations between truth and proof. Among young researchers there are Denis Bonnay (Ecole Normale Supérieure) and Patrick Allo (Vrije Universiteit Brussel). And I'm sure there are many more.
Now here is the question. Who is doing related work in the US? Although I don't know enough about the US departments to say anything definitely, my impression is that there is less work being done on these topics, perhaps because figures like Dummett and Prawitz had/have less influence in the US. Please let me know that there is no divide.
UPDATE As Kevin and Noam points out in the comments, OSU and Pitt/CMU are probably good candidates for places with students/faculty working with related topics. The faculty most will know, but who are the students. I know of Noam Zeilberger (CMU) and also Shawn Standefer (Pitt).
Sunday, August 10, 2008
She had heard all about excluded middles; they were bad shit, to be avoided; and how had it ever happened here, with the chances once so good for diversity? For it was now like walking among matrices of a great digital computer, the zeroes and ones twinned above, hanging like balanced mobiles right and left, ahead, thick, maybe endless. Behind the hieroglyphic streets there would either be a transcendent meaning, or only the earth.Who would have thought Oedipa was educated in Amsterdam?
-- Thomas Pynchon, The Crying of Lot 49, p. 125
Friday, August 08, 2008
So what's so neat about the classical restart rule? For, yes, it is pretty neat. Take a natural deduction system for intuitionistic logic and add the following rule: