# Sequents and Consequences

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.

• Sequent Calculus is a proof system with a peculiar formalization. Formulae are the "usual" ones, written wit connectives (like: $\lnot, \to$) and quantifiers, but the "basic object" of the calculus is not the formula but the sequent: $\Gamma \vdash \Delta$, where $\Gamma$ and $\Delta$ are sets of formulas and the "turnstile" $\vdash$ express the relation of consequence. Commented Apr 24, 2017 at 13:52
• 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 $\to$-R (corresponding to $\to$-intro) : from the sequent: $\Gamma, A \vdash \Delta,B$ the new sequent $\Gamma \vdash \Delta, A \to B$ can be derived. Commented Apr 24, 2017 at 13:55
• I thought sequents are not sets as (as hyperlinked for sequents under the question). Does that mean that deduction theorem written in sequent form (for the i.e.) is different than that of the other form? Commented Apr 24, 2017 at 16:23
• I did not know that. I know what those are! Isn't the deduction theorem <en.wikipedia.org/wiki/Deduction_theorem> as shown here not a multiset though because of the union? Commented Apr 24, 2017 at 16:30
• One more question if you can answer it in the answer box that will be fantastic! If you have a syntactic consequence as shown here, en.wikipedia.org/wiki/Logical_consequence are these multisets? That would make complete sense if that was a multiset. The union part makes sense then. Commented Apr 24, 2017 at 16:35

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.

• I appreciate all your help! Makes sense now. Commented Apr 24, 2017 at 16:45