The simplication of left implication rule in intuitionistic sequent calculus

Question

The original left implication rule in sequent calculus for intuitionistic logic is

$$ \dfrac{\Gamma, A \supset B \vdash A \quad \Gamma,A \supset B, B \vdash C}{\Gamma, A \supset B \vdash C} $$

There is a simplified version of it:

$$ \dfrac{\Gamma, A \supset B \vdash A \quad \Gamma, B \vdash C}{\Gamma, A \supset B \vdash C} $$

I can understand why we can remove $A \supset B$ in right primise, since $\vdash B \supset(A \supset B)$. but why we can not just remove $A \supset B$ from context of left primise make it more simpler? that means there must exist some proofs of $A$ make use of $A \supset B$, but i can't find out some proofs like that.

My question is from the lecture https://web2.qatar.cmu.edu/cs/15317/lectures/09-simplified.pdf, there exists a discussion about how to simplify the left implication rule.

On the left premise, can a proof of $A$ make use of $A \supset B$ ? Definitely. Maybe it is the case that $A$ involves a choice, and we can choose one option at the first application of $\supset L$ and another option at the second application.

I can't understant what this mean.

Answer 1

This sort of thing is what makes some of the structural rules of sequent calculus admissible, meaning that they can be proven (in a particular sense), rather than needing to assert them separately.

Here, leaving $A \supset B$ in the premises means that we can use it again farther up in the proof. This means that we don't need to use a contraction rule to duplicate $A \supset B$ if we want to use it twice.

If something similar is done with all the other rules, then contraction becomes admissible: whenever we have a derivation of $\Gamma, A, A, \Delta \vdash B$, we can prove that there is a derivation of $\Gamma, A, \Delta \vdash B$ too. In particular, if we have a proof that uses $A \supset B$ twice, then there's a proof that only uses it once too.

---

To understand why $A \supset B$ can be removed from $\Gamma, A \supset B, B \vdash C$, but not $\Gamma, A \supset B \vdash A$, let's try proving that any derivation of $\Gamma, A \supset B, B \vdash C$ can be turned into a derivation of $\Gamma, B \vdash C$.

To do this, we'll use the cut rule, which can then be eliminated.

$$ \dfrac{ \dfrac{ \dfrac{}{\Gamma, B, A \vdash B}\text{(init)} }{ \Gamma, B \vdash A \supset B} \text{($\supset$R)} \quad \dfrac{...}{\Gamma, A \supset B, B \vdash C} } { \Gamma, B \vdash C } \text{(cut)} $$

The "$...$" at the top stands for the given proof of $\Gamma, A \supset B, B \vdash C$.

---

However, proofs of $\Gamma, A \supset B \vdash A$ can use $A \supset B$ in an essential way. The text you link gives the example of a proof of $\vdash \neg \neg (A \vee \neg A)$. Let's take a look. Just a reminder that these proof trees are constructed from the bottom up, so that may help you understand where the derivation comes from.

$\neg A$ is a shorthand for $A \supset \bot$, so we'll start by expanding that.

$$ \dfrac{ \dfrac{ \dfrac{...} {(A \vee \neg A) \supset \bot \vdash A \vee \neg A} \quad \quad \dfrac{} {(A \vee \neg A) \supset \bot, \bot \vdash \bot} \quad \quad \text{$\bot$L} }{ (A \vee \neg A) \supset \bot \vdash \bot } \quad \text{$\supset$L} } {\vdash ((A \vee \neg A) \supset \bot) \supset \bot } \quad \text{$\supset$R} $$

At this point in the proof (at the "$...$"), we have a choice. We can either prove $A$ or $\neg A$ using $(A \vee \neg A) \supset \bot$. As it happens, we can use $A$ to prove $A \vee \neg A$ and then our premise to prove $\bot$, which means that we can prove $\neg A$.

Continuing the proof from there,

$$ \dfrac{ \dfrac{ \dfrac{ \dfrac {\dfrac{}{(A \vee \neg A) \supset \bot, A \vdash A} \quad \text{init}} {(A \vee \neg A) \supset \bot, A \vdash A \vee \neg A} \quad \text{$\vee$R$_1$} \dfrac{} {\quad (A \vee \neg A) \supset \bot, A, \bot \vdash \bot} \quad \text{$\bot$L} } {(A \vee \neg A) \supset \bot, A \vdash \bot} \quad \text{$\supset$L} }{ (A \vee \neg A) \supset \bot \vdash A \supset \bot } \quad \text{$\supset$R} }{ (A \vee \neg A) \supset \bot \vdash A \vee \neg A } \quad \text{$\vee$R$_2$} $$

So we used the premise $(A \vee \neg A) \supset \bot$ twice. The second time, we had an $A$ in the context which meant that we could make a different choice when proving $A \vee \neg A$.

Answer 2

There are several variants of this rule. One of them is indeed: $$ \dfrac{\Gamma \vdash A \quad \Delta, B \vdash C}{\Gamma, \Delta, A \supset B \vdash C} $$ In such a calculus, one would typically also have the rule of Weakening: $$ \dfrac{\Gamma \vdash A}{\Gamma, B \vdash A} $$ and the rule of Contraction: $$ \dfrac{\Gamma, A, A \vdash B}{\Gamma, A \vdash B} $$ Alternatively, one can have a calculus with your rule: $$ \dfrac{\Gamma, A \supset B \vdash A \quad \Gamma, A \supset B, B \vdash C}{\Gamma, A \supset B \vdash C} $$ Observe that in this rule the context $\Gamma$ is the same in both premises, whereas in the previous version of the rule you have two different contexts $\Gamma$ and $\Delta$.

The advantage of this second rule is that the rule of Contraction now becomes admissible. This means that if the sequent $\Gamma, A, A \vdash B$ is derivable, then so is $\Gamma, A \vdash B$. The rule of Contraction can therefore be dropped from the calculus. Ultimately, the benefit of this is that it simplifies the proof of Cut elimination (dealing with Contraction is the most difficult part of the proving Cut elimination for intuitionistic logic).

Answer 3

A couple of footnotes to the answers from @Pilcrow and @S.C. which already make the main point.

1. For what it is worth, the rule you give is in fact not the “original'' left implication rule, if Gentzen’s system LJ counts, as it surely does, as the original sequent calculus for intuitionistic logic.
2. For an excellent treatment, accessible but detailed, of the sequent calculus for intuitionistic logic, which elaborates on the rationale for tinkering with Gentzen’s left rule for the conditional, see Ch. 2 of Sara Negri and Jan von Plato's invaluable Structural Proof Theory.