What If Every Fact You Used Disappeared After One Use?
When a Fact Gets Used Up
Picture a mathematician in 1934, hunched over a stack of papers, trying to figure out why some proofs feel sneaky. Gerhard Gentzen (1909–1945) had invented a new way of writing proofs, called the sequent calculus, and he noticed something odd. In classical logic, you can copy a fact as many times as you like. You can also throw a fact away without using it. These two special moves — contraction (copying) and weakening (throwing away) — are invisible tricks. They make classical logic powerful, but they also let you prove things without ever showing exactly how to build what you claim exists.
Gentzen saw that intuitionistic logic, a rival system that insisted every existence proof had to show a construction, got rid of the weirdness by limiting these tricks — but at a cost: the beautiful symmetry of classical logic broke. Negation stopped working both ways. The logical world became lopsided.
Jump ahead to 1987. The French logician Jean-Yves Girard (born 1947) asked a startling question: what if we threw out contraction and weakening completely? No copying, no trashing. Every time you used a statement in a proof, it would be consumed, like a snack you can eat only once. This was the birth of linear logic.
In this new system, formulas behave like limited resources. If you have “A” and you use it to get “B”, you don’t get to keep “A” for later. The logic forces you to account for exactly how many times each piece is needed. At first, that sounds like a nightmare. But Girard realized it opened up a whole new way of modeling computation, where resources really are finite — memory cells, processing time, or the single copy of a data value.
The Day “And” and “Or” Split in Two
Without contraction and weakening, the connectives “and” and “or” break apart. In classical logic, there is one “and” that you can use in many ways. But when you cannot copy or erase, two different kinds of “and” show up, and they are no longer equivalent.
Imagine two types of “and” at a snack bar. The additive conjunction (written & and called “with”) says you could have either snack, but you have to choose which one to take. The multiplicative conjunction (written ⊗ and called “tensor”) says you actually do have both, but they come as a package — you must use both together, and once you use them, they’re gone.
Similarly, “or” splits. The additive disjunction (⊕, “plus”) means you get to pick one option but you must commit. The multiplicative disjunction (⅋, “par”) is trickier: it says the two sides are connected so that proving one might require using the other in a kind of swap.
This explains a famous disagreement between classical and intuitionistic logicians: the law of excluded middle, which says “A or not-A” is always true. In linear logic, this law reads differently depending on which “or” you use. The additive version “A ⊕ ¬A” is not provable — it matches the intuitionistic complaint that you can’t always decide which side is true. The multiplicative version “A ⅋ ¬A” is trivially provable — it reduces to “A implies A”, which even intuitionists accept. The argument that had been stuck for decades suddenly became clear: the two sides had been using different “or”s without knowing it.
The Secret Power of the Exclamation Mark
If linear logic just banned copying and erasing forever, it would be too weak to express most of mathematics. Girard’s next move was to reintroduce unlimited use — but only when you explicitly ask for it. He added two new symbols: ! (“of course”) and ? (“why not”), called the exponentials.
A formula marked with ! can be copied (contraction) and erased (weakening) as much as you like. It’s like saying, “This resource is not limited — feel free to reuse it.” The ? mark does the same on the other side of the logical fence. With these, you can recover both classical logic and intuitionistic logic inside linear logic. A classical implication “A implies B” can be read as “!A ⊸ B”, meaning you can use A as many times as needed. An intuitionistic implication works similarly, but with a careful restriction on how many conclusions you can draw.
This simple move turned linear logic into a kind of master logic. It doesn’t replace classical or intuitionistic logic — it contains them both, while adding a new resource-sensitive layer underneath that nobody had seen before.
Proofs Without a Script: The Invention of Proof Nets
Written proofs in a sequent calculus always have a step-by-step order, like a cooking recipe. But often the order doesn’t matter — you could do step 3 before step 2 and the result would be the same. This “bureaucracy of order” hides the real structure.
For the multiplicative fragment of linear logic (MLL), logicians found a gorgeous alternative: proof nets. These are graph-like pictures where formulas are nodes and the logical rules are links. Instead of a linear script, you see how all the pieces fit together at once. If someone hands you a tangled web and claims it’s a proof, you can check it by applying simple local rewriting rules — like tidying up a knot of string — until only a single tidy “net” node remains.
What makes proof nets so powerful? When you eliminate the cut rule (which glues two proofs together), you can do it locally — just rewrite a small spot without touching the rest. In normal proof systems, cut elimination can blow a proof up to enormous size, like a virus spreading through a computer. In MLL proof nets, it happens in linear time and stays clean. This gave computer scientists a new toolkit for designing efficient interpreters and for understanding parallelism: if two parts of a proof net aren’t connected, they can be processed at the same time without conflict.
Extending proof nets to the full linear logic, with additives and exponentials, turned out to be much harder. Researchers are still searching for a version that combines the same elegance with the full expressive power. That open problem is one of the reasons linear logic remains a hot topic today.
The Ultimate Puzzle: Is Linear Logic Decidable?
Every logician wants to know: can a computer decide, for every formula, whether it is provable? For some fragments of linear logic, the answer is yes — but it’s surprisingly expensive. Multiplicative linear logic (MLL) is already NP-complete: like solving a giant puzzle, checking a proof can take an enormous number of steps. Adding the additive connectives (MALL) pushes the problem up to PSPACE-complete, which is even harder.
The real cliffhanger comes with the full propositional linear logic (MELL, with exponentials). This system is so expressive that it can encode the behavior of Petri nets and vector addition systems — abstract machines that model how a factory’s conveyor belts might behave. The decidability of MELL — whether a computer could ever finish checking all formulas — is still disputed. Some researchers have published proofs that it is decidable; others claim those proofs contain errors, and the question remains open. In the meantime, we know that if it is decidable, it would be at least TOWER-hard — requiring a number of steps so huge it forms a tower of exponentials. This drama shows that a logic born from pure curiosity about resources has led straight into the deepest questions about what computers can do.
Why a Logic of Resources Matters to You
You probably don’t sit around writing sequent calculus proofs. But you already think in resource terms every day. When your phone battery is at 5%, you know a video call costs more than a text. When you bake cookies and the recipe says “one egg,” you can’t reuse the same egg twice. Classic logic would be perfectly happy pretending the egg is still there after you crack it — but reality isn’t so forgiving.
Linear logic matters because it gave us a precise mathematical language for exactly this kind of “how many times can I use it?” reasoning. That language now lives inside the design of programming languages that prevent memory leaks, in security systems that track who is allowed to access data, and in logic programming engines that can model a chemical factory or a board game. Whenever a system has to manage a limited set of things that can be created, transformed, and consumed, linear logic offers a way to reason safely and clearly.
The next time you share a bag of chips with friends or decide whether you can afford to skip a homework check, you’re doing linear logic in your head. The only strange part is that it took philosophers and logicians a whole century to catch up.
Think about it
- If you could only use each fact once in a debate, how would that change the way you argue with a friend?
- Can you think of a real-life situation where treating statements like limited supplies makes more sense than treating them as always true and reusable?
- If a computer program accidentally forgets that a resource was already used, what kinds of bugs or problems might happen?
