Category Theory
Zulip Server
Archive

You're reading the public-facing archive of the Category Theory Zulip server.
To join the server you need an invite. Anybody can get an invite by contacting Matteo Capucci at name dot surname at gmail dot com.
For all things related to this archive refer to the same person.

Stream: deprecated: logic

Topic: Terminology: “a calculus of sequents”

James Wood (Feb 21 2021 at 10:45):

I want to know whether there is any somewhat accepted terminology to distinguish sequent calculus in a strict sense from presentations of deduction systems that use sequents. By the former, I mean systems characterised by left and right rules that decompose a single formula, and with identity and cut rules such that identity expansion + cut elimination amounts to (weak) normalisation. By the latter, I include the former systems, but also natural deduction using a notation like $\Gamma \vdash A$, rather than binding hypothetical assumptions (variables) via $\vdots$. The distinction is made in this sentence (https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspondence#Natural_deduction_and_lambda_calculus):

Below, the left-hand side formalizes intuitionistic implicational natural deduction as a calculus of sequents (the use of sequents is standard in discussions of the Curry–Howard isomorphism as it allows the deduction rules to be stated more cleanly)

I'd like to say “calculus of sequents” for the broader class of calculi, but I'm concerned about this phrase not being distinct enough from “sequent calculus”. Are there any better terms for each class?

Valeria de Paiva (Feb 21 2021 at 14:08):

James Wood said:

I want to know whether there is any somewhat accepted terminology to distinguish sequent calculus in a strict sense from presentations of deduction systems that use sequents. By the former, I mean systems characterised by left and right rules that decompose a single formula, and with identity and cut rules such that identity expansion + cut elimination amounts to (weak) normalisation. By the latter, I include the former systems, but also natural deduction using a notation like $\Gamma \vdash A$, rather than binding hypothetical assumptions (variables) via $\vdots$. The distinction is made in this sentence (https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspondence#Natural_deduction_and_lambda_calculus):

Below, the left-hand side formalizes intuitionistic implicational natural deduction as a calculus of sequents (the use of sequents is standard in discussions of the Curry–Howard isomorphism as it allows the deduction rules to be stated more cleanly)

I'd like to say “calculus of sequents” for the broader class of calculi, but I'm concerned about this phrase not being distinct enough from “sequent calculus”. Are there any better terms for each class?

I agree that the distinction between these two kinds of sequents is important, but think proof theorists only talk about ND in sequent-style formulation, one of the many kinds of “calculus of sequents” that you meant. so the names are not great, but yes, I don't think you can make the distinction using “calculus of sequents” and “sequent calculus”. these two phrases need to be synonymous. my 2 cents.

Mike Shulman (Feb 21 2021 at 15:39):

Yeah, this confused me for a while too. It's unfortunate that "sequent calculus" seems to be universally used only for that particular class of "calculi using sequents", but I agree with Valeria that the difference between "sequent calculus" and "calculus of sequents" is too fine to carry mathematical meaning. (In particular, such a distinction would be impossible to express in many non-English languages.)

Mike Shulman (Feb 21 2021 at 15:39):

What about just calling the more general class "type theories"? (-:

Valeria de Paiva (Feb 21 2021 at 18:40):

Mike Shulman said:

What about just calling the more general class "type theories"? (-:

But @Mike Shulman the problem then is how do you distinguish type theories really (the ones that have terms and types and perhaps other kinds of judgments), from the "naked" version that is a sequent calculus only on the types?

Valeria de Paiva (Feb 21 2021 at 18:41):

and indeed @Mike Shulman is right: in Romance languages you don't have compounds like "sequent calculus" you have to talk about "calculo de sequentes" in Portuguese.

Mike Shulman (Feb 21 2021 at 19:03):

I suppose you could call them "logics".

Amar Hadzihasanovic (Feb 21 2021 at 19:06):

In the past I have referred to the particular class as "Gentzen-style" sequent calculus, but I do not know if that's recommendable in the light of the discussion on not naming nazi sympathisers if not strictly necessary.

Valeria de Paiva (Feb 21 2021 at 19:36):

Mike Shulman said:

I suppose you could call them "logics".

Yes, you could, but lots of people would be really upset. After all many people think of logics as axiomatic or Hilbert systems only. of course they're mistaken, Hilbert systems are practical to prove things about the system, but atrocious to find proofs in, but many people don't want to think of different presentations of logical systems.

Valeria de Paiva (Feb 21 2021 at 19:41):

@Amar Hadzihasanovic we're not talking about Gentzen-systems, strictly speaking. People called these Martin-Loef sequent presentation, because the rules are intro/elim, but they look on the page like sequent calculus rules: we declare our variables in a sequent $\Gamma$. so if you're only talking to category theorists any of these names work, but if you want to talk to other logicians, then it matters.

Mike Shulman (Feb 21 2021 at 20:33):

I don't have a lot of sympathy for anyone who isn't willing to refer to natural deduction as "logic". (-:

Valeria de Paiva (Feb 21 2021 at 20:49):

Mike Shulman said:

I don't have a lot of sympathy for anyone who isn't willing to refer to natural deduction as "logic". (-:

me neither, but these guys are not saying ND is NOT logic, they're saying it's not the only logic, nor the most well-behaved formalism in logic.

Mike Shulman (Feb 21 2021 at 21:02):

Oh, I see -- you mean using "logic" for this kind of calculus would be too narrow, because Hilbert systems are also a kind of logic.

Mike Shulman (Feb 21 2021 at 21:03):

I can see that.

Mike Shulman (Feb 21 2021 at 21:04):

I suppose one could talk about a "hypothetical deductive system".

Mike Shulman (Feb 21 2021 at 21:04):

Or perhaps "deductive system with hypotheticals" would be more clear...

Amar Hadzihasanovic (Feb 21 2021 at 21:04):

@Valeria de Paiva My message was in response to the original post, as I was under the impression that what James Wood called “sequent calculus in a strict sense” was essentially Gentzen-systems: he speaks of left-right rules (that I assumed is intro rules) and cut-elimination as normalisation. I am aware that the discussion has moved on to the more loose interpretation of sequent calculus. Sorry for not making it clearer. Of course there is a chance that I also misread the original post.

James Wood (Feb 21 2021 at 21:08):

There are too many negations! But I think everyone's making sense.

Amar Hadzihasanovic (Feb 21 2021 at 21:09):

So leaving aside the opportunity of naming Gentzen, would it be imprecise to use “sequent calculi” for the more general notion, and “Gentzen-style sequent calculi” for the stricter notion?

James Wood (Feb 21 2021 at 21:11):

Yeah, other than that issue, “Gentzen-style” seems like a good descriptor.

Valeria de Paiva (Feb 21 2021 at 21:13):

Amar Hadzihasanovic said:

Valeria de Paiva My message was in response to the original post, as I was under the impression that what James Wood called “sequent calculus in a strict sense” was essentially Gentzen-systems: he speaks of left-right rules (that I assumed is intro rules) and cut-elimination as normalisation. I am aware that the discussion has moved on to the more loose interpretation of sequent calculus. Sorry for not making it clearer. Of course there is a chance that I also misread the original post.

oh, I see. I think James Wood really was talking about “sequent calculus in a strict sense”, but then the issue is that ND is also a Gentzen-system, right? anyways, the problem is the naming of the more general systems that use sequent-like notation, but are actually ND, because we all got confused when we first saw them, right? I know I did get confused. they look like the same thing, but they're not, it's not a small syntactic detail that authors do differently: it has big consequences. but "deductive system with hypotheticals" is clear, but too long!

James Wood (Feb 21 2021 at 21:14):

Mike Shulman said:

Or perhaps "deductive system with hypotheticals" would be more clear...

This sounds like natural deduction to me, particularly in the Martin-Löf style. I'd argue that there aren't really hypotheticals in a sequent calculus – just another list of formulae that might be used. See single-sided presentations, too.

James Wood (Feb 21 2021 at 21:26):

Valeria de Paiva said:

because we all got confused when we first saw them, right?

I think it's really telling that Conor McBride has to bang on about type theory design decisions that amount to the basics of natural deduction. Newcomers (of course including myself a couple of years ago) can't tell apart ND and SC, and even once they can, they can't see what makes natural deduction rules presented as sequents work. Gentzen's notation for natural deduction has its own problems (the whole discharging of hypotheses is confusing as hell), but I think there's a time and place for students to learn it.

Conor McBride (Feb 21 2021 at 21:57):

Thus invoked, I must tell the story of how arriving five minutes early for a supervision changed my life.

I was taught natural deduction in conventional forward style. I struggled with and resented the creativity involved with disjunction elimination: invent the thing that holds in both cases! I solved the puzzles but it felt unpleasantly like hard work.

Days later, I arrived at my supervision five minutes early and caught Tom Forster writing up the solution on his blackboard, working backwards from the goal. It was obvious that the thing that should hold in both cases was the goal at hand. I felt both enlightened and betrayed.

Every textbook I have ever read on this topic makes the same mistake.

Valeria de Paiva (Feb 21 2021 at 22:01):

So you've learned NF from Thomas Forster? what a small world!