Can You Prove You Know? The Secret Logic of Reasons
When Seeing Isn’t Knowing: The Red Barn Puzzle
Imagine you’re driving through a strange town. Everywhere you look, you see barns — but most of them are just cleverly painted paper cutouts. Only one is real. Right in front of you, there’s a real red barn. You think, “I know that’s a red barn!” Yet, if almost everything around is fake, can you really be sure it’s a barn at all? This puzzle, inspired by a famous example from Alvin Goldman and Saul Kripke, shows how tricky knowledge can be.
Traditional epistemic logic, developed in the 20th century by thinkers like Georg Henrik von Wright (1916–2003) and Jaakko Hintikka (1929–2015), treats knowledge like a box: you know a statement if it’s true in every possible situation you can’t tell apart from your own. That idea works well for many things. But it can’t track why you know. In the Red Barn case, you see a red barn. Since there are no fake red barns, you do know there’s a red barn. And knowing there’s a red barn logically means you know there’s a barn. Yet your original feeling — that you don’t know it’s a barn — is still correct. Something is missing.
The missing piece is the reason behind your knowledge. Modal logic, with its boxes and possible worlds, doesn’t record that when you think “I know a barn,” you might be using the reason “because I see it,” which could be a fake-out. But when you think “I know a red barn,” your reason is different: “because I see a red barn and there are no fake red ones.” Justification logic fixes this by writing reasons directly into the language.
Proofs Are Reasons: From Math to Logic
The idea of tracking reasons didn’t start with fake barns. It began with mathematical proofs. In the early 1900s, the mathematician L.E.J. Brouwer insisted that in constructive mathematics, saying something is true means having a proof of it. The Brouwer-Heyting-Kolmogorov (BHK) semantics spelled out how proofs of compound statements work. For example, a proof of “A and B” is a pair: a proof of A and a proof of B. A proof of “if A then B” is a method to turn any proof of A into a proof of B.
Kurt Gödel (1906–1978) saw that this proof-based thinking could be captured using the classical modal logic S4, where the □ symbol means “it is provable.” He even defined a translation: prefix every part of a formula with □. But he faced a problem: his logic S4 claimed that if something is provable, then it’s true (□F → F), which is fine for mathematical proofs. However, if □ means “provable in a particular formal system,” then by Gödel’s own incompleteness theorems, the system couldn’t prove its own consistency. The puzzle remained.
The breakthrough came in 1995 when Sergei Artemov created the Logic of Proofs (LP). Instead of just □F, LP writes t : F, which means “t is a proof of F.” Now proofs became explicit objects, called justification terms. This finally gave the BHK semantics a precise logical home, linking intuitionistic logic, S4, and classical mathematical proofs.
A Toy Box of Reasons: How Justification Logic Works
Justification logic starts with ordinary true-false statements (called formulas) and adds a second kind of thing: justification terms. These terms are built from variables (like x, y, z for unknown reasons) and constants (like a, b, c for basic, unquestioned reasons), using a few simple operations.
The most important operation is application, written like multiplication. If you have a justification s for “If A, then B”, and a justification t for A, you can combine them to get s·t, which is a justification for B. This rule mirrors the way we naturally stack reasons: “If it’s raining, the sidewalk is wet” plus “I see rain” gives you a reason to believe the sidewalk is wet. We also have sum (+). If s justifies a claim F, then s + t also justifies F — you’ve just added extra material that might not be needed. Think of it like a book: if one chapter already proves a point, the whole book (chapter sum) still proves it.
Using these, justification logic can prove things like: if s : (A → B) and t : A, then [s·t] : B. That’s the explicit version of the modal law □(A → B) → (□A → □B), but with a crucial difference: the modal law says you automatically know everything that follows from what you know. Justification logic requires you to actually build the combined reason. That small difference solves the logical omniscience problem: real people don’t just know every logical consequence of their beliefs unless they have a justification chain.
Every system also needs constant specifications. These are a set of basic truths the thinker accepts as justified, like “e1 : (all men are mortal),” without digging deeper. The choice of constants lets us model skeptical or trusting agents.
Some systems also add factivity: the rule that if t justifies F, then F must be true (t : F → F). That’s the mark of knowledge, not mere belief. And positive introspection adds an operator ”!” so that if t justifies F, then !t justifies that t justifies F — the agent knows they have a reason.
Why 2+2=4 and Fermat’s Last Theorem Feel So Different
In everyday math talk, saying “I know 2+2=4” is trivial, while “I know Fermat’s Last Theorem” is a big deal. Yet in standard possible-world semantics, both are simply true in all possible worlds, so they’re equally “necessary.” This creates a puzzle called hyperintensionality: a context where logically equivalent sentences cannot be swapped without changing meaning. The philosopher Max Cresswell pointed out this problem in 1975.
Justification logic handles it naturally. Suppose Fermat’s Last Theorem (FLT) and 0=0 are both true and thus equivalent in truth. But that doesn’t mean a proof t of FLT is the same as a proof of 0=0. In justification logic, t : FLT and t : (0=0) are different assertions; they can have different truth values. So the logic respects the way something is justified, not just the bare fact. That’s why mathematicians can chat about who proved what without collapsing all true statements together.
Moreover, the logic provides a smart link: if there is a proof u that FLT and 0=0 are equivalent (i.e., u : (FLT ↔ 0=0)), and v is a proof of FLT, then by application we can construct f(u,v) that is a proof of 0=0. Reasonable connections between different justifications are maintained without forcing identity.
Mapping the Invisible: Connecting Modal Logic to Justification Logic
Modal logic systems like K, T, and S4 have been hugely successful for modeling knowledge and belief. Amazingly, each has a justification logic counterpart. You can think of the modal □ as meaning “there exists some justification.” If you take any theorem of, say, S4, and replace each □ with an explicit term, you can get a valid justification logic formula. This is the Realization Theorem, proved by Artemov and others.
For example, S4’s law □(□F → F) can be realized as something like x : (y : F → F), using factivity and introspection. Even more complex modal systems involving negative introspection (“if you don’t know, you know you don’t know”) or the Geach axiom (◊□X → □◊X) have justification counterparts, often requiring additional operations like ”?” for negative introspection or special function symbols. It turns out that the range of justification logics is infinite and still growing.
The Realization Theorem is powerful because it shows that whenever you have a modal argument about knowledge, there is an explicit justification version where each piece of reasoning is tagged with its reason. This connects the compact, implicit language of modal logic with the fine-grained, explicit language of proofs and evidence.
Why Your Reasons Matter Right Now
Justification logic isn’t just a toy for mathematicians. It gives us a way to talk about knowledge and belief that matches how we actually think. When you argue with a friend and say “I know that the movie starts at 7 because the ticket says so,” you’re using a justification term. The logic captures what happens when we combine reasons, trust axioms, or realize we were fooled.
It also explains why logical omniscience is unrealistic: you might know all the axioms of arithmetic, but you haven’t built the justification chain for every theorem. And in computer science, proof-checking programs rely on exactly these ideas to verify that a proof is correct, step by step.
The Red Barn from the beginning now makes sense: you have one justification u for “I believe it’s a barn” (just by looking), and another justification v for “I believe it’s a red barn” (looking plus noticing the color plus the absence of red fakes). When you apply the logical truth “B∧R → B” with justification a, you get a·v proving B — but that’s a different justification from u. So knowing B by the chain a·v doesn’t force u to be knowledge. Your original uncertainty was right, and the logic respects it.
Next time someone asks “How do you know?”, you can think of your reasons as terms waiting to be combined. Justification logic is the hidden engine behind every “because.”
Think about it
- If a detective uses a perfectly logical chain of reasons but one piece of evidence turns out to be planted, does the detective still “know” the conclusion? Why or why not?
- You believe it will be sunny because you check a weather app. Your friend believes it because they saw a rainbow yesterday. Both beliefs are true. Are the justifications equally good? Can you rank reasons?
- Can you think of a situation where having a good reason for something still didn’t make you feel certain? What would it take for you to say “now I really know”?
