Proposed by Jean-Yves Girard, attempts to unify classical logic and intuitionist logic (like [sequent calculus](Sequent%20Calculus.md)). Linear logic has a lot of applications and isomorphisms in programming languages, quantum physics, quantum information theory, game semantics, and even linguistics. Under linear logic, logical deduction is no longer merely about an ever-expanding collection of persistent "truths", but also a way of manipulating _resources_ that cannot always be duplicated or thrown away at will. TODO: understand and summarize https://en.wikipedia.org/wiki/Linear_logic#Sequent_calculus_presentation as it is the relevant section