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
Substructural logic is a general term for logics in which the structural inference rules:
the contraction rule
the weakening rule
the exchange rule
are not necessarily assumed, or only with restrictions.
Some particular substructural logics include:
linear logic, perhaps the best-known to category theorists, omits the contraction and weakening rules. “Noncommutative linear logic” omits also the exchange rule.
affine logic omits only the contraction rule. One might call it “coaffine logic” if we omit only the weakening rule.
Some forms of relevant logic and paraconsistent logic can be regarded as substructural logics (often of the coaffine variety).
Last revised on March 28, 2024 at 14:40:32. See the history of this page for a list of all contributions to it.