2
$\begingroup$

I've read somewhere that the cut rule in sequent calculus $$\frac{A \vdash \mathbf{C}, B \qquad A',\mathbf{C} \vdash B'}{A,A' \vdash B,B'} (\text{cut})$$ states that the $\mathbf{C}$ on the right is stronger than $\mathbf{C}$ on the left.

I would like to know what is this notion of strongness and how is $\mathbf{C}$ on the right stronger than $\mathbf{C}$ on the left.

Improve this question
$\endgroup$
4
  • $\begingroup$ My guess is that there is no real notion of "strongness", and "stronger" used in the above example is just a common terminology (without any real basis to call it so). $\endgroup$
    – Wojowu
    Jan 27, 2015 at 11:37
  • $\begingroup$ @Wojowu I suppose that it may not be without any real basis as the author was comparing the Identity axiom and the cut rule stating that in case of Identity axiom C⊢C, the C on the left is stronger than C on the right whereas in cut rule it is the converse. $\endgroup$
    – rsharma
    Jan 27, 2015 at 13:48
  • 2
    $\begingroup$ This seems hard to answer without knowing the context. That's not a common slogan. $\endgroup$
    – Henry Towsner
    Jan 27, 2015 at 14:08
  • $\begingroup$ @HenryTowsner For the complete context you can refer to section 5.1.4 (page 30-31) of this document cs.brandeis.edu/~cs112/2006-cs112/docs/… $\endgroup$
    – rsharma
    Jan 27, 2015 at 14:18

1 Answer 1

Reset to default
4
$\begingroup$

First, by "stronger than", Girard means "at least as strong as". So the identity rule can be read as saying "If you have a C on the left side, you can have C on the right side as well (because you can use the identity rule to derive them)", and in that sense "a C on the left is as good as having a C on the right".

And by that reading, the cut-rule could be interpreted as saying "If you have a C on the right, you can have a C on left (because you can cut them away using cut)".

Improve this answer
$\endgroup$
2
  • $\begingroup$ Thank you very much for the answer. Also, could you help me understand what does the author mean by "signature" in section 5.2.3 paragraph-2 of the document $\endgroup$
    – rsharma
    Jan 27, 2015 at 19:23
  • $\begingroup$ The term is defined right there in the paragraph, thought not as clearly as it might be. The idea is that P is positive (signature 1) in "P", is negative (signature -1) in "$P\rightarrow\phi$", positive again in "$(P\rightarrow\phi)\rightarrow\psi$", and so on. $\endgroup$
    – Henry Towsner
    Jan 27, 2015 at 21:03

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