Not signed in (Sign In)

Not signed in

Want to take part in these discussions? Sign in if you have an account, or apply for one below

  • Sign in using OpenID

Discussion Tag Cloud

Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.

Welcome to nForum
If you want to take part in these discussions either sign in now (if you have an account), apply for one now (if you don't).

nLab > Latest Changes: cut rule

Bottom of Page

1 to 26 of 26

  1.  
    • CommentRowNumber1.
    • CommentAuthorUrs
    • CommentTimeJan 20th 2014
    • (edited Jan 20th 2014)

    some bare minimum at cut rule

    • CommentRowNumber2.
    • CommentAuthorTobyBartels
    • CommentTimeJan 26th 2014

    I put in a remark about the nullary analogue (which I called the ‘identity rule’, although it goes by various names).

    • CommentRowNumber3.
    • CommentAuthorTodd_Trimble
    • CommentTimeJan 26th 2014

    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⊸ba \multimap b we have a derivation

    a⊢ab⊢ba⊸b,b⊢aa⊸b⊢a⊸b\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 ⊤→¬A℘A=A⊸A\top \to \neg A \wp A = A \multimap A that names the identity is dual to the arrow ¬A⊗A→⊥\neg A \otimes A \to \bot that implements an evaluation). In the one-sided version of MLL, it looks something like this:

    ⊢¬A,Aidentity⊢Γ,¬A⊢Δ,A⊢Γ,Δcut\frac{}{\vdash \neg A, A} \; identity \qquad \frac{\vdash \Gamma, \neg A \;\;\; \vdash \Delta, A}{\vdash \Gamma, \Delta} \; cut
    • CommentRowNumber4.
    • CommentAuthorTobyBartels
    • CommentTimeJan 26th 2014

    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!

    • CommentRowNumber5.
    • CommentAuthorTodd_Trimble
    • CommentTimeJan 26th 2014

    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.

    • CommentRowNumber6.
    • CommentAuthorTodd_Trimble
    • CommentTimeJan 26th 2014

    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?

    • CommentRowNumber7.
    • CommentAuthortonyjones
    • CommentTimeJan 26th 2014
    this is a little of topic but Bruno Paleo has an interesting paper on applications of proof theory to physics (http://www.logic.at/staff/bruno/Papers/2010-PhysicsAndProofTheory-PC.pdf). He gives an example of formalizing energy conservation using the cut rule. He also discusses future perspectives like using cut-introduction ('reductionism
    in Science can generally be captured by the proof-theretical notion of cut. Consequently, a significant part of the usual scientific activity can be formally described as cut-introduction' and 'potential benefits of using proofs to formalize Physics is the possibility of applying cut-introduction techniques in order to automatically discover useful physical concepts'), other thoughts on cut-elimination ('By using cut-elimination algorithms, it might be possible to automatically transform a solution that uses a derived principle (i.e. a cut) such as energy conservation into a solution that uses only the basic laws of a theory' and 'Cut-elimination corresponds to beta-reduction, which is the execution of the program. Cut-introduction corresponds to structuring of the program and possibly to code reuse. By extrapolating this isomorphism, theories of Physics formalized as collections of proofs can be seen as collections of programs. This kind of computation, which is implicit in the formalization of Physics, is yet another link between Physics and
    computation that might be the target of future work'), instrumentalism, theory evolution and algorithmic information theory ('Another indication that AIT and proof theory fit well together is the natural relation between cut-introduction and kolmogorov complexity').
    • CommentRowNumber8.
    • CommentAuthorTobyBartels
    • CommentTimeJan 27th 2014

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

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

    • CommentRowNumber10.
    • CommentAuthorTodd_Trimble
    • CommentTimeJan 27th 2014

    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.

    • CommentRowNumber11.
    • CommentAuthorTobyBartels
    • CommentTimeJan 28th 2014

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

    • CommentRowNumber12.
    • CommentAuthorTodd_Trimble
    • CommentTimeJan 28th 2014

    Thanks for that bit, Toby!

  13. I added an example of reducing a cut on A⊸BA \multimap B, to go along with the example of expanding an identity on A∧BA \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:Γ→At : \Gamma \to A or contexts k:A→Δk : A \to \Delta, depending on the polarity of AA.) I hope the parenthetical remark after the examples is suggestive enough.

    • CommentRowNumber14.
    • CommentAuthorTodd_Trimble
    • CommentTimeJan 28th 2014

    Thanks for the addition, Noam. I added just a few more words to the examples section.

    • CommentRowNumber15.
    • CommentAuthorMike Shulman
    • CommentTimeMay 5th 2016

    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?

    • CommentRowNumber16.
    • CommentAuthorThomas Holder
    • CommentTimeMay 5th 2016
    • (edited May 5th 2016)

    For the Girard quote see page 13 of this one. Excuse me if I become paraconsistent here but there is an Outline of a paraconsistent category theory (2004) by da Costa,Bueno& Volkov (available e.g. from the publisher).

    • CommentRowNumber17.
    • CommentAuthorMike Shulman
    • CommentTimeMay 5th 2016

    Thanks for the reference! I’ve added it to the page.

    Was your second sentence meant to be in another thread?

    • CommentRowNumber18.
    • CommentAuthorThomas Holder
    • CommentTimeMay 5th 2016

    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.

    • CommentRowNumber19.
    • CommentAuthorDavidRoberts
    • CommentTimeMay 6th 2016

    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.

    • CommentRowNumber20.
    • CommentAuthorMike Shulman
    • CommentTimeMay 6th 2016

    Well, this thread is about the cut rule, not about paraconsistent mathematics or ETCC. (-:

    • CommentRowNumber21.
    • CommentAuthorDavidRoberts
    • CommentTimeMay 7th 2016
    • (edited May 7th 2016)

    Sorry :-) if people want to discuss (I’m not itching to do so) then they can take it up elsewhere

    • CommentRowNumber22.
    • CommentAuthorMike Shulman
    • CommentTimeMay 7th 2016

    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.

  23. Fix typo in the beta-reduction example.

    Linas

    diff, v14, current

    • CommentRowNumber24.
    • CommentAuthorJ-B Vienney
    • CommentTimeNov 26th 2022

    Added a section on how cut elimination is a computation and how most of the time it isn’t clearly stated as it.

    diff, v16, current

    • CommentRowNumber25.
    • CommentAuthorJ-B Vienney
    • CommentTimeAug 19th 2023
    • (edited Aug 19th 2023)

    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 :(

    • CommentRowNumber26.
    • CommentAuthorJ-B Vienney
    • CommentTimeAug 19th 2023
    • (edited Aug 19th 2023)

    Fixed the quote

    diff, v18, current

1 to 26 of 26

  1.