Can I derive $ \vdash \Gamma $ from $ \vdash \Gamma, A, A^\bot $?

108 Views Asked by At

The Wikipedia article on linear logic mentions the following as an initial sequent:

$$ \over \vdash A, A^\bot $$

As far as I can understand from informal descriptions of linear-logic semantics, this would also be valid...

$$ \vdash \Gamma \over \vdash \Gamma, A, A^\bot $$

...because the $A$ and the $A^\bot$ would cancel each other out. But I don’t see an explicit rule to that effect and I don’t see how it can be derived from the given rules.

Is the latter derivation just entailed by the overall rules of sequent calculus, or is there a proof for it that I’m not seeing, or is it in fact invalid?

1

There are 1 best solutions below

1
On BEST ANSWER

Your question does not correspond to your title: actually you are asking if one can derive $\vdash \Gamma, A, A^\bot$ from $\vdash \Gamma$. It is the case if one adds the mix rule: http://llwiki.ens-lyon.fr/mediawiki/index.php/Sequent_calculus#Mix_rules Otherwise, it is not the case.