INCLUSION CRITERIA
An entry belongs in this division if and only if it is individuated by the restriction, removal, or fine control of one or more structural rules—weakening, contraction, exchange, associativity, or cut. Transitivity of consequence is a structural rule, and a logic individuated by dropping it belongs here however classical it is otherwise.
Required: At least one of the following:
- A proof system that omits or restricts weakening, contraction, exchange, associativity, or cut
- A resource or relevance reading of the consequence relation arising from that restriction
- Connectives (multiplicative/additive, fusion, ordered implications) whose meaning depends on structural discipline
Not sufficient: Being non-classical for other reasons—many truth values (Algebraic), an intensional operator (Modal), or a typing discipline (Type)—without a structural-rule restriction.
Boundary: Linear type systems and session types, presented as term calculi, belong in Type; the underlying linear logic belongs here. Relevance motivated only by a conditional's truth table without a substructural proof theory is borderline and judged by whether a substructural calculus is given.