Linear logic and substructural logics shake up traditional logic by treating propositions as consumable resources. This fresh approach allows for more precise reasoning about resource usage, making it super useful in computer science and programming.

These logics introduce new connectives and rules that capture resource-sensitive properties. They've found applications in areas like memory management, quantum computing, and program verification, showing how proof theory can tackle real-world problems.

Linear Logic and Substructural Logics

Overview of Linear Logic

• Linear logic is a substructural logic developed by Jean-Yves Girard in 1987
• Differs from classical logic by treating propositions as resources that are consumed when used
• Provides a more fine-grained analysis of proofs and computation
• Allows for reasoning about resource-sensitive properties (memory usage, time complexity)

Substructural Logics and Resource Sensitivity

• Substructural logics are logical systems that lack or restrict some of the structural rules of classical logic (weakening, contraction, exchange)
• Resource sensitivity is a key feature of substructural logics
  • Propositions are treated as resources that are consumed when used in a proof
  • Allows for more precise reasoning about resource usage and allocation
• Resource interpretation of linear logic
  • Each proposition represents a single-use resource
  • Proofs correspond to processes that consume and produce resources

Connectives in Linear Logic

Multiplicative Connectives

• Multiplicative conjunction ($\otimes$) and disjunction ($\parr$)
  • $A \otimes B$ represents the simultaneous availability of resources $A$ and $B$
  • $A \parr B$ represents a choice between resources $A$ and $B$
• Multiplicative implication ($\multimap$)
  • $A \multimap B$ represents a process that consumes $A$ to produce $B$
• Multiplicative constants: $1$ (unit) and $\bot$ (bottom)

Additive Connectives

• Additive conjunction ($&$) and disjunction ($\oplus$)
  • $A & B$ represents a choice between resources $A$ and $B$, but only one is used
  • $A \oplus B$ represents the availability of either resource $A$ or $B$
• Additive constants: $\top$ (top) and $0$ (zero)

Exponentials

• Exponential modalities: $!$ (of course) and $?$ (why not)
  • $!A$ allows for unlimited duplication and discarding of the resource $A$
  • $?A$ allows for unlimited duplication of the resource $A$, but not discarding
• Exponentials reintroduce some of the structural rules in a controlled manner
  • Allows for embedding of classical logic within linear logic

Proof Systems for Linear Logic

Sequent Calculus for Linear Logic

• Sequent calculus is a proof system that operates on sequents of the form $\Gamma \vdash \Delta$
  • $\Gamma$ and $\Delta$ are multisets of formulas
  • Intuitive reading: consuming the resources in $\Gamma$ produces the resources in $\Delta$
• Inference rules for each connective and exponential
  • Rules for multiplicative and additive connectives reflect their resource interpretation
  • Rules for exponentials allow for controlled use of structural rules

Proof Nets

• Proof nets are a graphical representation of proofs in linear logic
• Provide a more abstract and parallel view of proofs compared to sequent calculus
• Correctness criteria for proof nets (acyclicity and connectedness)
  • Ensures that proof nets correspond to valid proofs in linear logic
• Cut elimination in proof nets corresponds to the execution of proofs as processes

Other Substructural Logics

Relevance Logic

• Relevance logic requires that the antecedent and consequent of an implication are relevant to each other
• Rejects the principle of explosion ($A \land \lnot A \vdash B$) and the principle of monotonicity ($\Gamma \vdash A$ implies $\Gamma, B \vdash A$)
• Applications in computer science (type systems, information retrieval)

Affine Logic

• Affine logic is a variant of linear logic that allows for discarding of resources, but not duplication
• Obtained by adding the weakening rule to linear logic
• Used in the study of quantum computation and quantum information theory

Bunched Implications

• Bunched implications (BI) is a substructural logic that combines intuitionistic logic with a multiplicative conjunction
• Provides a logical foundation for reasoning about resource composition and separation
• Applications in program verification (separation logic) and computer security (access control)