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.
cross-linked this entry with intuitionistic type theory
and added references
and (here) a table of a pretty-printed form of the structural rules in DTT and their categorical semantics.
This is essentially the same edit as announced here for Martin-Loef dependent type theory, and the same request for more original references applies.
added this pointer to:
I have been trying to complete the list of examples in this entry, and to cross-link all the relevant entries. Currently it looks as follows:
structural rules
Is this actually accurate? Are all of these regarded as “structural” and is any missing?
I gather as core structural rules count weakening, contraction and exchange? Identity/var seems to be regarded as even more primitive? Is cut really regarded as “structural” or is it called a “context rule”, or both?
Maybe we could make a pretty hierarchical bullet list of these items.
added pointer to the origin of the Struktur-Schlußfiguren in
Gerhard Gentzen, §1.2.1 in: Untersuchungen über das logische Schließen I Mathematische Zeitschrift 39 1 (1935) [doi:10.1007/BF01201353]
Gerhard Gentzen, §1.21 in: Investigations into Logical Deduction, in M. E. Szabo (ed.), The Collected Papers of Gerhard Gentzen, Studies in Logic and the Foundations of Mathematics 55, Springer (1969) 68-131 [ISBN:978-0-444-53419-4, pdf]
together with a screenshot of the original paragraph from Gentzen 1935
am adding these pointers also to the specific entries, like contraction rule etc.
Is this actually accurate? Are all of these regarded as “structural” and is any missing?
My understanding is that these are all typically viewed as structural rules, though variable projection and substitution are often considered to be more primitive (you can consider type theories without weakening, contraction, or exchange, but if you remove variables and substitution, you’re arguably not left with something that resembles a type theory).
Cut and substitution are really the same concept (and I would call them both structural rules), but presented slightly differently (e.g. cut elimination corresponds to admissibility of substitution). I see this is very briefly mentioned on substitution, but not on cut rule.
Thanks!
If I am reading you correctly, then this agrees with Gentzen’s original definition: he lists
weakening,
contraction
exchange
cut
as the Struktur-Schlußfiguren.
If you’d like to exand on this in the entry I’d find it very useful. There is a lot of implicit convention/knowledge in this field.
1 to 6 of 6