"forward" natural deduction vs "backward" natural deduction

Question

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:

	L	R
$$\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?

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...