Want to take part in these discussions? Sign in if you have an account, or apply for one below
Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.
some bare minimum at cut rule
I put in a remark about the nullary analogue (which I called the ‘identity rule’, although it goes by various names).
In my experience with Gentzen-style sequent calculi, there is not typically an ’identity rule’ for all formulas, but only the identity axiom for the variables. Instances of identities for more complicated formulas are derived; e.g., for implications $a \multimap b$ we have a derivation
$\frac{\frac{a \vdash a\; \; \; b \vdash b}{a \multimap b, b \; \vdash \; a}}{a \multimap b \; \vdash \; a \multimap b}$I can see why you call the identity rule a nullary analogue of the cut rule (inasmuch as identity arrows are nullary compositions). It is interesting that Girard views identities as dual to cuts (roughly in the same way that an arrow $\top \to \neg A \wp A = A \multimap A$ that names the identity is dual to the arrow $\neg A \otimes A \to \bot$ that implements an evaluation). In the one-sided version of MLL, it looks something like this:
$\frac{}{\vdash \neg A, A} \; identity \qquad \frac{\vdash \Gamma, \neg A \;\;\; \vdash \Delta, A}{\vdash \Gamma, \Delta} \; cut$You only need an identity axiom for the variables precisely because the more general identity rule may be proved. For the same reason, Gentzen's sequent calculi do not need a cut rule. But in both cases, it's vital that the missing rule can be proved, since after all people do use them!
Okay, so we agree it’s a derived (or derivable) rule in that set-up, not an axiom or a basic rule of inference. That’s all I meant to say (and should have said). What you wrote is fine, just as long as everyone is clear on that point.
Actually, let me draw you out a little more here. Could you give more details what you mean where you wrote “Typically, a cut-elimination theorem will also eliminate the identity rule…”? I’ve never heard it put that way. I know how to eliminate cuts (by progressively “pushing them back” towards the axioms), and I know how to “eliminate” identities (again pushing them back, in favor of identities on subformulas), but it looks to me like these two schemes are treated separately. One has to do with rewriting binary compositions, and the other has to do with rewriting nullary compositions.
So my question is: how do you understand “eliminating identities” as part of eliminating cuts?
Could you give more details what you mean where you wrote “Typically, a cut-elimination theorem will also eliminate the identity rule…”?
What I really mean is that one proves both results (cut elimination and identity elimination) in the same way, one can usually prove the latter whenever one can prove the former (and in fact I would be surprised to see an exception in any formal system not created ad hoc just to be an exception), and that one should view the two results together. It is much like saying that an associative algebra typically has a unit (although at least there are naturally occurring exceptions to that).
For what it’s worth, I also found the wording here a bit strange, in part because I have seen descriptions of the cut-elimination algorithm which also eliminate identity axioms, and that always struck me as conflating two different ideas. I am used to thinking of these as two separate theorems (admissibility of the cut rule and admissibility of the identity rule), which indeed go hand-in-hand and are in a certain sense dual (elimination of cuts being analogous to $\beta$-reduction in natural deduction, and elimination of identities analogous to $\eta$-expansion).
Thanks for the reminder, Noam!
I’ve done a little editing at cut rule, expanding the idea section, and taking into account the discussion above into other sections. Please see what you think.
Very nice, Todd!
It's more than just an analogy between the identity rule and eta expansion, so I put in a bit about that. (The connection between cut and beta reduction is fuzzier in my mind.)
Thanks for that bit, Toby!
I added an example of reducing a cut on $A \multimap B$, to go along with the example of expanding an identity on $A \wedge B$. As for the analogy with eta/beta, I agree that it’s a strong analogy, but it’s not quite exact. (Typically, eta expansion is a principle which applies to open terms $t : \Gamma \to A$ or contexts $k : A \to \Delta$, depending on the polarity of $A$.) I hope the parenthetical remark after the examples is suggestive enough.
Thanks for the addition, Noam. I added just a few more words to the examples section.
I added the quote
“A logic without cut elimination is like a car without an engine” – Jean-Yves Girard
to cut rule. I don’t know where this quote is from, though I’ve seen it in a couple of places; does anyone know a citation?
Thanks for the reference! I’ve added it to the page.
Was your second sentence meant to be in another thread?
Well, the second sentence was meant for this thread since I didn’t want to flood neither the polymath nor the paraconsistent logics threads with just this reference especially since I’ve never taken a closer look at the article. Thematically it relates to paraconsistent mathematics and could also qualify for ETCC where other references to formalizations of category theory are listed.
The fact their ’complete category of sets’ is a category of material sets is a little odd, but perhaps that goes back to the original 1960s idea of the construction, before ETCS really became a thing.
Well, this thread is about the cut rule, not about paraconsistent mathematics or ETCC. (-:
Sorry :-) if people want to discuss (I’m not itching to do so) then they can take it up elsewhere
I know we often go off on tangents, but that tendency makes it hard to find a discussion again if you’re looking for it, and the subject doesn’t seem even tangentially related here. (-: I’d be happy to discuss it in another thread though.
To 15: The quote is from “Linear logic : its syntax and semantics”, a gentle introduction to linear logic by Girard in 1995 which is not the same thing than the well-known paper “Linear Logic” of 1986. And indeed it is one page 13 in this paper as said in 16, but the link given there is now broken. The quote is not “A logic without cut-elimination is like a car without engine” but “A sequent calculus without cut-elimination is like a car without engine” This improrer quote seems to be everywhere on the net now :(
1 to 26 of 26