Want to take part in these discussions? Sign in if you have an account, or apply for one below
Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.
For some text I need to explain the relation between sequents in the syntax of dependent type theory and morphisms in their categorical semantics.
I wanted to explain this table:
| types | terms | |
|---|---|---|
| (∞,1)-topos theory | ||
| homotopy type theory |
So I was looking for a place where to put it. This way I noticed that sequent used to redirect to sequent calculus. I think this doesn’t do justice to the notion and so I have
split off a new entry sequent
added a brief Idea-blurb
added my table and some explanation leading up to it
leaving the whole entry in genuinely stubby state. But no harm done, I think, if we compare to the previous state of affairs.
Thanks. I agree, especially given what I just learned about sequent calculus, that sequent deserves a page of its own.
I changed the heading “Formalizations” to “Semantics”, which seemed to me a better description of what was underneath it.
I’m not sure that I would define ‘sequent’ like that. That looks more like a definition of ‘judgement-in-context’ to me. The sequents in sequent calculus, in particular, are not really like that; for one thing, the left- and right-hand sides are more balanced, and the imbalanced part of the context is put in the middle.
This may have more to do with how I’m used to using the word ‘sequent’ than anything else. But still, it doesn’t seem to fit sequent calculus.
So you would say that even though judgments-in-context in type theory are written with the same notation as the sequents in sequent calculus (or a specialization thereof, allowing only one type on the right hand side), this is just a coincidence of notation, and they are not actually instances of the same thing?
They are certainly closely related things; in both cases, the idea is that one derives the stuff on the right from the stuff on the left. The concept of intuitionistic sequent serves as a bridge between them, since it is a special case of both.
My claim is just that (as I have seen the word used) sequents are the particular case of this general idea that appears in sequent calculus, not the general idea, and not the case that Urs is discussing.
The fully general sequents of classical and linear sequent calculus have a symmetry to them that judgements in HoTT lack, and it's possible to read either side as the context or the judgement. Of course, in a strong enough logic, you can always move everything over to the judgement side; but in classical and linear sequent calculus, you can move everything over to the context side just as easily! It would sound very odd to me to refer to the left side of a sequent in these calculi as a context or the right side as a judgement, since they play entirely symmetric roles. (And in the predicate calculus there is at least a little bit that is definitely the context: the variables, which people usually write in the middle and not on the left side.)
It seems equally odd to refer to a judgement in context in type theory as a sequent. But at least this doesn't violate the basic meaning of the word ‘sequent’ (of one thing following from another), so that may turn out to be my lack of experience.
Gentzen's intuitionistic sequent calculus has the nice property that it can profitably be viewed either way.
My claim is just that (as I have seen the word used) sequents are the particular case of this general idea that appears in sequent calculus, not the general idea, and not the case that Urs is discussing.
What, then, is the right term for the general idea and the case that I mention in the entry? We should accordingly rename it.
I can’t search through the literature right now. I could have sworn that I am using the terminology as usual in DTT.
Let’s see what Google gives…. here on the bottom of p. 4.
I now had a free second to come back to this here:
I think I am going to argue that it is in fact the other way around: under propositions as types the sequents as in sequent calculus or as – to be specific – in def. D1.1.5 of the Elephant are a special case of the sequents in the sense that I have been using it.
For under propositions-as-types, the string
has the same meaning as
And while we can naturally deduce from this that
as well as
we don’t want to make these different judgements conceptually equal. It is important that the first expresses a dependent type and the second its image under dependent product. These are related, but not the same.
Let me know if you disagree. But right now it seems to me that the only way to object to how the entry sequent currently starts is to take the standpoint that we cannot use propositions-as-types. If that’s really felt to be necessary, so be it. But at the moment I find what I currently have there the more natural perspective.
But a discussion of how expressions of the form relate to it, as above, certainly deserves to be added.
What, then, is the right term for the general idea and the case that I mention in the entry?
As I said, I would call the stuff discussed in that entry judgements in context, or really just judgements (since there is no such thing as a judgement without a context). In particular, if I had written the text on the bottom on page 38 (the 4th page) of Novitzká & Verbová, I would have used the word ’judgement’ (or ’judgment’ if I'd been using American spelling).
Probably ’sequent’ is really the best term for the general idea; that's not how I'm used to using that word, but clearly some people are using it that way, and I don't know another. (Maybe one possibility is ’assertion’, which was applies early to Frege's use of ’’; Frege invented that symbol, so every other usage is a generalisation of his, hence a generalisation of his assertion. However, I've only actually seen the term ’assertion’ used for the very limited ways that Frege and Russell used ’’, so it's probably not a good term after all.)
Nevertheless, as far as the stuff currently at sequent goes, I don't understand why you wouldn't just put that at judgment.
This one should be
using the de Morgan dual of .
But actually, your example misses some of the point of sequent calculus, which is is that instead of and , we have and , that is lists (or sometimes something more general) of propositions. So you have
in general. Then negation allows you to move between left and right arbitrary, giving
and
as well as other mixtures. (Here, applies pointwise to a list of propositions to produce a list of propositions.) This is the most important way of moving everything to the right or left side of a sequent, before getting fancy with , , , or . If you do apply these, however, then the true analogue of
on the right is
on the left. (Here, and apply to a list of propositions to produce a single proposition, which you didn't need, and I already mentioned , so the main point is .)
As you can see, the two sides are quite symmetric, and it's really arbitrary to say that one side is the context and the other side the judgement. (Thus the variables, which are unambiguously the context, are placed on neither side.) In fact, it's hard to see how to interpret a list of propositions on the right as a judgement (unless you have an intuitionistic sequent: one with only one proposition on the right). I read something recently (but I can't remember where now) where sombody advocated the position that, when you see a sequent, you should be free to interpret any proposition on either side as the judgement (with its side specified), with the remainder (all of the other propositions, on their respective sides, as well as the variables) as the context. This seems correct to me (even though traditionally the term ’context’ in sequent calculus refers only to the variables), and means that a sequent is very different from a judgement in dependent type theory.
In particular, if you want to view the sequent
as the judgement
you can only because you have chosen the proposition on the right, and it looks like you've done nothing but write the variables on the left because there happened to be only one proposition on the right. But if you want to view
as a judgement, then not only must you pick or (and let's pick ), but if you then write it as
you're clearly doing more than just writing the variables in a different place. (Or, of course, you could view it as
or any of a number of other equivalents, none of which involve simply writing things in a different place.)
Toby,
look at pages 29-30 of
where it says the following:
The forms of hypothetical judgement that I shall need are not so many. Many more can be introduced, and they are needed for other purposes. But what is absolutely necessary for me is to have access to the form
which says that is a proposition under the assumptions that are all true, and, on the other hand, the form
which says that the proposition A is true under the assumptions that are all true. Here I am using the vertical bar for the relation of logical consequence, that is, for what Gentzen expressed by means of the arrow in his sequence calculus, and for which the double arrow is also a common notation. It is the relation of logical consequence, which must be carefully distinguished from implication. What stands to the left of the consequence sign, we call the hypotheses, in which case what follows the consequence sign is called the thesis, or we call the judgements that precede the consequence sign the antecedents and the judgement that follows after the consequence sign the consequent. This is the terminology which Gentzen took over from the scholastics, except that, for some reason, he changed consequent into succedent and consequence into sequence, Ger. Sequenz, usually improperly rendered by sequent in English.
(My emphasis.)
So a judgement is to the left and to the right of the turnstile. The whole thing is a consequence which for funny reasons came to be called a “sequent”.
I have now also checked in the original
His Sequenz is introduced in section 2.3 there
Eine Sequenz ist ein Ausdruck der Form
And in the next sentence Gentzen calls the here the Antezedens and the the Sukzedens
There is no subscript on the arrow. And by Martin-Löf’s account above, that arrow is what today is written as a turnstile.
Toby,
I see your #10 only now, I guess we overlapped in posting. Two comments:
Just because we are allowed to pass from one sequent to another by deduction does not mean that in any given one we are not allowed to distinguish the context from its consequences.
That the subscript is to be interpreted precisely as seems to me to be the standard usage, e.g. section D1.2 of the Elephant. As before, the fact alone that you can apply deduction rules to pass to a different sequent in which what used to be context has become part of the succedent does not mean that in the previous sequent it was not the context.
Meanwhile, given the quote from Martin-Löf above I felt entitled to put that into the entry sequent. On the basis of this I currently don’t see a justification to separate the present content of that entry from its present title.
But if you can tell me where I am all mixed up, if I am, I expect that I will eventually understand and not object any further.
Ah, I guess I see now what’s going on. So in section 3 of
the authors point to Martin-Löf’s Siena lectures that I cited above and then rename Martin-Löf’s sequents to hypothetical judgements.
Toby, would that solve the disagreement, if at sequent I write “also called a hypothetical judgement”? (Notice that even saying “hypothetical judgement” it is still something that has a plain judgement on the left and a plain judgement on the right of the consequence-symbol).
Urs, I do not understand what 13.1 is referring to.
It makes little sense to me to say that, in Gentzen's
the belong to the context and the do not. (Separating them into antecedent and succedent is another matter; that is even-handed.)
I would be pretty happy to refer the sequents of Martin-Löf as hypothetical judgements; I see ‘hypothetical judgement’ and ‘judgement in context’ as pretty much equivalent. I would not be happy to refer to Gentzen's sequents that way; has anybody else referred to them as such?
I'm sorry that I can't get at my copy of the Elephant now, but can you tell me if the stuff from D.1 that you're looking at ever has commas on the right side of the turnstile? I am guessing not. This is the key feature of Gentzen's sequents that makes them very different from Martin-Löf's (or anything else that I've seen in type theory).
I found Martin-Löf's discussion of judgements that precede the consequence sign a little odd, since what is allowed on the left doesn't have to match what is allowed on the right. In his systems, however, contexts can only be built out of judgements (even though usually not every judgement is allowed to appear in a context), so that makes sense for him. (Note that each of these judgements also always appears in a context: the part of the entire context that precedes it.)
has anybody else referred to them as such?
Beyond that random article which I pointed to I had cited Martin-Löf himself:
Here I am using the vertical bar for the relation of logical consequence, that is, for what Gentzen expressed by means of the arrow → in his sequence calculus, and for which the double arrow ⇒ is also a common notation. It is the relation of logical consequence, which must be carefully distinguished from implication. What stands to the left of the consequence sign, we call the hypotheses, in which case what follows the consequence sign is called the thesis, or we call the judgements that precede the consequence sign the antecedents and the judgement that follows after the consequence sign the consequent. This is the terminology which Gentzen took over from the scholastics, except that, for some reason, he changed consequent into succedent and consequence into sequence, Ger. Sequenz, usually improperly rendered by sequent in English.
I take it that this lecture by Martin-Löf is regarded as foundational (that’s at least how Pfenning refers to it. ) So in this foundational lecture Martin-Löf says that the hypothetical judgements that he wants to consider are Gentzen’s sequents, only that he (Martin-Löf) abandons the symmetry between antecedent and succedent.
I don’t understand why it would be important not to follow Martin-Löf here only because in sequent calculus there are more properties imposed on these guys. It’s still the same idea. From a hypothesis we have a consequence. Or many consequences.
Also the Wikipedia article on Sequent agrees with me to view the term in this generality, and not specific to sequent calculus.
I do not understand what 13.1 is referring to.
I thought I was reacting directly to your #10. Maybe then I just don’t understand what the argument is about.
I thought one of your points was that sequents must have their context symmetrically displayed under the turnstile, instead of asymmetrically on the left. I pointed out that this is not the case in Gentzen’s original work.
Next I had the impression that you argued that in Gentzen’s calculus one can pass from one expression with stuff on the left to another expression with the same stuff now on the right. I tried to say that just because there is a rule to pass between expressions this way does not mean that in any given expression there is not an asymmetry between context and consequence. Which clearly there is in Gentzen’s original article.
But if we are not getting anywhere here, let’s let it rest for a while. Maybe it’s time to hear what others have to say.
Ah, I almost missed your question in #15:
I’m sorry that I can’t get at my copy of the Elephant now, but can you tell me if the stuff from D.1 that you’re looking at ever has commas on the right side of the turnstile?
Indeed, it doesn’t.
I am guessing not. This is the key feature of Gentzen’s sequents that makes them very different from Martin-Löf’s (or anything else that I’ve seen in type theory).
I guess this is the key point: what Johnstone has is different from Gentzen’s sequent calculus, yes, but he speaks of sequents and sequents calculus nevertheless. Gentzen’s calculus is regarded as just one example of a general notion, I’d say.
Keep in mind that Gentzen was working in classical logic, whereas most of the logics considered in The Elephant are not classical.
There are a couple of things that I want to say even before I read the other comments since my last:
First, a minor technical point: wherever I've written ’intuitionistic sequent’ above, it should have been ’minimal sequent’. (A classical sequent may have any number of propositions on the right; an intuitionistic sequent may have at most one, and a minimal sequent may only have exactly one. But it is possible to describe any of these three logics using rules based on any of these three types of sequent, and I prefer intuitionistic logic with minimal sequents.)
Now something more to the point: Urs has made it clear that the word ’sequent’ is used much more generally than in sequent calculi like Gentzen's and the stuff at sequent definitely belongs there. So while I was effectively saying «That page has the wrong content.», I can only correctly say «That page is incomplete.», and a perfectly good answer to that is «So complete it.», which I will accept. Of course, we can still talk here about what sequents are, but I'm not going to try to argue that judgements in context aren't also sequents.
Hopefully Urs knows after my last comment that I don't disagree with him as much I used to, so I shouldn't need to reply to much, but here are a few things:
When I asked
has anybody else referred to them as such?
I meant, has anybody (besides Urs) referred to the sequents in Gentzen's classical sequent calculus as hypothetical judgements? That still seems odd to me. Yet these are definitely sequents, so ’sequent’ and ’hypothetical judgement’ aren't synonyms.
I thought one of your points was that sequents must have their context symmetrically displayed under the turnstile, instead of asymmetrically on the left. I pointed out that this is not the case in Gentzen’s original work.
I wouldn't make that claim now that I see how generally sequents are used (or rather how general are what are considered sequents). And I would never say ’must’. But I still claim that in Gentzen's sequent calculi the variables are usually placed under the turnstile (if anywhere) and only these are usually considered the context. And I don't see anything to the contrary in your quotation from Gentzen himself, where there are no variables.
More generally, the idea that a context (wherever you write it) consists only of variable declarations and does not include any propositional antecedents is quite common, even the distinction is rather artificial using propositions as types. It makes sense for Gentzen's sequent calculi, especially the classical one, although even there I prefer the alternate interpretation that I mentioned in the middle of #10 (in the paragraph with no displays), in which the variables must be part of the context but some propositions may also be viewed thus.
In any case, it's not true in Gentzen's classical sequent calculus that ’context’ means the left side of a sequent (with or without the variables included).
Next I had the impression that you argued that in Gentzen’s calculus one can pass from one expression with stuff on the left to another expression with the same stuff now on the right.
I just mean that there is no big difference in character between the two sides, such that one is context and the other is not. It's like domain and codomain in a category like ; you have to keep track of which is which, but they play entry symmetrical rôles (unlike in a category like ). The ability to move things around with negation is perhaps a distraction (even though it does exhibit the symmetry), but we were already talking about moving things around then.
But if we are not getting anywhere here, let’s let it rest for a while. Maybe it’s time to hear what others have to say.
I write the above before I read this, so I'll post it. The pont that I really need to make is that a classical Gentzen sequent like
does not (at least not unambiguously) have the form
Here are my 2¢: A sequent often has the form
meaning that the conjunction of the judgments (the antecedents) imply the disjunction of the judgments (the succedents). A particular case, namely intuitionistic sequents, have at most one succedent, which is then often called the consequent. And in that case we may choose to view the list of antecedents as a context.
But note that there are exceptions to the rule. A mild one is the one you’ve discussed concerning first-order logic with terms and propositions in context (of sorted variables ):
This is easily recast to match the rule, as
Where we have two different kinds of judgment on the left, and only one on the right, and we sort the judgments on the left so that sort declarations precede the judgments asserting the truth of propositions.
Another exception is focalized calculi that have a wide variety of sequent types. For instance, in Rob Simmons’ Structural Focalization, we see:
(an inversion sequent with an inversion context) as well as
(a left focus sequent).
Finally, I thought I might mention that some people are interested in hypersequents, which are sequences
of sequents read disjunctively. Thus, they are sequents-of-sequents with no antecedent sequents.
I’m sorry if most of this has been said above; I mainly just wanted to express my opinion that sequents are more general than intuitionistic (single-conclusion) sequents.
Thanks Toby, thanks Ulrich!
I gather I come across as argumentative, but I just want to understand. Some of these things would probably have been easier to hash out by personal discussion than via text messages.
I can only correctly say «That page is incomplete.»,
Yes, certainly. I have now added a stub Definition-section to sequent with placeholder subsections for some of the formal versions of sequents that I can discern here. Anyone who has a minute please feel free to add material.
I have also expanded the Idea-section in an attempt to better indicate the variety of flavors of sequents. Anyone should feel encouraged to try to improve on what is there.
A remaining question that I have is about Toby’s statement here:
The point that I really need to make is that a classical Gentzen sequent like does not (at least not unambiguously) have the form .
What does that expression express when you read it out in words? Does it not say that the right hand follows from the left? Probably this is the main point of misunderstanding between me and Toby.
The intended reading of is “if is true then at least one of or is also true”, which is quite a mouthful compared to the somewhat misleading “ follows from ”. I would only use the latter when there’s only one proposition on the right of the turnstile.
The intended reading of is “if is true then at least one of or is also true”,
This is what I was thinking, thanks for confirming. This is, to my mind, precisely the meaning of “in the context of ” we have the consequence .
That the comma on the right is read a a disjunction is not a big deal, is it? “Given we have or .”
It’s not a big deal, no. Of course the monoidal product on the right (disjunction) is different from the monoidal product on the left (conjunction), and this inevitably affects the formalism for how sequents are “composed” according to the cut rule. Categorically, this is modeled by a polycategory (like a multicategory, but with both inputs and outputs), where composition is restricted to plugging a single output term into a single input. In the “linear” versions, the two monoidal structures are related by a certain strength to form a weakly distributive category (Cockett and Seely), which can be completed by a full and faithful embedding in a -autonomous category.
It’s not a big deal, no.
Okay, let’s see what Toby says about it. I want to understand his point of view.
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.
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
does not (at least not unambiguously) have the form
.
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.
To me, a list of judgments 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 “ true” for propositions , 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).
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.)
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.
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
to
(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 ;-).
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 . 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 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 -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 be interpreted as of type , or as ? There’s an ambiguity here. It corresponds to whether we write a sequent “intuitionistically” as or as . 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 for example) was that he was thinking along similar lines.
@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 “ is true” for propositions , 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.
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 “” 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.
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?
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 “” really means. Imagine where we would be if we had to have such discussion about, say, “” in linear algebra. ;-)
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 -calculus-like term systems that play the same role for classical logic as simply-typed -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.
@Finn: To be fair, I did specify what I meant by that. :-) But I’ll take a gander at what you wrote.
I agree with everything that Ulrik has said, with these minor exceptions:
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.
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 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 added and generalised a lot at sequent calculus, which I felt that I needed to do before sequent.
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.
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.
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.
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.
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 both sides 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.
Good idea! I had only quite minor edits.
1 to 51 of 51