Talk:Sequent

I propose merging this page into the sequent calculus page, and turning this page into a redirect to the latter. ---- Charles Stewart 17:33, 18 Aug 2004 (UTC)

Spelling Context

Note to self and any others who embark on search & correct missions to correct succede to succeed (the non-math-literate ones like myself, anyway) - succedent is in fact a real word and correctly spelled as such. Those naturally drawn to the subject matter of which this entry is a part no doubt already knew that - just a note for others. Longshot14 05:45, 2 March 2006 (UTC)

Careful with the redirects!

I just got to this page by clicking on the word assertion in another page. This word was interpreted as Logical assertion which was then redirected here. I think we need to have a separate article for assertion, even if the content of the latter might be minimal. Thanks! dcresti 19:39, 31 May 2007 (UTC)

Wrong rule

Isn't the rule given in the "Rules" section upside down? It is certainly sound (tough not so useful, and atypic), but the other way round it would be the cut-rule, which is probably what was intended. Mattias Ulbrich 17:24, 15 February 2007 (UTC)

Removed a phrase

I removed the following:

It may help to point out that we assign these meanings to these symbols. The :rules themselves behave in a mechanical nature and do not carry underlying :meaning. See Gödel's incompleteness theorems for more on that topic.

as it is not clear to me what this is trying to say, and how it is helpful. Zero sharp 19:43, 11 May 2007 (UTC)

logical formulae?

What's meant with logical formulae? Maybe Well-formed formula?
Also, this article would benefit from a real example. Thanks, --Abdull (talk) 18:46, 25 October 2009 (UTC)

Merge sequent page into sequent calculus page

I think I've just been wasting my time adding references to the "Sequent" page. The "Sequent calculus" page makes this page completely superfluous. Anything useful in the "Sequent" page should be moved to the "Sequent calculus" page and the "Sequent" page should redirect to it, as suggested in the comment made 10 years ago at the top of this Talk-page.
--Alan U. Kennington (talk) 14:48, 10 June 2014 (UTC)

I like the approachable character of this page. You have made our life easier with your work. What if we were to transfer it as an introduction in the target page, which is less fun to read. --Ancheta Wis   (talk | contribs) 15:21, 10 June 2014 (UTC)

It would be personally very appealing to me to have a simple page where sequents are explained in a way which non-specialists can discover what sequents are all about. I like making deeply esoteric concepts comprehensible to non-specialists. I can see arguments for and against. One argument for merging is that I was disappointed when I saw the "Sequent" page to see so little information. So I thought I should start adding comments to motivate sequents in a very simple way. Basically that idea that Gentzen's sequents are the units of inference in natural deduction just as tautologies are the unit of inference for the Hilbert style of logical calculus. And similar comments like that. The thing which I felt the "Sequent" page needs is the motivation from the applications to natural deduction. However, then I realised that this is provided in great quantity on the "Sequent calculus" page. So yes, I can see a good reason to have a separate page which is comprehensible to non-specialists (like me, for example). But then one must ask: What should be done with the other dozens of totally esoteric, incomprehensible mathematical logic pages which only specialists can understand? This almost suggests having a parallel wikipedia which explains things to non-specialists. In my opinion, the purpose of an encyclopedia is to explain things to non-specialists. So in a sense, the original purpose has been lost!

Now your idea of adding the Sequent page at the top of the "Sequent calculus" page does not seem so good to me. I think that the highly technical header material on the "Sequent calculus" page should be preceded by an introduction for non-specialists.

Please bear in mind that I have written almost nothing at all of the "Sequent" page. I was thinking that I would start writing more material in the next 24 hours. But I have sort of abandoned that plan because of the abundant material on the "Sequent calculus" page. All that I contributed was a few references which I have found while doing a literature search for this subject in my own 45-book mathematical logic collection.

Conclusion:
I think that what is really needed is a bit of explanatory material in the "Sequent calculus" page. I can see many places where it could be improved. My principal reluctance in this is that the specialists will probably undo most of what I write because it does not fit their view of things.
--Alan U. Kennington (talk) 15:49, 10 June 2014 (UTC)

Trilobite logic

Now I've spent 24 hours improving (I hope) the sequent calculus page. I added a couple of introductory paragraphs in plain English for non-specialists (like me), highlighted some of the text with clearer section headings, and added a few references. So far, so good. However, I think I have discovered a kind of historic discontinuity between the old clunky Gentzen sequent calculus and the modern practical kind of sequent calculus which I have read in the books of Suppes (1957), Lemmon (1965) and Margaris (1967). I cannot find a historic link between the early sequent calculus using tree diagrams and the more modern sequent calculus which looks more like a computer program in nice neat lines with dependency lists (sequent left hand sides) for each line. I think of the Suppes/Lemmon/Margaris approach as dinosaur logic. So to me, the old Gentzen sequent calculus is a kind of trilobite logic.

The Gentzen style of sequent calculus has great historical interest, but it is so far out of date, it's really an embarrassment to talk about it. So ideally I would like to add a section to the sequent calculus page to present the modern style of practical sequent calculus (which by the way, I have shown is semantically sound, but that's another story). However, I cannot really do that because there is a big historical discontinuity between the old and modern styles of sequent calculus. I cannot find any link between them in the 45 books on logic in my personal collection. So I can't link the modern and old sequent calculus styles on that wikipedia page. It is quite possible that Suppes rationalised and modernized sequent calculus some time before 1957. Unfortunately, he gives no references at all in his book. He must have published the development somewhere.

Question:
Can anyone tell me how the Gentzen style of sequent calculus is historically linked to the Suppes (1957) style?

I cannot put the semi-modern Suppes style up on wikipedia unless I can find the historical link. And by the way, the more modern style (which I have developed myself from the Margaris style) is very nice indeed for proving theorems. It's a real breeze and a delight compared to other styles of predicate calculus and FOL that I have used. But wikipedia forbids original research. So you won't be seeing my system here for another 5 years at least. But that's another story....
--Alan U. Kennington (talk) 14:22, 11 June 2014 (UTC)

There may be a way around this. To me, constructivist mathematics and Gentzen go hand in hand, and to me, constructivism is the base for computer programming, i.e., hacking. Based on this I found P. Wadler (1993), "Curry-Howard isomorphism for Sequent Calculus", a private communication which is citation #13, p.75 in Hugo Herbelin (1994). "A Lambda-calculus Structure Isomorphic to Gentzen-style Sequent Calculus Structure" Computer Science Logic 933 (1994) 61--75. Herbelin is already cited in the Curry-Howard isomorphism article citations, along with a provisional history, from which to work backward to Suppes. Probably Suppes has no citations other than Gentzen? --Ancheta Wis   (talk | contribs) 16:29, 11 June 2014 (UTC)

There's a real mystery here. It seems that Patrick Suppes was not a mathematical logician in the normal sense, but more interested in computers and education. Reading between the lines, I think that the reason he came up with such a practical, simple (and correct) sequent calculus was that he was not an academic mathematics logic guy. (I hasten to add that he is still alive and 92 years old. But I doubt he would want to correspond on this issue!) Then Lemmon acknolwedged in his 1965 logic book that he based his ideas on Suppes, thereby producing an excellent book which was used for first year Uni logic in the philosophy department when I was at Uni. (Unfortunately Lemmon died in 1966 when he was about 36 years old.) But Lemmon seems also to not have been a full-on academic logic theorist apart from his modal logic. Then Margaris wrote his book for beginners too, and it's a very clear book also. So all three of these were beginners' introductory works, not the deep theoretical sorts of works.

However, I have just in the last few minutes realised that the Kleene "Mathematical Logic" book (1967) does the Suppes/Lemmon/Margaris style of sequent calculus in a formal way with serious proofs. And Kleene was, of course, a serious academic logician.

Bingo! I've just read the description of Theorem 13 in the Kleene book, and it is directly based on the Gentzen 1934/35 papers. It uses sequents (with only one proposition on the right) as the inputs and outputs to rules in the same way as Suppes/Lemmon/Margaris. Then Kleene gives example theorems using a similar, but slightly more technical, less abbreviated layout.

The odd thing is that this Kleene book is 1967, contemporary with Margaris, but after Suppes and Lemmon. Maybe Suppes and Lemmon just worked it out by intuition, which would not have been difficult. But Kleene presents his practical sequent calculus as theorems, both for psopositional calculus, predicate calculus and first-order logic. Anyway, this is absolutely what I was looking for. Since it makes the direct historical link with Gentzen's sequent methods, and uses the language of Gentzen, and even presents full Gentzen systems later in the book with the full Gentzen-style sequents, I think this material is very worthy of inclusion in the sequent calculus wikipedia page.

Now Kleene does not use the word "sequent" for his logical calculus which uses single-consequent conditional assertions (i.e. single-output sequents). He reserves that word for Gentzen's system with multiple outputs.

So now my question is whether this kind of single-output sequent calculus will be accepted by the specialists who maintain the sequent calculus as genuine. The main value in the Suppes/Lemmon/Margaris/Kleene sequent calculus is that it a wonderfully easy system to learn for doing practical applications to theorems. I've been using it for several months for about 60 theorems of my own, and it's a real dream to use. It's almost impossible to "prove" false theorems with it. Other systems are very vulnerable to errors in the interpretation of free and bound variables. (By the way, I'm writing a book on this subject at the moment.) So this is an applicable version of Gentzen sequent calculus which is probably also entirely usable for theoretical research in metamathematics. That's the impression I get from the Kleene book.

Maybe what I should do is add this Suppes/Lemmon/Margaris/Kleene approach on the sequent wikipedia page, and then if it starts to look good enough, it could be moved into the more specialist-interest sequent calculus page. — Preceding unsigned comment added by Alan U. Kennington (talk • contribs) 17:13, 11 June 2014 (UTC)

---

It turns out that I have been barking up the wrong tree. I've just read the first paper by Gentzen, and it very clearly distinguishes between natural deduction NK (and NJ) systems and sequent calculus LK (and LJ) systems. Even though the Suppes, Lemmon, Margaris and Kleene books clearly use single-succedent sequents, and are not arranged as trees of predicate formulas as in the Gentzen paper, they are also not at all the same as the LK calculus. Strictly speaking, they are a kind of hybrid, but they are called sequential presentations of natural deduction on the natural deduction wikipedia page. That's seems accurate to me, although it is also true to say that they are sub-systems in some sense of the LK sequent calculus.

I conclude that I was mistaken, apparently, in trying to link the "sequential presentations of natural deduction" with Gentzen's sequents, because he emphasized in 1934 that sequents were an alternative to natural deduction, not a special kind of natural deduction. So in terms of the wikipedia page organization, the Suppes/Lemmon/Margaris/Kleene methods do belong there. So I will gradually remove some of the material which I added to the sequent calculus page.
--Alan U. Kennington (talk) 20:25, 11 June 2014 (UTC)

System L and sequents. Should evacuate and redirect this page soon.

First, the material which I had thought of adding to the sequent page is actually already in existence (although only briefly) in the System L article. Therefore I personally have nothing to add to the sequent page.

Second, the word "sequent", according to my literature searches in the last couple of days, is used exclusively in the sense of sequent calculus with disjunctive lists of propositions on the right hand side of the assertion symbol. In other words, the word "sequent" is not applied to the natural deduction style of assertions which always have one and only one proposition on the right of the assertion symbol. (This is unfortunate, because there does not seem to be a standard terminology for such single-output assertions. The word "judgement" or "judgment" seems to be non-standard. It isn't in any of my 45 mathematical logic books.) Gentzen made a crystal clear sharp division between natural deduction with single-proposition outputs and "logistic" deduction with disjunctive output proposition-lists. This sharp division seems to have survived up to the current time.

There is a further division of natural deduction into tree-diagram layout in the old Gentzen style, and tabular layout in the Suppes/Lemmon style, which apparently is called System L, although I have not read any original sources on this system specifically using this name "System L".

Thus there seems to be the following division of the subject.

1. Sequent calculus. All sequents belong in this topic.
2. Natural deduction. This does not use sequents.
   1. Tree-diagram layout. This is most often used in the metamathematical theory literature.
   2. Tabular layout. This is used mostly for the purposes of teaching logic in textbooks. It is also very useful for practical applications by anyone who actually wants to use logic to do some mathematics.

Conclusion:
The set of topics which come under sequent but not under sequent calculus is the empty set. So the sequent page is redundant. — Preceding unsigned comment added by Alan U. Kennington (talk • contribs) 11:58, 12 June 2014 (UTC)

Per Martin-Löf discusses the use of the term 'judgement' in Martin-Löf, Per (1983). "On the meanings of the logical constants and the justifications of the logical laws" (PDF). Siena Lectures. Martin-Löf attributes your observation to a linguistic divide (the English-speaking world neglects Kant), which may be worth an article. --Ancheta Wis   (talk | contribs) 13:49, 12 June 2014 (UTC)

Yes, you are right. Kant is really only known in philosophy departments in the English-speaking world, as far as I know. But most German academics I have met seem to be familiar with Kant. But I think the issue here, in my opinion, is that the word "judgement" (or "judgment" in north America) strongly implies subjectivity in English, which is the opposite of what one wants in mathematical logic! Even in half a dozen philosophical logic books on my bookshelf (e.g. Quine, Körner, Wilder), I cannot find the word "judgment" in the index. (One of them even had Kant in the index!) I'm sure I have never seen it. And it seems to me to be the worst choice of word for it. Surely it is simply a "conditional assertion". How can it be anything else?

Anyway, getting back to business, I have started trying to extract some things of some value from the sequent page to put in the sequent calculus page, in preparation for retiring the sequent page. I have also added a clear distinction between natural deduction and sequent calculus on the sequent calculus page. This could be helpful to people who know even less than I do! There must be such people out there somewhere!! — Preceding unsigned comment added by Alan U. Kennington (talk • contribs) 15:10, 12 June 2014 (UTC)

Other-language versions of the sequent page

One argument in favour of the retention of the "sequent" page is that fact that it is translated literally into three other languages, namely Spanish, Japanese and Chinese. The "sequent" page in Italian has more information than the English-language page, including many of the inference rules expressed in numerator/denominator form, while the Russian page has almost no information at all.

The argument against retaining the "sequent" page in English is that the true sequent has disjunctive semantics for multiple propositions on the right hand side, and therefore the "sequent" topic is a subset of the "sequent calculus" topic. It is not possible to explain a sequent without also explaining "sequent calculus". It's like trying to explain a screwdriver without also explaining what a screw is! The one makes no sense without the other.

However, if one did wish to retain the "sequent" page as a separate page, it could be a useful place to explain the difference between a sequent and a simple conditional assertion with only one proposition on the right. There is currently no wikipedia page for "conditional assertion". In fact, if you do a search for it with double-quotes, you get the text which I wrote myself on the "sequent" page. So I think this would be an excellent place to clarify the categories of assertions:

1. Unconditional assertion.
2. Simple conditional assertion.
3. Sequent.

This would parallel the text which I added to the "sequent calculus" page to clarify the difference between:

1. Hilbert-style logical calculus.
2. Natural deduction.
3. Sequent calculus.

The "sequent calculus" contains many confusing technicalities for non-specialists. This is an argument in favour of having a less technical "sequent" page.

Another thing that could be clarified on the "sequent" page is the curious notion of a "judgement" or "judgment" (which is spelled very inconsistently on wikipedia). This is not familiar to most people in the logic area, in my opinion. There is no point in explaining assertions in terms of "judgments" if the word "judgment" is even less familiar to readers than the word "assertion". Normally an encyclopedia should explain less well-known words in terms of more well-known words!
--Alan U. Kennington (talk) 04:00, 15 June 2014 (UTC)

The distinction between the sequent page and the sequent calculus page.

After doing some editing of the sequent page for a few days (and doing some concomitant research of the literature), it seems to me now that there is a distinct role for a sequent page as opposed to the sequent calculus page. The distinction is more or less analogous to the distinction between the proposition page and the propositional calculus page. The sequent and proposition pages deal with just the logical concepts themselves, and their meanings, whereas the corresponding calculus pages are concerned more with the detailed rule-sets for the respective calculi and the theoretical properties and implications of such calculi.

Therefore it seems to me now that the sequent page should not be deleted. It does have a useful role. This is particularly so because the rule-sets and properties on the sequent calculus page are really incomprehensible to non-specialists, and in fact it is an esoteric subject. For the non-specialist, it is the natural deduction systems along the lines of Lemmon's System L which are more comprehensible and relevant outside the mathematical logic research context.
--Alan U. Kennington (talk) 07:56, 17 June 2014 (UTC)

Assertion symbols in sequents do not signify provability.

It is currently stated in the "Interpretation" section that the assertion symbol "⊢" in a sequent signifies provability. This is true in modern model theory, but certainly not in Gentzen's 1930s sequent calculus. To explain this, it must be noted that Gentzen originally used "→" in sequents instead of our modern "⊢", and he used "⊃" to mean the implication operator which we nowadays would write as "⇒" or "→". Gentzen definitely knew the difference between provability and implication in the modern sense, but he asserted very clearly that his assertion symbol was a synonym for the implication operator. In other words, it was very definitely not a provability assertion. On page 180 of his 1934 paper, Gentzen wrote:

2.4. Die Sequenz A₁, ..., A_m → B₁, ..., B_n bedeutet inhaltlich genau dasselbe wie die Formel

(A₁ & ... & A_m) ⊃ (B₁ ∨ ... ∨ B_n).

That is totally categorical and clear (especially if you know German!). Gentzen made not the slightest distinction between the assertion symbol and the implication operator. In fact, his sequent calculus was all about the provability of sequents from other sequents. That was in fact the real innovation in sequent calculus, replacing unconditional propositions with conditional propositions as the unit of inference. Never ever does he regard the assertion symbol inside a sequent as a provability assertion.

This point of view is 100% agreed with by Alonzo Church, "Introduction to mathematical logic", Princeton University Press, Princeton, New Jersey, 1944, 1956, 1996, ISBN 978-0-691-02906-1. If you look on page 165, you will see the following.

Employment of the deduction theorem as primitive or derived rule must not, however, be confused with the use of Sequenzen by Gentzen. For Gentzen's arrow, →, is not comparable to our syntactical notation, ⊢, but belongs to his object language (as is clear from the fact that expressions containing it appear as premisses and conclusions in applications of his rules of inference).

Once again, this is categorical and clear. So I am mystified that anyone could write in the sequent wikipedia article that the implication symbol in a sequent signifies provability. It clearly does not, and I am not aware of any literature (apart from wikipedia) which makes this claim, even in more modern literature.

I can only conjecture that the author of the paragraphs in the sequent page claiming that the turnstile signifies provability must have been confusing sequents with modern model theory, where the symbol "⊢" signifies provavility, and the symbol "⊨" signifies semantic implication, i.e. that the consequences follow from the assumptions in all models, but not necessarily within a given first-order language.

I am reluctant to tread on anyone's toes by deleting the claims on the sequent page about the provability meaning for the sequent symbol "⊢". However, I do want to just note here that the evidence seems to be very much against it. — Preceding unsigned comment added by Alan U. Kennington (talk • contribs) 05:58, 19 June 2014 (UTC)

As you likely know, the protocol in this case is to

1. Identify the statements, which you have done.
2. Isolate or tag these statements.
3. This can be done with inline tags, such as "citation needed": {{cn}}, or "discuss": {{discuss}}, etc.
4. Wait for the originator to respond. Usually, if the originator is still active, you would expect some response soon.
5. If no one has responded, in say a week, then announce it on the Mathematics Project, if you have not done so already.
6. In the meantime, you/(we editors) can lay the groundwork for changes to the tagged items.
7. Likely, no one will have responded, say by an explanation, or with a go-ahead.
8. In that case, proceed as you have planned. By convention, the originator will abide by the actions undertaken in behalf of the encyclopedia.

The case you make, based on the citations you have found, specifically showing the evolution from Gentzen 1934,35, is likely to stand. I would think the originator will abide by your work, and I look forward to your edits.

But it appears that we can email the original editor of this article, who has expressed interest in being apprised of changes (he has chosen not to watch the article, apparently, but he updates his contact information on his web site). This might prove more efficient for you than the eight-step list above. →Ancheta Wis   (talk | contribs) 12:33, 19 June 2014 (UTC)

Apparent shift of paradigm?

Although Gentzen 1934/35 and Church 1944/58 are crystal clear in saying that "⊢" is the same as "⇒", which is part of the object language, not the metalanguage, there may have been a "shift of paradigm"! Curry 1963/76, page 184, and Lemmon 1965, page 12, seems to say fairly clearly that "⊢" signifies provability. (However, Lemmon defined sequents to be single-assertion natural deduction style conditional assertions only.) My suspicion is that the developments in model theory during later decades led to a reinterpretation of history. Gentzen's original paper was saying anyway that the system was complete, and therefore there was no difference between syntactic and semantic implication. So it did not make any difference at that time, and model theory had not really started as a serious mathematical subject as it is today.

So I think there may be two paradigms: the classical paradigm and the modern paradigm. Although Margaris (1967) did not talk about sequents, he did present a kind of natural deduction in his book, and definitely he defined "⊢" to signify provability.

I think it would be very interesting to trace where the paradigm shift happened exactly, and who did it!
--Alan U. Kennington (talk) 18:09, 19 June 2014 (UTC)