Good idea! I had only quite minor edits.

]]>Thanks again Toby, and thanks Mike.

Since this property seems to be important to estimate the role of sequent calculus, I’d like to have a paragraph on this already in the Idea-section of the entry *sequent calculus*. I have added the following, trying to form a conglomerate of what you two said here. Please adjust where necessary:

]]>A central property of sequent calculus, which distinguishes it from systems of natural deduction, is that it allows an easier analysis of proofs: the subformula property that it enjoys allows easy induction over proof-steps. The reason is roughly that, in the language of natural deduction, in sequent calculus “every rule is a term introduction rule” which introduces a term on

bothsides of a sequent with no term elimination rules. This means that working backward every “un-application” of such a rule makes the sequent necessarily simpler.

I’ve put in the logical rules for the classical sequent calculus, but I'm not sure that I like the form chosen for each.

I came up with the equality rule on the left on my own, but it seems like it must be correct.

]]>I don't particularly care for sequent calculus, but proof theorists like it. And it's as Mike says; more precisely, as you work backwards, there are only finitely many possible previous steps. Of course, the length (and width) of a derivation are still arbitrary, but this fact is still helpful, or so I'm told.

This is covered in our article briefly under the heading of the subformula property.

]]>My understanding is that the essential distinguishing feature of sequent calculus is that “all rules are introductions”. That is, rather than a rule which introduces a type and one which eliminates it, you have a rule which introduces it on the left and a rule which introduces it on the right. That means that when working backwards looking for a proof, every “un-application” of a rule “simplifies” some formula or other, so you can be sure that the search will terminate. Or something like that.

]]>Thanks, Toby!

I have read through it. Can you maybe help me : I still don’t have any grasp for which of these rules are so special that sequent calculus is apprently so special.

Let’s restrict attention to an “intuitionistic theory” for the moment. Which of the rules of sequent calculus are it then that make it be of such different nature than natural deduction or something.

P.S. One purely typographical comment on what you wrote: at least on my system the exchange rule is really hard to read, because the uppercase and lowercase phi-s and psi-s are almost indistinguishable.

]]>I added and generalised a lot at sequent calculus, which I felt that I needed to do before sequent.

]]>I added a comment that “intuitionistic sequent” is often used to mean *exactly* one succedent (which is, I believe, my experience), even though technically I guess it would make more sense to call those “minimal sequents”.

I haven’t really been following this discussion, but as I’m now at IAS surrounded by type theorists, I thought I’d ask their opinions. Of the three type theorists nearby when I asked whether a hypothetical judgment such as used in type theory could be called a “sequent”, I got two “yes”es and one “no”. So apparently there is no uniformity of terminology even among type theorists. The “no” later qualified by saying that he could see how one might use it that way, although he would not do so himself.

I think I like the current state of the entry sequent (which isn’t to say that it couldn’t still be improved, of course).

]]>I agree with everything that Ulrik has said, with these minor exceptions:

- I don't know about these more general kinds of sequent calculi (hyper‑, focused, etc), so of course I wouldn't know if what Ulrik said about them is correct (although I presume that it is, of course).
- I would just as soon
*not*introduce the term ’sequent deduction calculus’ for sequent calculus.

Another minor point is that Wikipedia's article Sequent uses the terms ’sequent’ and ’judgment’ only in the senses that I originally did (contrary to a remark earlier by Urs). But this does not contradict that (as Urs has demonstrated above) they are also used more generally.

]]>@Finn: To be fair, I did specify what I meant by that. :-) But I’ll take a gander at what you wrote.

]]>Maybe not quite on-topic, but…

Todd wrote:

it’s well known that the Curry-Howard paradigm (where proofs of sequents are interpreted as suitable functions) breaks down for classical logic

Not entirely true – there are $\lambda$-calculus-like term systems that play the same role for classical logic as simply-typed $\lambda$-calculus does for minimal logic. It is true that the naive interpretation of these as categories doesn’t work; there are several possible ways around this, but none of them is obviously the right one.

I wrote a technical report about all this around the time I started my Ph.D., pdf is here.

]]>How would you feel about that?

Whatever you feel like doing would probably make me feel quite happy. Thanks for your help.

(It seems to me some good public information on these matters would generally be much appreciated. Given how much time we spent on just talking about what something as fundamental to formal logic as “$\vdash$” really means. Imagine where we would be if we had to have such discussion about, say, “$+$” in linear algebra. ;-)

]]>Urs, I certainly like where the entry is going now; it seems very reasonable to me. And of course you’re excused for thinking about context the way you did, as that’s the norm for intuitionistic, natural deduction calculi, which we’re all so interested in these days.

Can you say what the difference is between a “deduction calculus” and a “sequent calculus”?

Did I say “deduction calculus”? I don’t think it’s a standard term, but I maybe it’s a good term to cover a formal calculus for deriving sequents! Unfortunately, sequent calculus already has a quite firm meaning as a particular type of deduction calculus (but we already had that discussion in another thread). Maybe “sequent deduction calculus” is even more precise, to distinguish from calculi deriving formulae?

I’ll try to touch up sequent calculus later today, perhaps moving some of the current material to sequent deduction calculus. How would you feel about that?

]]>Thanks Todd, thanks Ulrik!

For the moment I can easily react to Ulrik’s comments. I need to think about what Todd’s comment imply for the entry. Maybe at some point it will be easier if an actual expert does some editing.

Concerning Ulrik’s list:

Since you let both Ctxt and Jdgmt be judgments, wouldn’t it be clearer to call them Antecedent and Succedent (or Antecedent and Consequent, if you prefer)? Calling one of then the judgment seems misleading, since everything in sight is a judgment.

Sure, that’s easy enough: I have now in the entry changed “$Ctxt \vdash Jdgment$” to “Antecedent \vdash Succedent”. I am maybe excused for the fact that until now and throughout, the nLab used to call the stuff on the left of the turnstile the *context* (as in that entry which wasn’t introduced by me).

Next, you introduce lists of Ctxts. I think the reader will find that confusing: What is the context? Is there one or are there several?

Hm, I thought I introduced that to account for the reactions that I got here. But now I have renamed all these “contexts” to “antecedents”. Is it better this way?

Next, when you mention the first-order variant, you require the lists to be propositions. While technically correct, I think it would connect more clearly to the general concept, if we said we require the judgments to be of the form “φ is true”

Sure, I added that now.

Finally, systems for deriving sequents could be either sequent calculi, or natural deduction calculi, I’d say.

Added a pointer to that, too. Can you say what the difference is between a “deduction calculus” and a “sequent calculus”? By the way, I am getting the impression that the entry *sequent caclulus* says effectively nothing about what sequent calculus really is. Maybe you or somebody feels inspired to add a paragraph on that.

@Todd: thanks for the summary of your thesis!

@Urs: my (very minor) quibbles with sequent are:

Since you let both Ctxt and Jdgmt be judgments, wouldn’t it be clearer to call them Antecedent and Succedent (or Antecedent and Consequent, if you prefer)? Calling one of then the judgment seems misleading, since everything in sight is a judgment.

Next, you introduce lists of Ctxts. I think the reader will find that confusing: What is *the* context? Is there one or are there several? And as I said, sometimes we’ll focus (syntactically or just in our minds) on one of the judgments, and then the rest occurring in the sequent are the context. Or there’s a left and a right context. As Todd said, we can get into trouble if we force everything but one judgment to be on the right. Also, as I said before, that’d be breaking the symmetry in a way that’s not always helpful.

Next, when you mention the first-order variant, you require the lists to be propositions. While technically correct, I think it would connect more clearly to the general concept, if we said we require the judgments to be of the form “$\varphi$ is true” for propositions $\varphi$, and then as a shortcut (since all judgments have this form), leave out the “is true” part since it’s understood.

Finally, systems for deriving sequents could be either sequent calculi, or natural deduction calculi, I’d say.

]]>Hi Ulrik. My thesis is, alas, unpublished (it was completed in 1994), and even worse I no longer have the files. It gave a solution to a coherence problem (a problem of deciding equality: which definable diagrams in the theory of symmetric monoidal closed category commute?), using a combination of methods from linear logic (linear proof nets), sequent calculus, and enriched category theory. While I think the solution is nice, the thesis was in my judgment badly written and overwrought and somewhat embarrassing from an expositional point of view, and I’ve long been hesitant to give people hard copies. One of my hopes is to rewrite it a lot more concisely and make the results more public (from my web for example).

*Some* idea of the solution to that coherence problem can be gained from the paper Natural Deduction and Coherence for Weakly Distributive Categories; see especially the calculus of rewirings. The fact that the logic for symmetric monoidal closed categories is intuitionistic (MILL: multiplicative intuitionistic linear logic) means the rewirings can be organized as a confluent and strongly normalizing rewrite system, which in turn makes deciding equality relatively easy compared to the situation for MLL.

@Urs: thanks for clarifying the question (and sorry for the sidetrack in this comment). Toby can (and should!) speak for himself of course, but my own experience from my thesis is, roughly speaking, that it is difficult giving an unambiguous *functional* interpretation to sequents $\phi \vdash \psi, \chi$. I’m not sure this is what Toby had in mind, but for what it’s worth I’ll continue anyway: it’s well known that the Curry-Howard paradigm (where proofs of sequents are interpreted as suitable functions) breaks down for classical logic, which is where Gentzen worked. Sticking just to propositional logic, what this means is that there is no cartesian closed category in which double negation is involutive (negation being internally homming into 0, the initial object) that doesn’t reduce to a mere poset, i.e., Boolean algebra.

We do of course have a satisfying Curry-Howard paradigm for intuitionistic logic, where Heyting algebras categorify to cartesian closed categories (with coproducts). Here sequents appear in the form $\vec{x}: \Gamma \vdash a: A$ with one type to the right, and we can interpret the antecedent types as domain objects in a multicategory, with multiple input terms and one output term.

We also have a good functional paradigm for linear logic. Here we have a classical negation, and correspondingly two-sided sequents where we can slide formulas back and forth across the turnstile with the help of negation, but we drop structural rules hitherto associated with cartesian structure. The categorified semantics of proofs takes place in $\ast$-autonomous categories.

But one issue in the latter case, where disjunction is not simply “additive” (i.e., coproduct) disjunction that would correspond to the classical logic of Gentzen but rather “multiplicative”, is how to interpret disjunction *functionally*. Should a term of type $\psi \vee \chi$ be interpreted as of type $\psi^\ast \multimap \chi$, or as $\chi^\ast \multimap \psi$? There’s an ambiguity here. It corresponds to whether we write a sequent $\phi \vdash \psi, \chi$ “intuitionistically” as $\phi, \neg \chi \vdash \psi$ or as $\phi, \neg \psi \vdash \chi$. Believe it or not, this can result in some real complications.

If this is not too directly related to what you guys were discussing, then my apologies – I haven’t been paying full attention to the thread. But the hints I got from Toby (when he brought up $Rel$ for example) was that he was thinking along similar lines.

]]>To me, a list of judgments ψ,χ just isn’t a single judgment.

On the other hand it’s not just a list, it’s a list connected by “or”. But anyway, would that mean that if in the entry I just change

$Context \vdash Judgement$to

$Context \vdash Judgements$(plural) that would resolve any disagreement? (Do *you* have a disagreement with the present state of the entry *sequent*, apart from it being incomplete?)

To maybe illustrate where I am coming from: I have no problem that there are different shades of what a sequent is like. What puzzles me however is if some of these shades of meaning are taken to overwrite what *clearly* seems to be the *basic idea* of a sequent: that the LHS gives rise to the RHS.

(I might have given up on this point, if I did not know Martin-Löf on my side here ;-).

Last comment on this, I promise!: I forgot to mention co-intuitionistic sequents which are single-antecedent, multiple-succedents. Then the context proper is on the right!

Thus, I think that thinking of context as what’s on the left is biased and limiting. If we’re interested in exploring duality and symmetry in logic (which I sometimes am!), then we should adopt a symmetric picture as the general case, and then study what happens when the symmetry is broken one way or the other as special cases.

]]>One more thing:

For sequents with multiple succedents, the succedent list is often callen the *right context*, so a sequent can be thought of as having the form

(Now, it’s slightly inconvenient there’s then nothing which is *in* this combined context, but that’s where focalization could come in.)

To me, a list of judgments $\psi, \chi$ just isn’t a single judgment. What’s wrong about saying, like I did above, that a sequent generally has a list of antecedent judgments and a list of succedent judgments, but there are important special cases?

Besides intuitionistic logic, there are also Tait-style calculi, where (like in hypersequent calculi) sequents only have the succedent list (exploiting the symmetry of an involutive negation).

Re 25:

only one proposition on the right of the turnstile

I’d be careful with this language in this discussion. When all judgments are of the form “$\varphi$ true” for propositions $\varphi$, it’s tempting to say that it’s the propositions themselves that are listed, but the integrity of the “sequent” concept (if there’s anything left of it!) demands that judgments are listed.

Re 29:

But just to let you know, I had to deal with sequent calculus quite a bit in my thesis.

Todd, is there a reason there’s no link to your thesis on your homepage at the moment? I’d like to see it!

Of course, I’d also like to maintain that sequents are more general than what is studied in sequent calculi. The roots of derivations in other formal systems also deserve the name “sequent” (e.g., natural deduction).

]]>Okay, Todd, your expertise is greatly appreciated. To remind us: Toby and I are still trying to understand each other’s contrary point of view expressed last time in #22, where Toby writes:

The point that I really need to make is that a classical Gentzen sequent like

$\phi \vdash \psi.\chi$

does not (at least not unambiguously) have the form

$Context \vdash Judgement$.

I still don’t understand why Toby says this. If your comments so far were meant to concern this point, then I missed your point and would ask you to please explain in more detail.

]]>Toby’s view is of course important. But just to let you know, I had to deal with sequent calculus quite a bit in my thesis.

]]>It’s not a big deal, no.

Okay, let’s see what Toby says about it. I want to understand his point of view.

]]>