4
$\begingroup$

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.

$\endgroup$
1
  • 1
    $\begingroup$ It might be worth noting where you read this rule, since there are many many variants of every logic (even if they end up equivalent). $\endgroup$
    – S.C.
    Jul 3 at 11:32

3 Answers 3

6
$\begingroup$

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

$\endgroup$
0
5
$\begingroup$

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

$\endgroup$
3
  • $\begingroup$ I know the first rule u meantioned, it may called multiplicative form that premises have different contexts, my version is additive form that have same contexts, but its doesnt matter about what i asked. It seems that you all misunderstand what i mean, i should update my question... $\endgroup$
    – maplgebra
    Jul 3 at 14:58
  • $\begingroup$ @maplgebra Sorry, but I think that my answer as well as the answer of S.C. does answer your question. You ask: "why we can not just remove $A \supset B$ from context of left premise make it more simpler?" The answer is that you can remove $A \supset B$ from the context, but only if your calculus contains the rule of Contraction. Conversely, the point of including $A \supset B$ is to allow you to drop the rule of Contraction. $\endgroup$
    – Pilcrow
    Jul 3 at 19:49
  • $\begingroup$ Oh I got u, thats really a good perspective! My bad, i should give more details about the context of calculus. $\endgroup$
    – maplgebra
    Jul 4 at 4:48
3
$\begingroup$

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.
$\endgroup$
1
  • $\begingroup$ Sorry my bad, did not make this question clear, i just updated it, can u check it again? $\endgroup$
    – maplgebra
    Jul 3 at 15:07

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.