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!
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.
Who said tonk is bad? Ok, granted, that's not all there's to it. You also need the following proviso: Below every occurence of from A proceed to B, there is an occurrence of A. Then proceed to discharge A. With Classical Restart so defined, we can get classical logic out. Here is a proof of Peirce's Law from the paper:
Check it out for yourself. The paper contains a lots investigation of the rule and how it relates to other systems, but I haven't checked out all the details yet.
Posts
