natural deduction metalanguage, practical foundations
type theory (dependent, intensional, observational type theory, homotopy type theory)
computational trinitarianism =
propositions as types +programs as proofs +relation type theory/category theory
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 (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,
shown in the following table together with their categorical semantics of dependent types:
the weakening rule,
the contraction rule,
the exchange rule,
the identity rule?,
the cut rule.
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)
Last revised on March 27, 2023 at 19:00:04. See the history of this page for a list of all contributions to it.