(Cross-posted at NewAPPS)

As some
of you may have seen, we will be hosting the workshop ‘Proof theory and philosophy’ in Groningen at the beginning of December. The idea is to focus on
the philosophical significance and import of proof theory, rather than
exclusively on technical aspects. An impressive team of philosophically
inclined proof theorists will be joining us, so it promises to be a very
exciting event (titles of talks will be made available shortly).

For
my own talk, I’m planning to discuss the main structural rules as defined in
sequent calculus – weakening, contraction, exchange, cut – from the point of
view of the dialogical conception of deduction that I’ve been developing,
inspired in particular (but not exclusively) by Aristotle’s logical texts. In this post, I'll do a bit of preparatory brainstorming, and I look forward to any comments readers may have!

In a
nutshell (as previously spelled out e.g. here), the dialogical conception is based on the idea that a deductive proof is best understood as
corresponding to a

*semi-adversarial dialogue*between two fictitious characters, proponent and opponent, where proponent seeks to establish a final conclusion from given premises, and opponent seeks to block the establishment of the conclusion. Proponent puts forward statements stepwise, which she claims follow necessarily from what opponent has already granted in the course of the dialogue. Opponent can grant these statements, or else he can object that a given statement does not follow necessarily from what he has granted so far, by providing a counterexample (a situation where premises hold but conclusion does not). Another move available to opponent is: "why does it follow?" This would correspond to an inferential step by proponent that is not sufficiently perspicuous and compelling for opponent; proponent must then break it down into smaller, individually perspicuous inferential steps. The game ends when proponent manages to compel opponent to grant her final conclusion.
The
motivation behind this dialogical conceptualization is what could be described
as a

*functionalist*approach to deductive proofs: what are they good*for*? What is the goal or function of a deductive proof? On this setting, the main function of a deductive proof is that of*persuasion*: a good proof is one that convinces a fair but ‘tough’ opponent of the truth of a given statement, given the (presumed) truth of other statements (the premises).
I
believe that this dialogical/functionalist approach allows for a
philosophically motivated discussion of the different structural rules. This
becomes important in the context of the recent surge in popularity of
substructural approaches to paradoxes (just yesterday I came across the
announcement for a very interesting workshop taking place in a few weeks in
Barcelona precisely on this topic). A number of people have been arguing that
in many of the paradoxes (the Liar, Curry), it is the availability of

*contraction*that allows for the derivation of the paradoxical conclusion (as I discussed here and here). I have expressed my dissatisfaction with many of these approaches given the lack of an independent motivation for restricting contraction: to say that contraction must be restricted solely because it gives rise to paradox is nothing but a ‘fix-up’ which does not take us to the core of the phenomenon. What is needed is a reflection on why contraction was thought to be a legitimate principle in the first place, and arguments against this presumed original rationale for contraction (or any other rule/principle).
Naturally,
restrictions on structural rules are not a new idea: indeed, relevant
logicians have offered arguments against the plausibility of weakening, and
linear logicians pose restrictions on contraction. But in both cases, what
motivates restriction of these structural rules are not paradox-related considerations; rather, it stems from independent reflection on
what the logical systems in question are good

*for*– in other words, something resembling the functionalist approach I am defending here. Linear logic is usually described as a logic of resources, and as such it matters greatly how many copies of a given formula are used – hence the restriction on contraction. Relevant logics require a relation of relevance between premises and conclusion, which can be disrupted by the addition of an arbitrary formula – hence the restriction on weakening.
Now,
as it turns out, the dialogical conception of deductive proofs has its own
story to tell about each of these structural principles. Let us start with
weakening, which is the following structural rule in its sequent calculus
formulation (I will restrict myself to left-weakening, as right-weakening poses
a range of other problems related to the concept of multiple conclusions):

A => C

--------------

A, B => C

In
first instance, if necessary truth-preservation is the only requirement for the
legitimacy of proponent’s inferential steps, then weakening may seem as an
entirely plausible principle: if opponent has granted A and is then compelled
to grant C because C follows of necessity from A, then whatever additional B that comes up in the dialogue and is granted by opponent will not invalidate
the move to C. That's simply the property of monotonicity, one of the core components of a deductive proof.

However,
there is much more to be said on weakening from a dialogical perspective, and
now it becomes useful to distinguish different

*kinds*of such dialogical interactions. In the spirit of the purely adversarial interactions described for example in Book VIII of Aristotle’s*Topics*, it is in fact in the interest of proponent to confuse opponent by putting forward a large number of statements, some of which will be irrelevant to her final conclusion. In this way, opponent will not ‘see it coming’ and therefore may be unable to guard himself against being forced to grant the final conclusion. So in a purely adversarial setting, weakening is in fact*strategically advantageous*for proponent, as it may have a confusing effect for opponent.
By
contrast, in a context where the goal is not only to beat the opponent by
whichever means, but also to produce an

*explanatory*proof – one that shows not only*that*the conclusion follows, but also*why*it follows – weakening becomes a much less plausible principle. Indeed, for didactic purposes for example, it makes much more sense to put on the table only the information that will in fact be relevant for the derivation of the conclusion, precisely because now confusing the interlocutor is the opposite of what proponent is trying to accomplish. And indeed, as it turns out, Aristotle’s syllogistic – which, according to some scholars, was developed to a great extent so as to provide the general framework for the theory of scientific explanation of the*Posterior Analytics*– is a*relevant system*, one where weakening is restricted. That is, for explanatory purposes, weakening is a pretty bad idea. So in other words, depending on the*goal*of a particular dialogical interaction of this kind, weakening will or will not be a legitimate principle.
(As this post has already become quite long, I will leave
contraction, exchange and cut for a second installment later this week. So stay
tuned!)

UPDATE: Part II here.

UPDATE: Part II here.

hi Catarina,

ReplyDeletetwo trivial comments. instead of "and linear logicians pose restrictions on contraction" you should say linear logicians pose restrictions on contraction and weakening. Indeed you remove both rules in Linear Logic and moreover, it is thought that it's the removal of both, at the same time, that makes the logic well-behaved, proof-theoretically. Also I think you muddled your variables when discussing the weakening rule in the post. But I like a lot the idea of the dialogical conception of deductive proofs, it seems to make sense in many different levels.

Hi Valeria, thanks! Yes, I had made a mess with my variables, which seems to be fixed now :)

DeleteAnd yes, of course you are right that linear logic restricts weakening as well, for reasons very similar to those why it restricts contraction. I suppose I didn't mention this mostly so as to get a nice symmetry between contraction and linear logic on one side, and weakening and relevant logics on the other side. But you are right, from a Gricean point of view I should have mentioned both for LL :)

hi, thanks. Catarina. I think the point of LL getting rid of both weakening and contraction is important, because many of the mathematical arguments for naturalness and usefulness of logical systems rely on aesthetic criteria like symmetry. and relevance logic has had a very hard time trying to get itself pretty enough to be taken seriously... the picture I have in mind is that relevance logic and direct logic each remove one structural rule on the left, LL removes both and this helps to make its cut-elimination work, it makes it more symmetric, from a proof-theory point of view.

DeleteI'm looking forward to the next blog post on contraction, exchange and cut!

Thanks for a thought-provoking post. Two comments:

ReplyDelete1. "So in a purely adversarial setting, weakening is in fact strategically advantageous for proponent, as it may have a confusing effect for opponent."

I wonder whether it might also be a strategic DISadvantage for Proponent as well (depending on the rules of the adversarial conflict): it opens up Proponent to criticisms she might not otherwise be vulnerable to. That is, if Proponent is responsible for defending all the premises she puts forward, then Opponent has many more targets to attack, if Proponent adds a bunch of unnecessary premises to the argument.

2. You must've gotten this question a zillion times before, so feel free to just give a link to an answer you've given elsewhere. What is the relation of your view to so-called game-theoretic semantics?

Hi Greg, thanks. Regarding your first point, in the questions and answers Aristotelian format that provides my main inspiration, proponent does not have to defend premises once they are granted by opponent; in fact, once opponent grants them *opponent* is commited to them but *not* proponent (which is the core of my dialectical explanation of reductio proofs, which I also blogged about some time ago).

DeleteRegarding your second point: well, first of all Hintikka and I are inspired by the same source, namely Aristotle and ancient dialectic! :) But there are many differences between his framework and mine, for example in that I am not in the business of explaining the meaning of specific logical terminology in game-theoretical terms. But perhaps the main difference (which also applies to other dialogical approaches, such as Lorenzen's) is that in the full version of the story my opponent is a built-in opponent (http://m-phi.blogspot.nl/2012/06/deductive-proofs-transferability-and.html ), a silent participant, whereas these other approaches have two active participants.

thanks, and thanks!

DeleteThis comment has been removed by the author.

ReplyDeleteI enjoyed the possibility in this explanation of dialogous logic that proof-theoretic logic might have some relation to principles of exclusivity.

ReplyDeleteFor example, there is a suggestion, particularly in your statement about left-weakening, that A => C would mean an 'A exclusive for C', and likewise that 'A, B => C' would mean an A and a B exclusive for C.

Some people may consider those to be ideal sets, which only make sense when qualia terms are used, or with simple arithmetic that is too restrictive (e.g. perhaps Pascal numbers). There is a suggestion that if exclusion were the operant principle, that then A, B => C would not follow in some cases, because the additional premise B could be the opposite of C, and thus 'A => C' would not follow. Perhaps this is a diversion, but modal realists might think that opposite are reconcilable, whereas in many actual theories and practices, opposites imply negation. Perhaps a rule to build in would be acceptance or rejection of duplicity, with even metaphysical consequences.

The general point I am trying to get at is that sometimes a theory seems to supervene a mode or calculation (for example the concept of value, or the concept of exception). I am very interested to see what those more mathematical than myself have to say about this, or if math in general is just an ox running away with an orange cart. This could be a very large subject to address in the future, if anyone is interested. And I am interested to hear immediate responses as well, if anyone is intrigued by this concept of exclusivity.

By the way, as a sidenote to students or those who are intrigued, I have some papers which may or may not be considered useful in relation to exclusivity or categories as a discipline, at southernct.academia.edu/NathanCoppedge