nLab structural rule

Idea

General

The structural rules of a logic or deductive system are those rules which make no reference to logical operators but only to the unstructured premises of a deduction.

In standard intuitionistic logic the structural rules notably include the weakening rule and the contraction rule. Discarding these rules leads to linear logic. Generally, logical systems discarding some structural rules are called substructural logics.

In dependent type theory

In (intuitionistic) dependent type theory the structural rules include (e.g. Jacobs (1998), p. 122, UFP13, A.2.2, Rijke (2018), Sec. 1.4):

• the variable rule,

• the weakening rule,

• the substitution rule

shown in the following table together with their categorical semantics of dependent types:

Examples

• the weakening rule,

• the contraction rule,

• the exchange rule,

• the identity rule?,

• the cut rule.

Related pages

• substructural logic is logic in which one or more structural rules are omitted.

References

Discussion in dependent type theory:

• Bart Jacobs, Chapter 10 in: Categorical Logic and Type Theory, Studies in Logic and the Foundations of Mathematics 141, Elsevier (1998) [ISBN:978-0-444-50170-7, pdf]

  (emphasis on the categorical model of dependent types)

• Univalent Foundations Project, §A of Homotopy Type Theory – Univalent Foundations of Mathematics (2013) [web, pdf]

  (in the context of homotopy type theory)

• Egbert Rijke, Dependent type theory [pdf], Lecture 1 in: Introduction to Homotopy Type Theory, lecture notes, CMU (2018) [pdf, pdf, webpage]

  (in the context of homotopy type theory)