Updated Question

I'm following Interactive Tutorial of the Sequent Calculus which states the rules for "backwards" deduction and comparing it to the rules for "forward" natural deduction as stated in the Wikipedia Sequent Calculus article.

In general, if the "forward" rule is written as:

$$S_0 \over S_1$$

then the corresponding "backward" rule is written as:

$$S_1 \over S_0$$

For example, the "forward" rule for ${\wedge}R$ is written as (in the Wikipedia article):

$$\Gamma \vdash, \Delta, A \wedge B \over \Gamma \vdash \Delta, A \qquad \Gamma \vdash \Delta, B$$

while the corresponding "backward" rule is written as (in the interactive tutorial, see the summary section at the bottom):

$$\Gamma \vdash \Delta, A \qquad \Gamma \vdash \Delta, B \over \Gamma \vdash, \Delta, A \wedge B$$

Whereas the "forward" deduction system works from top sequents to bottom sequents, the "backward" deduction system works from the bottom sequents to the top sequents -- so isn't it the same? Instead of writing things from top to bottom, we're writing things from bottom to top and applying flipped rules to account for this. Am I correct?

The Interactive Tutorial of the Sequent Calculus also states the rules for using quantification in "backwards" deduction as follows:

$$\forall$$ $$\Gamma, P(z) \vdash \Delta \over \Gamma, \forall xP(x) \vdash \Delta$$ $$\Gamma \vdash P(x), \Delta \over \Gamma \vdash \forall xP(x), \Delta$$
$$\exists$$ $$\Gamma, P(x) \vdash \Delta \over \Gamma, \exists xP(x) \vdash \Delta$$ $$\Gamma \vdash P(z), \Delta \over \Gamma \vdash \exists xP(x), \Delta$$

These look like the quantifier rules of LK Calculus. Are they? If not, then these rules are part of the "backward" natural deduction -- are there equivalent "forward" natural deduction rules for quantifiers?

Original Question

I'm following along to Interactive Tutorial of the Sequent Calculus. It seemingly has the inference rules of "backwards" deduction. E.g. it states ${\wedge}R$ as:

$$\Gamma, A, B \vdash A, \Delta \qquad \Gamma, A, B \vdash B, \Delta \over \Gamma, A , B \vdash A \wedge B, \Delta$$

By contrast, Wikipedia's Sequent Calculus article lists the "forward" natural deduction ${\wedge}R$ as:

$$\Gamma' \vdash, \Delta', A \wedge B \over \Gamma' \vdash \Delta', A \qquad \Gamma' \vdash \Delta', B$$

In the natural deduction version, if you let $\Gamma' = \Gamma, A, B$ and $\Delta' = \Delta$ and flip the sequents (top to bottom, bottom to top), then you get the "backward" deduction rule.

I find the statement of the "backward" deduction rules odd though and harder to apply. They don't seem as general - not because of the flipping, but because of the extra $A, B$ in the hypotheses. Are they equivalent? Is it ok to remove the extra $A, B$?

Another weird statement of a rule is the way the tutorial states the "backwards" ${\neg}L$:

$$\Gamma, A \vdash A, \Delta \over \Gamma, A, \neg A \vdash \Delta$$

What's weird is that under the line is a contradiction ($A \wedge \neg A$). Is it me, or does this make the rules harder to apply?

Why are the rules stated this way?

  • 1
    $\begingroup$ Where did you see above "weird" inference rule in your linked ref? I only see similar rules as wikipedea article's in the Summary section... Do you mean those in the Branching rules section? $\endgroup$ Dec 3, 2021 at 1:32
  • 1
    $\begingroup$ It looks to me like the rules in the Wikipedia table that you call "forwards" are simply written upside-down for no discernible reason. $\endgroup$ Dec 3, 2021 at 2:29
  • 1
    $\begingroup$ If you further read the wiki article to all the rules of LK section, ∧R rule is same as your interactive source. $\endgroup$ Dec 3, 2021 at 2:29
  • 1
    $\begingroup$ Note in your quoted wikipedea source the rule actually is written as R∧ rule, you inadvertently wrote as ∧R... But in LK section the wikipedea writes the usual ∧R rule. Seems wikipedea authors intentionally flip here. $\endgroup$ Dec 3, 2021 at 2:35
  • 1
    $\begingroup$ As for the "backwards" "forward" rules for quantifiers, these are standard corresponding L/R rules in LK and match wikipedea source. Recall L rules are elim-rules in ND while R rules are intro-rules in ND, you can regard "backwards" here as our main proof search strategy, you don't need to match exactly to L/R rules, it all depends on your goal form based on which you just choose either L or R rules. All rules of LK is listed there already (not that many), no more other "forward/backward" rules. $\endgroup$ Dec 3, 2021 at 2:53

1 Answer 1


There's nothing weird here, from your reference it states about backwards deduction feature of sequent calculus:

In order to show A ∨ B ⊢ A, B is true, you need to show A ⊢ A, B is true and B ⊢ A, B is true." Notice that in both of the subgoals, there no longer is a disjunction; in sequent calculus, we use backwards deduction to get rid of logical operators until we have atomic clauses.

So the author is emphasizing how to use sequent calculus inference rules to get rid of logical connectives in your goal $\Gamma, A , B \vdash A \wedge B, \Delta$ which contains a conjunction. Recall in SC we can have some admissible/derivable rules, but in your above case you can simply view the whole $\Gamma, A , B$ on the left of the turnstile as a multiset $\Gamma'$, then this is just the conventional $\land$ R rule.

As for contradiction on the left of turstile, it's explosion, so any $\Delta$ simply follows...

  • $\begingroup$ thanks! I rewrote the question. Should I post it or edit this one, but keep the current question to give this answer context? $\endgroup$
    – joseville
    Dec 3, 2021 at 2:16
  • 1
    $\begingroup$ @joseville If no new question, you can of course edit an existing post. Post a new question if you still have some lingering unanswered question. $\endgroup$ Dec 3, 2021 at 2:16

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .