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.
Stubs for structural rule, weakening rule, contraction rule, and exchange rule.
Of course, now I need to write premise and deduction, since I used them. Also identity rule and cut rule, since I listed them.
Thanks. Linked back and forth to substructural logic.
I might take issue with calling cut a structural rule, and perhaps identity too. Certainly cut plays a vey different role in logic than the other structural rules.
Thanks, I was surprised that we didn’t already have structural rule; I must have been remembering substructural logic.
Cut and identity go together; they form a binary/nullary pair and can both be eliminated (except atomic instances of identity). Wikipedia calls them structural rules and they fit the definition of not involving connectives, but they are different from the others.
You know, the nomenclature here has always seemed a tad bizarre to me, viz. “structural” rules vs. “logical” rules. Why is say exchange considered ’structural’ and say an introduction rule for a connective ’logical’? Aren’t connectives structure? (They sure are in linear logic!) In any case, it would make just as much if not more sense to me if these adjectives were completely reversed in their roles.
@Todd, I think one way to think of it is that semantically, structural rules correspond to the defining structure and axioms of the type of category you consider. In nonlinear nondependent type theory, that’s a cartesian multicategory: cut and identity are composition of multimorphims, while exchange, weakening, and contraction are reindexing of the domains of multimorphisms. Then the formation, introduction, elimination, and computation rules for types/connectives are about characterizing objects in such a categorical structure via universal properties.
I don’t think I have any opinion on the suitability of the particular adjectives ’structual’ and ’logical’ to their assigned meanings, but I think the fact of a separation makes sense.
These two names have never made much sense to me either, but they are pretty well established.
@Mike #6: of course I do see the point about separating into two classes of rules this way, but I wasn’t asking about that. To me, it would make just as much if not more sense to call the reindexing of domains of multimorphisms “logical”, or refer to the “ambient logic” of the type of multicategory one is considering as cartesian, linear, or whatever. And in the semantics, where one must inevitably choose which objects play the role of sums, products, etc. – that’s property-like structure.
As Toby says, the terminology is old (probably goes back to Gentzen) and well-established – I wasn’t proposing we do anything about it. I just didn’t understand what Gentzen’s (or whoever’s) reasons were, and I still find it a bit odd. (But it was only a little mini-rant, and I’m done. Please, carry on, as you were! (-: )
Okay, sorry I misunderstood your comment. As I said, I agree that the terminology is pretty arbitrary.
1 to 9 of 9