What If You Could Assume Anything? The Logic of “What‑If” Boxes
A Strange New Rule: Arguing Inside a Box
You are arguing with a friend about whether it will rain. You say, “Suppose for a moment it does rain. Then we would need umbrellas. So if it rains, we will need umbrellas.” You do not really know that it rains—you just temporarily assume it to see where the idea leads. That is a natural move in everyday reasoning.
In the early 1930s, two logicians independently turned this everyday trick into a revolutionary way of doing logic: natural deduction. Gerhard Gentzen (1909–1945) and Stanisław Jaśkowski (1906–1965) both designed systems in which proofs could contain subproofs—parts of the argument that depend on temporary assumptions, exactly like your “suppose it rains” moment. Jaśkowski drew literal boxes around these subproofs. Gentzen used a different style, with formulas hanging from the leaves of a proof tree.
Later, Frederic Fitch (1908–1987) simplified the boxes into vertical lines with a short horizontal line—a style still used in many logic textbooks. The central insight was the same: you can reason inside a box, treating the assumption as true. But you may not take anything out of the box that relied on that assumption until a special rule closes the box. Once closed, you can assert a new formula that does not depend on the assumption—like “If it rains, we will need umbrellas.”
How to Build a Proof: Introduction and Elimination Rules
Natural deduction treats logical connectives as building blocks. For each one—and, or, if…then—there are two rules. An introduction rule tells you how to build a sentence that uses that connective. An elimination rule tells you how to use a sentence that already has it.
Take and. Introduction says: if you have two separate statements, like “It is raining” and “The ground is wet,” you can combine them into one: “It is raining and the ground is wet.” Elimination lets you pull out either piece. From the whole conjunction, you can conclude “The ground is wet” alone.
The real power appears with if…then (the conditional). Its introduction rule uses a subproof. You put the “if” part inside a box as a hypothesis. If you manage to reach the “then” part inside that box, you close the box and assert the whole conditional—without ever proving the hypothesis is actually true. That matches your weather argument exactly. The elimination rule, modus ponens, says: if you have “If A then B” and you also have A, you get B.
These rules are designed so that the elimination rule just undoes what the introduction rule does. You should never get more out than you put in. The philosopher Arthur Prior (1914–1969) showed how bad things get when rules do not match. He invented a fake connective he called tonk. Its introduction rule: from A infer “A tonk B.” Its elimination rule: from “A tonk B” infer B. With both rules, you could prove anything from anything—a disaster. Prior’s joke made it clear that introduction and elimination rules must be in harmony. The elimination rule must not give you extra power beyond what the introduction rule already granted.
The Danger of Detours: Straightening Out Proofs
Because natural deduction’s rules come in symmetrical pairs, a proof can sometimes take a pointless detour. Suppose you introduce a conditional—assume A, get B, close the box, and obtain “If A then B.” Immediately afterward, you use that conditional with A (still available) to get B again by elimination. That is like walking around the block only to end up right where you started.
Gentzen realized you could always “straighten out” such detours. Instead of applying introduction then elimination, you could simply use the steps from inside the subproof directly. He called this process normalization. A proof in normal form has no wasted loops. Every formula in it is a part—a subformula—of the original assumptions or the final conclusion. That neatness helps mathematicians and computer scientists trust proofs.
For a long time normalization was only fully understood for intuitionistic logic, the constructive logic Gentzen built. Classical logic, with its extra rule for indirect proof (roughly: “if assuming not‑A leads to a contradiction, then A is true”), seemed to resist a clean normalization. But in 2012, logicians Jan von Plato and Annika Siders found a clever way to extend normalization to classical natural deduction. They rearranged the order of rules to remove “classicizing detours.” The result showed that even classical proofs can be made clean—and that the ideal of harmony might stretch further than Gentzen feared.
The Big Fight: Which Logic Is the True One?
The neat, harmonious structure of natural deduction led some philosophers to a bold thought. Maybe the right logic—the one that captures genuine correct reasoning—must have introduction and elimination rules that are perfectly balanced for all its connectives. Classical logic’s rule for indirect proof did not seem to have an elimination twin that matched it naturally. Intuitionistic logic, on the other hand, did. So they suggested that intuitionistic logic, not classical, is the One True Logic.
The most famous defender of this view was Michael Dummett (1925–2011). He argued that the meaning of a logical word (like ‘or’ or ‘if’) is given entirely by the rules for its use—its introduction and elimination rules. This idea, called inferentialism, says you do not need to talk about truth in some mysterious outside world. You only need to know how the word works in arguments. Dummett went further: if meaning comes from use, then learning a language cannot involve grasping a hidden realm of facts. Classical logic, he thought, relied on the idea that every statement is either true or false even if we cannot know it. That, Dummett claimed, forced classical logic into a kind of meaning holism that makes language learning impossible. He called his position anti‑realism—the view that our linguistic practices create meaning, rather than simply pointing at ready‑made facts.
Not everyone agreed. Critics pointed out that you could reformulate classical rules to fit the harmonious pattern. Others thought the jump from logical rules to all of language and reality was too quick. Still, the debate over harmony and inferentialism remains alive in philosophy today. It forces us to ask: how much of our thinking comes from the rules we follow, and how much from the world we describe?
Why It Still Matters: From Computers to Everyday Language
Today, natural deduction is not just a historical curiosity. Its subproof structure matches the way programmers think about temporary local variables. Many computer proof assistants—programs that check mathematical arguments—use natural deduction at their core. The idea of “assume this, then that, then close the box” translates directly into code.
But the philosophical spark touches your life even more directly. Every time you say, “Assuming for the sake of argument that you are right…” you are drawing an invisible natural deduction box in the air. The inferentialist thought—that meaning might be nothing more than rules of use—echoes in how children learn language. They pick up the patterns for saying “and” or “because” without ever being told what the words “stand for” in the world.
The big unsettled question, born with those first boxes in 1934, is still with us. Does our reasoning create the structure of correct thinking, or does it discover a structure that was already there? Next time you imagine a temporary “what if,” you are stepping into a conversation that started with a simple trick of drawing a box around a thought.
Think about it
- If you can temporarily assume anything—even something you know is false—just to see where it leads, can you ever prove something true about the real world? Why or why not?
- Some philosophers say the meaning of ‘and’ is completely captured by its rules (for example, from “A and B” you can conclude “A”). Do you think a word’s meaning can be reduced to its rules of use, or does it need something more—like pointing to real objects? What about a word like ‘justice’?
- Imagine two systems of natural deduction where the rules are perfectly balanced—introduction and elimination match exactly. But the two systems disagree on whether “A or not A” is always a valid claim. How could we decide which system is the “right” one? Would the idea of balance itself help us choose?
