Heh, don't know much about the sequent calculus - have only really messed around with natural deduction. Takes a long time to get my head around the judgements though - especially if they aren't presented in a syntax-directed style.
Conversation
Yeah me too - I think sequent calculus can have multiple conclusions to the right of the turnstile? But I think there are deeper things than that - I've just never seen a side-by-side comparison. I think for whatever reason in PL research natural deduction is more popular?
2
I really don't understand the explanation here, which seems to try to distinguish it from natural deduction: ncatlab.org/nlab/show/sequ
1
has attempted to explain it to me in the past - something to do with in natural deduction you can make your proof tree get larger as you attempt to get to the leaves? So it's harder to know if you are going to finish or not? I might have got that wrong though. 😬
1
The most usual way to understand the difference, ime, is to call something "natural deduction" when it uses intro and elim rules, and "sequent calculus" when it uses only intro rules.
1
2
Typically sequent calculi allow you to introduce formulas in different locations, which is how you (roughly) get the effect of intro and elim.
1
1
Number of conclusions is a red herring; you get both kinds of system with different options here. And while the paradigms of each are pretty different, you definitely get systems that blur the line as well.
1
1
Another common feature: cut elimination is usually pretty straightforward for ND systems, and long and involved for SC---and it gives you interesting corollaries in SC but not ND.
3
2
Or: think about destructors for pairs. Fst(pr) and snd(pr) are the usual ND way; let <x, y> = pr in E is the usual SC way.
2
2
ah yeah I think I remember that stuff from the negative vs positive presentations of types like dependent pairs? ncatlab.org/nlab/show/depe
A little delicate, since nothing there is quite SC-ey. But if you move the premise p from their positive elim rule to antecedent position in the conclusion, you'd have an SC-style rule, introducing Sigma on the left.
1