Sequents and Consequences

Question

Recently I posted a question concerning the Deduction Theorem. However, I have seen rules written in sequent notation as well (i.e. φ⊢ψ⊢φ→ψ). I am confused as how the two are related. Particularly, I am wondering what is the difference between consequences and sequents. I have seen modus ponens and a lot of inference rules written in sequent notation. Can you write these rules as consequences (for example sets) as well? Any help would be greatly appreciated.

Answer 1

Sequent Calculus is a proof calculus with a peculiar formalization.

Formulas are the "usual" ones, written wit connectives (like: $¬,→$) and quantifiers, but the "basic object" of the calculus is not the formula but the sequent: $Γ⊢Δ$, where $Γ$ and $Δ$ are multisets of formulas and the "turnstile" $⊢$ express the relation of consequence.

The rules of the calculus are stated in term of sequents and they formalize the way we can "transform" one or more sequents into a new one, like the rule for $→$-R (corresponding to $→$-intro of Natural Deduction):

$$\dfrac {Γ,A ⊢ Δ,B}{Γ⊢Δ,A→B}$$

that reads: from the sequent: $Γ,A ⊢ Δ,B$ the new sequent $Γ⊢Δ,A→B$ can be derived.

As you can see, this rule embeds the feature of the Deduction Theorem.

The same is for Natural Deduction with the $→$-intro rule.