Understanding the ⊢ notation and context in Natural Deduction vs Sequent Calculus

Question

I'm trying to understand how to interpret the turnstile notation Γ ⊢ A when it appears in natural deduction systems, and I'm confused about the relationship between natural deduction and sequent calculus. My current understanding:

In natural deduction (as originally formulated by Gentzen), contexts are not explicitly written, and assumptions are tracked implicitly through the proof tree structure In sequent calculus, the turnstile ⊢ is used as a sequent separator, with contexts explicitly manipulated Gentzen's original natural deduction didn't use turnstile notation and didn't explicitly handle contexts

What's confusing me: I've encountered modern presentations of natural deduction (like on Wikipedia's Natural Deduction page) that use notation like:

Γ ⊢ π1 : A Γ ⊢ π2 : B
───────────────────────── ∧I
Γ ⊢ (π1, π2) : A ∧ B

This looks like sequent notation, but it's being called natural deduction. My questions:

1. When Γ ⊢ A appears in a "natural deduction" system, should this be understood as a sequent, or is it just a notational convenience?
2. If modern natural deduction uses explicit contexts with ⊢, what exactly distinguishes it from sequent calculus? Is it purely the style of inference rules (e.g., natural deduction only grows contexts, while sequent calculus can directly manipulate them with left rules)?
3. In traditional natural deduction without explicit contexts, is it correct to say that "the context is just whatever formulas appear above in the proof tree"? If so, does the sequent-style notation in natural deduction (with explicit Γ) provide the same advantage as sequent calculus—namely, making rules local by eliminating the need to traverse the entire proof tree to track context?
4. When natural deduction uses sequent-style notation with contexts but doesn't manipulate contexts the way sequent calculus does, what's the purpose of writing the context explicitly?

I'm trying to understand whether these are fundamentally different proof systems or just different notational presentations of similar ideas, and when it's appropriate to call something "natural deduction" vs "sequent calculus."

• Naïm Camille Favier: As a point of data, there's an informal discussion of natural deduction vs sequent calculus in Mike Shulman's notes on categorical logic. Both are phrased in terms of sequents, but the distinction seems to be about right and left rules.

Answer 1

1. When Γ ⊢ A appears in a "natural deduction" system, should this be understood as a sequent, or is it just a notational convenience?

Sequent.

2. If modern natural deduction uses explicit contexts with ⊢, what exactly distinguishes it from sequent calculus? Is it purely the style of inference rules (e.g., natural deduction only grows contexts, while sequent calculus can directly manipulate them with left rules)?

There is no formal definition of what constitutes a sequent calculus and what a natural deduction system.

But typically, for each connective (or quantifier, in first-order logic, etc.), a sequent calculus has a pair of left and right introduction rules, whereas a natural deduction calculus has a pair of introduction and elimination rules (on the right).

Also, a natural deduction system always has a single formula on the right-hand side of the sequent, whereas sequent calculi (at least for classical logic, though possibly for intuitionistic logic as well) typically allow multiple (or zero) formulas on the RHS (so the "context" is really two-sided). (There are also "Tait-style" sequent calculi that only have the RHS, so to speak.)

3. In traditional natural deduction without explicit contexts, is it correct to say that "the context is just whatever formulas appear above in the proof tree"?

The "context" would consist of undischarged assumptions on leaves above the current node, not all formulas.

If so, does the sequent-style notation in natural deduction (with explicit Γ) provide the same advantage as sequent calculus—namely, making rules local by eliminating the need to traverse the entire proof tree to track context?

I’d say yes.

4. When natural deduction uses sequent-style notation with contexts but doesn't manipulate contexts the way sequent calculus does, what's the purpose of writing the context explicitly?

I’m not sure I understand this question. The contexts are needed for completeness of the system. Natural deduction does manipulate the contexts: cf. the implication introduction rule $$\dfrac{\Gamma,{\color{blue}{A}}\vdash B}{\Gamma\vdash A\to B}$$ or the disjunction elimination rule $$\dfrac{\Gamma\vdash A\lor B\qquad\Gamma,{\color{blue}{A}}\vdash C\qquad\Gamma,{\color{blue}{B}}\vdash C}{\Gamma\vdash C}$$ where parts of the context that change are indicated. (Depending on the exact set-up, the disjunction elimination rule may even be written in a "split-context" way where each of the three premises use possibly different contexts that are collected in the conclusion.)