Fact-checked by Grok 2 weeks ago

Substructural logic

Substructural logics are a class of nonclassical logical systems defined by the restriction or omission of one or more structural rules—such as weakening, contraction, and exchange—that are standard in the sequent calculi of classical and intuitionistic logics.^[1] These rules, originally formalized by Gerhard Gentzen in the 1930s, govern the manipulation of premises in proofs, including the ability to discard irrelevant assumptions (weakening), reuse assumptions multiple times (contraction), and reorder them freely (exchange).^[1] By limiting these operations, substructural logics treat logical resources as consumable and ordered, avoiding paradoxes like those of material implication where irrelevant premises lead to arbitrary conclusions.^[2] The concept of substructural logic gained prominence in the late 20th century, building on earlier foundational work in relevant and noncommutative systems.^[2] Pioneering contributions include Ivan Orlov's 1928 propositional logic, which rejected weakening to ensure relevance between premises and conclusions; Wilhelm Ackermann's 1950s entailment logic, which further limited permutation and assertion; and Joachim Lambek's 1958 associative calculus, a noncommutative system for syntactic categories in linguistics.^[2] A major milestone was Jean-Yves Girard's introduction of linear logic in 1987, presented not as an alternative to classical logic but as an extension that refines it by forbidding weakening and contraction as global rules, instead controlling resource reuse through special exponential connectives like ! and ?.^[3] This innovation highlighted substructural logics' potential for modeling resource-sensitive processes, such as computation and concurrency.^[3] Key variants of substructural logics include relevant logics (e.g., R and E, which primarily reject weakening), linear logics (which reject both weakening and contraction), and affine logics (which allow weakening but not contraction).^[2] These systems have structural formulations that can be monotonic or nonmonotonic, reflexive or irreflexive, depending on the rules retained, and they often employ frame-based semantics like Routley-Meyer frames with ternary accessibility relations to capture relevance.^[2] In applications, substructural logics underpin type theories in programming languages for safe resource management, categorial grammars in linguistics via Lambek calculus, and partial correctness reasoning in Hoare logic extensions, where assertions are modeled using intuitionistic linear implications without full exchange.^[4] Their study also intersects with proof theory, addressing metainferences and hierarchies that approximate classical logic while resolving semantic paradoxes like the Liar.^[1]

Fundamentals

Definition and Motivation

Substructural logics are a family of non-classical logical systems formulated in sequent calculus where some or all structural rules—such as weakening, contraction, exchange, and associativity—are omitted or restricted, thereby altering the ways in which premises can be manipulated during inference.^[5] This restriction distinguishes them fundamentally from classical logic, in which premises can be freely added (via weakening), duplicated or reused (via contraction), or reordered (via exchange) without affecting validity, treating logical resources as abundant and interchangeable. In substructural logics, by contrast, premises are viewed as consumable or limited resources that must be tracked precisely, preventing arbitrary duplication or discard and enabling finer control over inference steps. The motivation for substructural logics stems from diverse disciplinary needs to model resource-sensitive reasoning beyond the assumptions of classical logic. In philosophy, they address limitations of material implication, such as its paradoxes where irrelevant premises yield valid conditionals (e.g., a false antecedent implying anything), by enforcing relevance between premises and conclusions in systems like relevant logic.^[6] In computer science, these logics support resource management in concurrent and parallel programming, where assumptions or data cannot be freely copied or discarded, as exemplified in linear logic's treatment of proofs as processes consuming inputs to produce outputs.^[3] Similarly, in linguistics, substructural systems facilitate dependency tracking in syntactic composition, ensuring that grammatical elements combine directionally without extraneous reuse, as in categorial grammars for natural language structure.^[7] Substructural logics emerged in the late 20th century as a unified framework to resolve issues of relevance and linearity in inference, with foundational contributions including Lambek's 1958 calculus for syntax, Anderson, Belnap, and Dunn's 1975 developments in relevant entailment, and Girard's 1987 introduction of linear logic.^[7]^[6]^[3]

Structural Rules in Classical Logic

In classical sequent calculus, as introduced by Gentzen in his foundational work on proof theory, sequents are expressed in the notation \Gamma \vdash \Delta, where \Gamma represents a multiset of formulas serving as the antecedents or premises on the left-hand side, and \Delta represents a multiset of formulas serving as the consequents or conclusions on the right-hand side. This notation treats formulas as resources that can be used without inherent restrictions on multiplicity or order, reflecting the unrestricted nature of classical deduction.^[8] The core structural rules in this system—weakening, contraction, exchange, and associativity—govern the manipulation of these multisets, enabling flexible handling of premises and conclusions. Weakening allows the addition of irrelevant formulas to either side of the sequent without affecting derivability; for instance, from \Gamma \vdash \Delta, one may derive \Gamma, A \vdash \Delta (left weakening) or \Gamma \vdash \Delta, A (right weakening), where A is any formula not contributing to the proof. Contraction permits the elimination of duplicate formulas in the antecedents by merging multiple occurrences into one; specifically, from \Gamma, A, A \vdash \Delta, the sequent \Gamma, A \vdash \Delta follows (left contraction), with a symmetric rule for the right side.^[8] Exchange, also known as permutation, ensures that the order of formulas within \Gamma or \Delta is immaterial, allowing arbitrary reordering such as swapping adjacent formulas on either side. Associativity further reinforces the multiset structure by making the grouping of formulas irrelevant; thus, sequents like (\Gamma, A, B) \vdash \Delta and \Gamma, (A, B) \vdash \Delta are equivalent, as the comma operation is associative. These rules collectively underpin the system's permissiveness, allowing proofs to ignore resource limitations in formula usage. In classical logic, these structural rules play a pivotal role in achieving key theoretical properties, including the cut-elimination theorem, which guarantees that any proof using the cut rule (a form of transitivity) can be transformed into an equivalent cut-free proof, and the completeness of the system relative to classical semantics. They facilitate unrestricted manipulation of premises, ensuring that classical sequent calculus LK fully captures the expressive power of classical propositional and predicate logic.^[8]

Core Concepts

Sequent Calculus Framework

The sequent calculus framework serves as the foundational proof theory for substructural logics, providing a structured way to represent logical deductions through sequents and inference rules. Introduced by Gerhard Gentzen in his seminal work on logical inference, this system formalizes proofs as trees built from initial axioms and rule applications, enabling precise analysis of deduction processes.^[9] A sequent takes the form \Gamma \vdash \Delta, where \Gamma is a multiset of formulas on the left (antecedent, representing assumptions) and \Delta a multiset on the right (succedent, representing conclusions); the turnstile \vdash indicates that the assumptions entail the conclusions.^[10] Proofs begin with axioms of the form A \vdash A, where a formula A appears on both sides, and are extended via inference rules that preserve the validity of sequents.^[9] Inference rules in sequent calculus are categorized into logical rules, which handle the introduction and elimination of logical connectives, and structural rules, which permit manipulations of the antecedent and succedent such as weakening, contraction, and exchange.^[10] Logical rules include left and right introduction rules for connectives like implication (\to), conjunction (\land), and disjunction (\lor). For implication, the right introduction rule (\to_R) derives \Gamma \vdash A \to B from \Gamma, A \vdash B, while the left introduction rule (\to_L) derives \Gamma, A \to B, \Delta \vdash C from \Gamma \vdash A and \Delta, B \vdash C.^[11] Similarly, for conjunction, the right introduction rule (\land_R) allows \Gamma \vdash A \land B from \Gamma \vdash A and \Gamma \vdash B, and the left introduction rules (\land_{L1}, \land_{L2}) project components accordingly.^[10] The cut rule, a key structural-logical hybrid, eliminates implications by combining two sequents: from \Gamma \vdash A and \Delta, A \vdash B, it yields \Gamma, \Delta \vdash B, facilitating the connection of subproofs but often targeted for elimination in normalized proofs.^[9] A cornerstone of the framework is the proof normalization process, embodied in Gentzen's cut-elimination theorem (Hauptsatz), which demonstrates that any proof using the cut rule can be transformed into an equivalent cut-free proof through a series of reductions. This theorem, proven for both classical and intuitionistic logics, ensures the consistency of the system and highlights the subformula property in cut-free proofs, where all formulas in a derivation are subformulas of the end-sequent.^[10] In classical and intuitionistic settings, cut-elimination preserves logical equivalence and supports automated proof search by avoiding non-local cuts.^[11] Sequent calculus relates to natural deduction as a complementary system, both originating from Gentzen's efforts to model deduction more analytically; while natural deduction emphasizes elimination and introduction rules in a tree-like structure mimicking informal reasoning, sequent calculus offers a symmetric treatment of antecedents and succedents, better suited for hypothetical judgments and multiple conclusions.^[11] This symmetry facilitates the study of structural properties in proofs, providing a versatile foundation for extensions in substructural logics.^[10]

Relaxation of Structural Rules

Substructural logics achieve resource sensitivity by relaxing the structural rules of classical sequent calculus, which typically include weakening, contraction, exchange, and associativity.^[2] These relaxations prevent unrestricted manipulation of premises, modeling scenarios where assumptions represent limited resources that must be tracked precisely.^[12] One common relaxation omits weakening, the rule allowing arbitrary addition of premises (e.g., from \Gamma \vdash C to \Gamma, B \vdash C), ensuring all formulas in the antecedent \Gamma must be used in the derivation.^[2] Omitting contraction, which merges multiple occurrences of a formula (e.g., from \Gamma, A, A \vdash C to \Gamma, A \vdash C), treats repeated premises as distinct, preventing duplication and enforcing single-use consumption.^[12] Restricting exchange makes premise order significant, as in non-commutative systems where reordering (e.g., \Gamma, A, B \vdash C does not imply \Gamma, B, A \vdash C) is invalid.^[2] Non-associativity further relaxes grouping, treating antecedents as ordered trees rather than flat multisets, so structures like A, (B, C) differ from (A, B), C.^[2] These relaxations yield distinct systems: affine logics permit weakening but omit contraction, allowing discard but not reuse of resources; strict relevance logics omit both weakening and contraction to enforce premise relevance; full linear logics extend this by also restricting exchange for order sensitivity.^[12]^[2] For instance, classical logic derives A, B \vdash B from A \vdash A and B \vdash B via weakening, but substructural variants without weakening fail this inference, requiring explicit resource accounting.^[4]

Varieties

Linear Logic

Linear logic, introduced by Jean-Yves Girard in 1987, represents a refinement of classical and intuitionistic logics by treating logical resources as consumable entities that cannot be freely duplicated or discarded.^[13] This approach arises from a relaxation of structural rules in the sequent calculus, specifically by prohibiting weakening and contraction for linear formulas while permitting exchange.^[13] A central innovation is the introduction of the exponential modality !, which marks formulas as reusable resources; only !A allows contraction (duplication) and weakening (deletion), enabling the recovery of classical behavior for such persistent propositions.^[13] Linear logic further distinguishes between multiplicative connectives, which combine resources sequentially, and additive connectives, which operate in parallel: the multiplicative conjunction ⊗ and par ⌓ (denoted as \parr) emphasize resource consumption, while the additives & (with) and ⊕ (plus) focus on choice without resource splitting.^[13] The full set of connectives includes these alongside linear implication (⌓, or -o), negation (~), and the dual exponential ? for the "why not" modality in the succedent.^[13] In practice, these features ensure precise resource tracking. For instance, to derive the sequent A, B \vdash A \otimes B from the axioms A \vdash A and B \vdash B, the tensor introduction rule requires both premises to be combined exactly once, without duplication or omission of either resource:

\frac{A \vdash A \quad B \vdash B}{A, B \vdash A \otimes B} \text{($\otimes$R)}

This contrasts with classical conjunction, where resources could be reused freely.^[13]

Relevant Logic

Relevant logic, also known as relevance logic, emerged in the mid-20th century as a response to perceived inadequacies in classical and modal logics regarding the notion of entailment. It was primarily developed during the 1950s and 1970s by philosophers Alan Ross Anderson and Nuel D. Belnap, Jr., who sought to formalize a stricter criterion for logical implication where premises must genuinely contribute to the conclusion. Their collaborative work culminated in the seminal two-volume treatise Entailment: The Logic of Relevance and Necessity, which established the foundational systems and philosophical motivations for the field.^[14] A central feature of relevant logic is the rejection of the weakening rule, which in classical logic permits the addition of irrelevant premises without affecting validity; this ensures that all premises in an entailment are meaningfully used to derive the conclusion, embodying the principle of relevance. Unlike stricter substructural systems, contraction—the rule allowing multiple uses of a premise—is typically permitted in core relevant logics like R, but subject to overall relevance constraints enforced by the system's axioms and rules. Exchange (permuting premises) and associativity (reordering groupings of premises) are generally preserved, maintaining a flexible yet disciplined handling of premise combinations. The logic introduces specialized connectives to capture relevant relationships. The relevant implication, denoted →, requires that the antecedent and consequent share at least one variable (or content in semantic terms), preventing implications from holding vacuously; for instance, if A and B have no common variables, A → B is not a theorem. Fusion, symbolized as • (or sometimes ◦), serves as a multiplicative conjunction that combines premises in a way that preserves relevance, behaving like a "non-additive and" where both operands must be utilized without dilution.^[14] Relevant logic as a substructural system specifically relaxes the weakening rule to enforce anti-weakening, prioritizing the substantive connection between premises and conclusions over unrestricted premise manipulation. A key illustration of its distinctiveness is the avoidance of classical paradoxes arising from irrelevant transitivity, such as the schema (P \to Q) \to ((Q \to R) \to (P \to R)), which fails as a theorem when P and R share no variables, as the premise P \to Q does not meaningfully support the irrelevantly chained conclusion P \to R.^[14]

Other Substructural Systems

BCI logic is a substructural system that omits the structural rules of contraction and weakening, thereby treating implications as non-duplicable and non-discardable resources in its implicational fragment.^[15] This logic serves as the foundational basis for combinatory logic, where its axioms correspond to the combinators B, C, and I, enabling variable-free term manipulation without resource duplication.^[15] BCK logic is defined by axioms B, C, and K, permitting weakening but prohibiting contraction, with exchange retained via the C axiom; this results in a system where resources are used at most once but can be discarded.^[15] It models aspects of the lambda calculus that prohibit resource duplication, aligning with typed lambda terms where variables occur at most once, thus supporting precise control over resource consumption in computational proofs.^[15] Non-commutative linear logic, often denoted as NL, relaxes the exchange rule in the multiplicative fragment of linear logic to enforce ordered resource usage, distinguishing it from commutative variants by preserving sequence in premise combinations.^[16] This makes NL suitable for modeling linguistic structures or concurrent processes where the order of hypotheses affects inference outcomes.^[16] Affine logic permits weakening but prohibits contraction, allowing resources to be discarded as optional but preventing their duplication, which contrasts with linear logic's stricter exact-use requirement.^[17] It proves useful in type systems for representing optional arguments or probabilistic computations where unused resources can be ignored without reuse.^[17] These systems illustrate a lattice of substructural restrictions, where logics are ordered by the inclusion of structural rules, with fully restricted variants like BCK at one extreme and progressively permissive ones like affine approaching classical behavior.^[18]

Formal Semantics

Residuated Lattices

A residuated lattice is an algebraic structure that serves as the canonical semantics for the multiplicative fragment of substructural logics. Formally, it is a tuple \langle L, \wedge, \vee, \otimes, \mathbf{1}, \multimap, \multimap^\mathrm{op} \rangle, where \langle L, \wedge, \vee \rangle is a lattice, \langle L, \otimes, \mathbf{1} \rangle is a monoid, and the binary operations \multimap (right residual) and \multimap^\mathrm{op} (left residual) satisfy the residuation condition: for all a, b, c \in L,

a \otimes b \leq c \quad \iff \quad b \leq a \multimap c \quad \iff \quad a \leq c \multimap^\mathrm{op} b,

where \leq is the lattice order.^[18] In substructural logics, residuated lattices model the multiplicative connectives, such as fusion (\otimes) for conjunction and implications (\multimap, \multimap^\mathrm{op}) for conditionals, capturing resource-sensitive reasoning where premises are not freely reusable or discardable. The absence of structural rules in these logics corresponds to specific properties of the lattice: for instance, the lack of contraction (non-duplication of premises) aligns with the non-idempotence of \otimes (i.e., a \otimes a \not\leq a), while the absence of weakening (non-discardability) relates to the monoid unit \mathbf{1} not being the lattice top.^[18] Key variants of residuated lattices tailor the semantics to particular substructural systems. Full Lambek logic (FL) is semantically characterized by general residuated lattices (RL), which impose no additional restrictions beyond residuation. Integral residuated lattices (IL) add the condition that \mathbf{1} is the top element (x \leq \mathbf{1} for all x), enabling weakening and modeling intuitionistic-like systems. Non-commutative variants (as in RL and IL) distinguish left and right residuals to reflect ordered resource combination, whereas commutative residuated lattices enforce (\ a \otimes b = b \otimes a\ ), corresponding to logics with exchange (permutation of premises).^[18]^[19] Many substructural logics are sound and complete with respect to classes of residuated lattices. For example, BCI logic is complete relative to commutative integral bounded residuated lattices, while the multiplicative fragment of linear logic is complete with respect to *-autonomous residuated lattices (a variant with dualizing objects). Soundness follows from the interpretation of sequents as inequalities in the lattice, and completeness is established via canonical extensions or cut-elimination theorems for the corresponding sequent calculi.^[18]^[19] The residuation condition embodies a Galois connection between the monoid operation and residuals, ensuring that \otimes is the left adjoint to the right residual in the lattice order:

\begin{aligned} & a \otimes (-) \dashv (-) \multimap a, \\ & (-) \otimes a \dashv a \multimap^\mathrm{op} (-). \end{aligned}

This adjunction provides the foundational link between the syntactic implications and algebraic inequalities in substructural semantics.^[18] Semantics for specific varieties of substructural logics, such as linear logic, often extend residuated lattices with phase spaces or coherence conditions to model additive connectives alongside multiplicatives.^[18]

Premise Composition Methods

In substructural logics, premises in sequent calculi are composed into antecedent structures that reflect restrictions on structural rules such as weakening, contraction, exchange, and associativity, unlike the flat sets used in classical logic. These compositions enable precise modeling of resource sensitivity, relevance, and order in proofs.^[20] Classical logic employs sets for antecedents, where formulas are unordered and duplicates are identified, allowing unrestricted weakening (introduction of irrelevant premises) and contraction (reuse of premises). This set-based composition supports the full structural rules, ensuring that the order and multiplicity of premises do not affect provability.^[20] Multisets extend sets by accounting for the multiplicity of formula occurrences without regard to order, prohibiting contraction to track each premise's exact usage as a limited resource. In linear logic, antecedents are formalized as multisets, where operations like fusion (juxtaposition) combine them without merging duplicates, enforcing that each premise is consumed exactly once in derivations. For instance, Girard's sequent calculus for multiplicative linear logic uses multiset antecedents to model resource consumption, as in sequents of the form \Gamma \vdash \Delta, where \Gamma and \Delta are multisets. This approach implies that proofs maintain a strict accounting of assumptions, preventing the paradoxes of material implication arising from irrelevant or overused premises. Similarly, in relevant logics, multisets in antecedents ensure that premises are relevant to the conclusion by disallowing contraction, as formalized in systems like R, where antecedents represent collections with counted occurrences to enforce the variable-sharing principle.90045-4)^[21]^[2] Sequences introduce order sensitivity by treating antecedents as linear arrangements of formulas, omitting the exchange rule to preserve positional dependencies. In the Lambek calculus, antecedents are sequences, reflecting non-commutativity to model syntactic structures in natural language, where the order of premises corresponds to phrase composition. Formalization involves division operators (left and right slash) that operate on these ordered structures, with rules like application ensuring that premise order is maintained: for example, from A B \vdash C, one derives A \vdash B \backslash C or B \vdash A / C, without permuting elements. This has implications for grammatical modeling, as sequences capture directional dependencies in categorial grammars. Trees generalize sequences to non-associative, hierarchical structures, allowing antecedents to branch without implicit grouping, which omits the associativity rule. In non-associative variants of the Lambek calculus, such as NL, antecedents are represented as binary trees to model non-flat constituency in linguistic trees, with operations like extraction respecting the tree's branching. This formalization restricts merging to explicit nodes, preventing associative regrouping of premises. Such tree-based compositions are used in multimodal substructural systems to handle complex nesting without associativity assumptions.^[22]^[23] These premise composition methods provide advantages in controlling resource flow within proofs, enabling substructural logics to model phenomena like computational resources in linear logic or syntactic hierarchies in Lambek systems, where classical sets would allow overly permissive manipulations. Semantically, these syntactic structures align with operations in residuated lattices, offering a corresponding algebraic interpretation.^[20]

History and Applications

Historical Development

The origins of substructural logic trace back to at least the 1920s, with Ivan Orlov's 1928 formulation of a propositional relevant logic that rejected weakening to ensure relevance between premises and conclusions.^[2] Significant developments occurred in the mid-20th century, particularly in relevant logics motivated by concerns over the paradoxes of material implication in classical logic. In the 1950s, Alan Ross Anderson and Nuel D. Belnap began systematizing relevant logics, emphasizing that premises must be genuinely used in derivations to avoid irrelevant implications; their foundational work culminated in the multi-volume Entailment: The Logic of Relevance and Necessity (1975, 1992), which established proof-theoretic frameworks restricting structural rules like contraction and weakening to ensure resource sensitivity.^[20]^[2] Independently, in 1958, Joachim Lambek introduced the Lambek calculus as a noncommutative, associative system for modeling syntactic structures in linguistics, omitting weakening and contraction to track linguistic resources precisely; this calculus, detailed in "The Mathematics of Sentence Structure," laid groundwork for categorial grammars and substructural approaches in formal semantics.^[20]^[2] Interest in these resource-aware logics surged in the late 1980s, particularly with Jean-Yves Girard's introduction of linear logic in 1987, which reframed sequent calculus by treating hypotheses as consumable resources and incorporating modalities for controlled reuse, as presented in his seminal paper "Linear Logic" in Theoretical Computer Science.^[20]90045-4) This revival highlighted substructural logics' potential beyond philosophy, influencing proof theory and computation. Around the same time, Kosta Došen advanced the abstract study of logics via structural rule restrictions in papers like "Logical Constants as Punctuation Marks" (1988) and "Sequent Calculi for Some Consequence Relations" (1990), and he coined the term "substructural logics" at the 1990 workshop to unify systems deviating from full Gentzen-style structural rules.^[2] The field's consolidation occurred in 1990 with the First International Workshop on Substructural Logics in Tübingen, Germany, which fostered dialogue among researchers in relevant, linear, and Lambek-style systems; proceedings edited by Peter Schroeder-Heister and Kosta Došen (1993) marked a key milestone in community formation.^[24] Through the 1990s and 2000s, substructural logics integrated with computer science, particularly in type theory, concurrency, and algebraic semantics, as evidenced by Greg Restall's An Introduction to Substructural Logics (2000), which synthesized proof and model theories.^[2] A comprehensive algebraic treatment emerged in Residuated Lattices by Nikolaos Galatos, Peter Jipsen, Tomasz Kowalski, and Hiroakira Ono (2007), providing a unified framework for many substructural varieties and underscoring their mathematical depth.^[20]

Modern Applications

In computer science, substructural logics, particularly linear logic, have been integrated into type systems to enforce resource-sensitive computations and provide complexity bounds. Girard's Light Linear Logic (LLL), introduced in 1998, refines linear logic by restricting structural rules to characterize polynomial-time functions through the proofs-as-programs correspondence, enabling type-based analysis of computational complexity without relying on external bounds.^[25] This approach has influenced implicit computational complexity theory, where types directly control resource usage in functional programming languages. Additionally, session types, rooted in linear logic, model concurrency in message-passing systems by ensuring linear use of communication channels, preventing errors like deadlock or race conditions in distributed protocols. The correspondence between linear logic propositions and session types, formalized in works like Caires and Pfenning's 2013 framework, allows processes to be verified as adhering to expected interaction sequences, enhancing safety in concurrent programming languages such as those based on the π-calculus.^[26] In linguistics, the Lambek calculus serves as a foundational substructural system for categorial grammars, enabling the modeling of natural language syntax through resource-sensitive composition without the limitations of context-free grammars. Developed by Lambek in 1958, this non-commutative logic treats syntactic categories as types and function application as deduction, capturing phenomena like extraction and discontinuous dependencies that exceed context-free power, such as in Dutch cross-serial dependencies. Modern extensions, including multimodal categorial grammars, leverage these properties to parse complex linguistic structures while preserving directional constraints on argument combination.^[27] In philosophy, substructural logics support models of belief revision and defeasible reasoning by incorporating relevance constraints that prevent irrelevant assumptions from propagating, addressing limitations in monotonic classical systems. Relevant logics, a key substructural variety, ensure that premises bear directly on conclusions, facilitating defeasible inferences where beliefs can be overridden by new evidence without global inconsistency. For instance, in belief revision frameworks, substructural approaches reformulate conditional logics to handle dynamic updates under resource scarcity, as explored in integrations of substructural sequents with revision operators.^[28] This is particularly useful for modeling practical reasoning in ethics and law, where default rules yield to exceptions without requiring full recomputation. Emerging applications since 2010 highlight substructural logics in quantum information and AI proof assistants. In quantum computing, linear logic models the no-cloning theorem by prohibiting contraction, reflecting the impossibility of duplicating unknown quantum states and enabling resource-aware protocols for quantum circuits and error correction. Abramsky and Coecke's 2004 framework provides a categorical semantics for quantum protocols, drawing on monoidal structures akin to those in linear logic to capture quantum processes, time evolution, and measurements while respecting resource limits.^[29] In AI, linear types have been mechanized in proof assistants like Coq to verify resource-bounded proofs, with formalizations of linear logic supporting cut-elimination and focusing for certified programming. Nigam et al.'s 2017 Coq encoding demonstrates how substructural types ensure precise control over proof resources, aiding in the development of secure, efficient theorem provers.^[30] Compared to classical logic, substructural logics excel in real-world modeling by explicitly handling scarcity and dependency, where resources like assumptions or data cannot be freely duplicated or discarded, thus avoiding paradoxes in resource-intensive domains such as concurrency and quantum systems. This resource sensitivity provides finer-grained control, enabling accurate representations of consumption and ordering in proofs and processes.^[31]

References

[1]
[PDF] Editorial Introduction: Substructural Logics and Metainferences - HAL
Jan 7, 2023 · Abstract. The concept of substructural logic was originally introduced in relation to limitations of Gentzen's structural rules of ...
[2]
[PDF] Relevant and Substructural Logics - Greg Restall
with an eye to proofs, or with an eye to models.2 Relevant and substructural logics are no ...
[3]
[PDF] LINEAR LOGIC : ITS SYNTAX AND SEMANTICS - Jean-Yves GIRARD
Linear logic is not an alternative logic ; it should rather be seen as an exten- sion of usual logic. Since there is no hope to modify the extant classical or.
[4]
[PDF] Substructural Logic and Partial Correctness - CS@Cornell
We formulate a noncommutative sequent calculus for partial correctness that subsumes proposi- tional Hoare Logic. Partial correctness assertions are ...
[5]
An Introduction to Substructural Logics - ResearchGate
Substructural logic [7, 19] is a general term for a family of logics that prohibit or limit the use of some of the structural rules. Based on various ...
[6]
https://press.princeton.edu/books/paperback/9780691600420/entailment-vol-ii
[7]
[PDF] The Mathematics of Sentence Structure Joachim Lambek
Mar 11, 2008 · The calculus presented here is formally identical with a calculus constructed by G. D. Findlay and the present author for a discussion of ...
[8]
Structural Proof Theory - Cambridge University Press & Assessment
Sara Negri, University of Helsinki, Jan von Plato, University of Helsinki. Appendix by Aarne Ranta. Publisher: Cambridge University Press. Online publication ...Missing: rules | Show results with:rules
[9]
[PDF] Untersuchungen über das logische Schließen I - Digizeitschriften
Titel: Untersuchungen über das logische Schließen I. Autor: Gentzen, G. Ort: Berlin. Jahr: 1935. PURL: https://resolver.sub.uni-goettingen.de/purl ...
[10]
[PDF] Sequent Calculus
The sequent calculus was originally introduced by Gentzen [Gen35], primarily as a technical device for proving consistency of predicate logic. Our goal of ...
[11]
[PDF] A Tutorial on Computational Classical Logic and the Sequent Calculus
Gentzen's sequent calculus provides a native language for classical logic which admits ... corresponds one-for-one with the structural rules of Gentzen's LK ...
[12]
[PDF] Talk Notes: Substructural Logics
Linear logic, by forgoing weakening and contraction, requires every assumption to be used exactly once; affine logic forgoes only contraction (use each assump-.
[13]
Linear logic - ScienceDirect.com
1987, Pages 1-101. Theoretical Computer Science. Linear logic☆. Author links open overlay panel. Jean-Yves Girard ... Because of its length and novelty this paper ...Missing: original | Show results with:original
[14]
Entailment and Relevance - jstor
Volume 25, Number 2, June 1960. ENTAILMENT AND RELEVANCE'. NUEL D. BELNAP, JR. Those who object to the identification of strict implication and entail- ment ...
[15]
BCK and BCI Logics, Condensed Detachment and the 2-Property
A BCI-λ-term with no free variables is called aBCl-combinator. There is a precise correspondence between BCK-combinators in CL and those in λ-calculus (and ...
[16]
Non‐commutative intuitionistic linear logic - Wiley Online Library
1 Abrusci, V. M., Sequent calculus for intuitionistic linear propositional logic. In: Proceedings of the summer School and Conference on Mathematical Logic, ...
[17]
Semantics of weakening and contraction - ScienceDirect.com
These give rise to two logics which are “inbetween” linear and intuitionistic logic: in affine (or weakening) logic one always has a weakening and a ! w for ...<|separator|>
[18]
Substructural Logics and Residuated Lattices — an Introduction
This is an introductory survey of substructural logics and of residuated lattices which are algebraic structures for substructural logics.
[19]
[PDF] A Survey of Residuated Lattices1 - Vanderbilt University
In the language of residuated lattices, this subvariety is defined relative to RL by the identity x(x\e) = e. Other well known subvarieties of RL include ...
[20]
Substructural Logics - Stanford Encyclopedia of Philosophy
Aug 15, 2024 · Substructural logics are non-classical logics notable for the absence of one or more structural rules present in classical logic.
[21]
Relevance Logic - Stanford Encyclopedia of Philosophy
Jun 17, 1998 · In the work of Anderson and Belnap the central systems of relevance logic were the logic \(\mathbf{E}\) of relevant entailment and the system ...
[22]
[2501.00496] Semi-Substructural Logics à la Lambek - arXiv
Dec 31, 2024 · ... non-associative Lambek calculus, with trees as antecedents. Each calculus is respectively equivalent to the sequent calculus with stoup (for ...
[23]
Non-associative, Non-commutative Multi-modal Linear Logic
Aug 1, 2022 · Non-associative contexts will be organized via binary trees, here called structures. Definition 1. (Structured sequents). Structures are ...<|separator|>
[24]
A Historical Introduction to Substructural Logics - Oxford Academic
Oct 31, 2023 · It is as if the structural part of logic were more fundamental: to change logic, we have to change this part. Logical constants are in principle ...
[25]
[PDF] LIGHT LINEAR LOGIC - Jean-Yves GIRARD
Light Linear Logic is a purely logical system with a more careful handling of structural rules : this system is strong enough to represent all polytime ...
[26]
[PDF] Linear Logic Propositions as Session Types
In this paper we present a type system for the π-calculus that exactly corresponds to the standard sequent calculus proof system for dual intuitionistic linear ...
[27]
A Logic for Categorial Grammars: Lambek's Syntactic Calculus
Our second chapter is a rather complete study of the Lambek calculus, which enables a completely logical treatment of categorial grammar.
[28]
[PDF] When Conditional Logic and Belief Revision Meet Substructural ...
Conditional logic and belief revision the- ory are prominent theories in artificial intelligence dealing with common sense reasoning. We show in this article ...Missing: defeasible | Show results with:defeasible<|separator|>
[29]
[PDF] Linear Logic for Generalized Quantum Mechanics
Linear logic is used as a dynamic quantum logic, extending quantum logic with time, and is a generalized dynamic quantum logic.
[30]
[PDF] Mechanizing Linear Logic in Coq - Vivek Nigam
Feb 16, 2018 · This paper formalizes linear logic in Coq and mechanizes the proof of cut-elimination and the completeness of focusing. Moreover, the ...