What Does “And” Mean? It’s All About the Rules
A Fork in the Road: Two Ways to Explain “And”
Imagine you’re building a robot friend who speaks your language. You program it to understand the word “and.” How do you do it? One way is to give it a truth table: “A and B” is true exactly when A is true and B is true. Simple. But there is another way. You could teach the robot the rules of proof: If you have A and you have B, you may combine them to say “A and B.” And from “A and B” you may pull out A alone or B alone. If the robot learns those rules, does it know what “and” means?
These two strategies represent a deep split among philosophers of logic. The first view—denotationalism—says that a word’s meaning is what it points to in the world, often captured by truth conditions. The second view—inferentialism—says that meaning comes from the inference rules we use when we reason. This second view leads to a whole research program called proof-theoretic semantics. It asks: could the rules for proving a statement actually be the meaning of the logical words inside it?
The battle isn’t just about “and.” It touches “if…then,” “or,” “not,” and much more. And it forces us to rethink what truth itself is.
Gentzen’s Radical Idea: Introduction Rules as Definitions
In the 1930s, the German logician Gerhard Gentzen (1909–1945) designed a new way of writing proofs. He called it natural deduction, and it looked like a branching tree. At the top were assumptions. At the bottom was the final statement. In between, there were only two types of steps for each logical word: introduction rules and elimination rules.
Take “if…then,” written with the arrow ( \to ). The introduction rule says: if you assume A and from that assumption you deduce B, then you may drop the assumption and conclude ( A \to B ). In a picture, you might draw a box around the temporary assumption A, and inside the box you derive B; then you can close the box and write ( A \to B ).
The elimination rule for ( \to ) is the familiar modus ponens: from ( A \to B ) and A, you may infer B. Together, these rules feel perfectly balanced. You can introduce the arrow when you’ve shown B follows from A, and you can eliminate it by feeding it an A to get B.
Gentzen believed that the introduction rules actually define the logical word. He wrote that the introductions “represent, as it were, the ‘definitions’ of the symbols concerned, and the eliminations are no more than the consequences of these definitions.” In other words, the meaning of ( \to ) is the rule that lets you build it, and the elimination rule is just a way of using that meaning—it shouldn’t add anything new.
This harmony between introduction and elimination became the heart of proof-theoretic semantics. If you’ve ever noticed that “and” feels like both a combination rule and a splitting rule, you’ve felt that harmony.
Prawitz’s Puzzle: What Makes a Proof Valid?
The Swedish logician Dag Prawitz (born 1936) took Gentzen’s idea and asked: when is a proof genuinely correct, not just shaped like a proof? He noticed something important. Sometimes a proof contains a detour: an introduction rule immediately followed by an elimination rule for the same word. That’s like building something just to take it apart. For example, you might assume A, deduce B, introduce ( A \to B ), and then—right away—combine it with A to get B. But you already had B! The extra steps are pointless.
Prawitz showed that any such detour could be reduced: you could transform the proof into a simpler one without the loop. He called this normalization. A proof that has no detours is in normal form. In intuitionistic logic—a system that avoids certain classical rules—every closed proof (a proof with no assumptions left hanging) can be reduced to a normal form whose last step is an introduction rule. That fact is called the introduction form property and has become so central that some philosophers call it the “fundamental assumption” of proof-theoretic semantics.
On this view, a proof is valid if it stands in the right relationship to introduction rules. A closed canonical proof—one that ends with an introduction—is valid when its immediate subproofs are valid. Non-canonical proofs are valid if they can be reduced to valid canonical ones. Open proofs (those with assumptions) are valid if every closed copy you get by plugging in valid proofs for the assumptions is valid.
This definition doesn’t just describe what a proof looks like; it tells you what a proof is. And because the meaning of a logical word is given by its introduction rules, a valid proof is one that respects that meaning all the way through.
Martin-Löf’s Machine: Proofs as Objects
The Swedish mathematician Per Martin-Löf (born 1942) pushed the idea even further. In his type theory, proofs aren’t just written lines—they are objects you can name and handle. A statement isn’t just true or false; it is a type, and having a proof of it is like having a piece of data that fits that type. You can write a judgment like t : A, which means “the object t is a proof of the proposition A.”
Here the introduction rule for ( A \to B ) has a very concrete meaning: a proof of ( A \to B ) is a function—a recipe that, whenever you give it a proof of A, builds you a proof of B. If you have such a function, and then you get a proof of A, you can apply the function and out pops a proof of B. That’s exactly what the elimination rule does.
Martin-Löf distinguished two layers: the demonstration layer, where you actually argue and convince someone, and the proof object layer, where the meanings are explained. You can think of it like this: when you solve a math puzzle, the demonstration is your written explanation, while the proof object is the mental construction that makes the answer work. The object layer is where the logical words get their meaning.
One big difference from Prawitz: Martin-Löf did not stand outside the system and label which proofs are valid. The rules that tell you what counts as a proof are part of the same system—you can’t even talk about a proposition being meaningful unless you already know what counts as a proof of it. This makes his approach deeply constructive: a statement is true only if a proof has actually been constructed.
Why Intuitionists Don’t Like “Or”
Proof-theoretic semantics is closely tied to a philosophical position called anti-realism, championed by the British philosopher Michael Dummett (1925–2011). Realists believe that every statement is already true or false, whether we can discover it or not. Anti-realists say: if you can’t, even in principle, get a proof one way or the other, it doesn’t make sense to claim the statement is definitely true or false.
This leads straight to a famous logical law: the law of excluded middle, which says that for any statement A, either A or not‑A must be true. In classical logic, that’s a basic principle. But in the intuitionistic logic that underlies most proof-theoretic semantics, you can’t just assert ( A \lor \neg A ) without having a proof of A or a proof of its negation. The same goes for the rule that from a contradiction anything follows—ex falso quodlibet—which intuitionists treat with suspicion.
Why does natural deduction push us toward intuitionistic logic? In natural deduction, if you use the classical rule of indirect proof (assuming ( A \to \bot ) to prove A), the neat division of labour between introduction and elimination breaks. The rules start mixing different logical words, and proofs can get stuck—they no longer obey the introduction form property. For many proof-theoretic semanticists, that’s a sign that classical logic gets meaning wrong.
Dummett argued that this logical choice matches a philosophical one: anti-realism. If meaning is tied to our ability to prove, then reality cannot be thought of as something that’s already settled, forever beyond our reach.
So What? Meaning, Truth, and Your Own Logic
You might think all this is just a puzzle for logicians with chalk dust on their sleeves. But the debate seeps into everyday thinking. Every time you say “If it rains, the picnic is off,” you’re using a rule of inference. According to proof-theoretic semantics, the meaning of that sentence doesn’t come from some cloudy version of all possible worlds where it rains and the picnic gets cancelled. It comes from how you would go from evidence of rain to a decision to cancel—the proof steps you’d actually follow.
This changes how we design software that reasons, how we teach children logic, and what we count as understanding a word. It also asks us to wonder: when two people disagree about what’s true, are they disagreeing about facts, or about what counts as a proof?
The girl at the fork is all of us. We’ve learned words like “and,” “or,” and “if” through rules we barely notice. Proof-theoretic semantics suggests that those rules aren’t just handy shortcuts—they are the meaning. And that means the next time you put together a chain of reasoning, you aren’t just following a track: you’re building the very shape of what you mean.
Think about it
- If you understand “and” because of the rules you learned, could someone who learned different rules for “and” mean something completely different—and would they still be wrong?
- Imagine a machine that can prove every true mathematical statement. Would you then think of “truth” as the same thing as “what the machine can prove”?
- If you can’t prove there is life on a distant planet, and you can’t prove there isn’t, does it still make sense to say that either there is or there isn’t—right now?
