Hardy's paradox: a contradiction, on one condition¶

Vitaly Reznik

This page claims no new physics. It shows what the logic behind this site, ZTL (Zero-Trust Logic), does with a famous quantum puzzle, next to what two other logics do with exactly the same input. The difference is the point.

The paradox¶

Alice and Bob share a pair of particles, prepared together and then sent apart. Each of them can ask their own particle one of two questions:

question 1, whose answer is 0 or 1;
question 2, whose answer is + or −.

Each can ask only one question in a run: asking one spoils the other, so the two cannot be asked together.

In 1992–93 the physicist Lucien Hardy described a way of preparing the pair for which quantum mechanics predicts the following, and experiments agree:

Alice asks	Bob asks	what quantum mechanics predicts
2, and gets −	1	Bob gets 1. Always. (fact 1)
1	2, and gets −	Alice gets 1. Always. (fact 2)
1	1	never both 1 (fact 3)
2	2	both get − in about one run in twelve (fact 4)

Take a run of the last kind, where both asked question 2 and both got −, and reason:

Alice got −. By fact 1, if Bob had asked question 1 instead, he would have got 1.
Bob got −. By fact 2, if Alice had asked question 1 instead, she would have got 1.
So both answers to question 1 would have been 1.
But by fact 3 that never happens.

A contradiction, from four true facts.

The same input for three logics¶

I wrote the run as plain statements:

verified (actually observed): "Alice asked question 2 and got −", "Bob asked question 2 and got −";
unverified (nobody observed them): "Alice's answer to question 1 would be 1", "Bob's answer to question 1 would be 1";
the claim: facts 1, 2 and 3, applied in this run, with each "if… had asked" written as a plain "if… then" about the unasked answer.

Nothing about states, waves or probabilities. The choice of what is verified and what is not is mine, and it is the obvious one: the questions nobody asked are the ones whose answers nobody saw.

Then three logics read the same statements.

logic	what it says about the chain
classical logic	A contradiction. No values of the two unasked answers make all three facts true at once.
strong Kleene logic (a three-valued logic in which "unknown" simply passes through)	Undecided. It says neither true nor false, and nothing about why.
ZTL	A contradiction — if each unasked answer is one and the same in every step that uses it. If each place where an unasked answer appears is read on its own, there is no contradiction. The two answers to check are named: Alice's and Bob's answers to question 1.

The first two answers I computed directly; the third is the verdict of ZTL's public judge, which anyone can reproduce with the command at the end of this page. In the judge's own words:

false in every completion: refuted if each name … reads the same at every occurrence; read each occurrence on its own and it is NOT refuted.

Why the difference matters¶

Classical logic gives a verdict with no condition. Whoever trusts it must then decide by themselves which of the premises to drop — and over the years many concluded that something must pass between the particles.

Kleene logic gives no verdict. It is honest about not knowing, but it does not say what it would need to know.

ZTL gives a verdict with its condition: the contradiction exists only if a question nobody asked has one answer, the same in every step of the argument. It puts the hidden assumption on the table and names the two values it rests on. And those two can never be checked: in this run the questions were not asked, and cannot be asked afterwards.

I also ran three checks:

Each fact alone is not refuted by the run. Facts 1 and 2 stay open; fact 3 holds, but only on credit, resting on answers nobody checked.
One name per step — "Alice's answer to question 1 in the step of fact 2" and "… in the step of fact 3" as two separate statements, and the same for Bob: the judge says open, no contradiction.
A control, where the judge could have doubted what was really seen: a run in which Alice got − and Bob really did ask question 1 and got 1. The judge: fact 1 established for that run.

What ZTL does and does not do here¶

It does not do new physics, and it does not solve the paradox. Whether the lesson is that unasked questions have no answers at all (Asher Peres's view: unperformed experiments have no results, 1978), or that the answer on one side depends on what is chosen on the other (the reading behind Henry Stapp's 1997 argument for non-locality), ZTL does not decide — the next section shows how far it does get. Both reject a single answer valid in every situation; they differ on why. ZTL only shows that the contradiction needs that single answer.

It is not a trick tailored to physics either. The caveat "if each name reads the same at every occurrence" is general: ZTL attaches it to any conclusion that uses an unchecked value more than once. It was added to the judge on 29 October 2026, before it was applied to this paradox, for a reason in logic itself — so that "if p then p" and "not (p and not p)" would be judged consistently. Its message describes it in terms of ordinary data: no change between the check and the use, the same meaning in premise and conclusion.

What it does is the thing a careful reasoner should do and classical logic does not: it refuses to draw a conclusion from unchecked values without saying, out loud, what it assumes about them.

Peres or Stapp? We ran that too¶

ZTL does not take sides — but the two sides can be put to it. This time each unasked answer is named by what the other side chose: "Alice's answer to question 1 when Bob asks question 2", "… when Bob asks question 1", and the same for Bob. Whether those differ is exactly what the quarrel is about.

asked of the judge	verdict
the three facts, on their own	open — no contradiction
Stapp's thesis: an unasked answer depends on what the other side chose	on credit — rests only on unchecked values
the opposite: it does not depend on the other side	open
the three facts and "it does not depend on the other side"	refuted (if stable) — a contradiction
the facts imply: if the unasked answers exist, at least one depends on what the other side chose	established (if stable)

The last line is the part both sides accept, and ZTL establishes it: if questions nobody asked have answers, those answers must depend on the choice made on the other side. That is what Hardy's argument proves.

The quarrel is about the "if". Stapp takes the answers to exist, and concludes that something depends on a distant choice. Peres denies they exist, and the conclusion has nothing to stand on. For ZTL this is a question about values that can never be checked: in this run the questions were not asked, and cannot be asked afterwards. So Stapp's thesis stays on credit for good, and its opposite stays open: neither can ever be established. That is not indecision on ZTL's part: no observation can tell the two readings apart, because they predict the same results for every experiment.

So ZTL does a little more than refuse to choose. It proves the part the two sides share, and it shows why the choice between them cannot be settled by checking anything.

To check the established line yourself (the same rows as above, with these six names):

curl -s -X POST https://api.ztljudge.com/judge -H 'Content-Type: application/json' -d '{
  "rows": [
    {"name": "xa", "means": "Alice asked question 2 and got minus", "status": "verified", "ground": "run-17-alice"},
    {"name": "xb", "means": "Bob asked question 2 and got minus", "status": "verified", "ground": "run-17-bob"},
    {"name": "za2", "means": "Alice'"'"'s answer to question 1, when Bob asks question 2", "status": "unverified"},
    {"name": "za1", "means": "Alice'"'"'s answer to question 1, when Bob asks question 1", "status": "unverified"},
    {"name": "zb2", "means": "Bob'"'"'s answer to question 1, when Alice asks question 2", "status": "unverified"},
    {"name": "zb1", "means": "Bob'"'"'s answer to question 1, when Alice asks question 1", "status": "unverified"}],
  "claim": "((xa -> zb2) & (xb -> za2) & ~(za1 & zb1)) -> (~(za2 <-> za1) | ~(zb2 <-> zb1))"}'

The answer contains "disposition": "EARNED IF STABLE".

Where physicists stand¶

The assumption ZTL names is the one physicists have argued about for decades. We did the run first and looked at the literature afterwards; that is how we work.

Peres (1978), above. David Mermin and William Unruh located the weak point of Stapp's argument in its statements about measurements that were not made. Robert Griffiths, in his "consistent histories", showed that statements belonging to sets of questions that cannot be asked together may not be combined in one argument; with that rule Hardy's contradiction does not arise.
Samson Abramsky and Adam Brandenburger (2011) placed Hardy's paradox in a general picture, contextuality: each situation taken alone is consistent, but no single assignment of answers fits all of them together. A 2026 paper (Liu, Wang and colleagues, arXiv:2601.01445) proves that, for finite scenarios of ideal measurements, a Hardy-type paradox exists exactly when the scenario is contextual in this sense.
Ehtibar Dzhafarov and Janne Kujala's contextuality by default (2015) treats the same property measured in different situations as different variables from the start, and measures contextuality by how far they can be matched up. The judge's "one name per step" reading is a cruder version of the same first move — without the measuring part.

Check it yourself¶

The judge is public. This command sends the run, as written above:

curl -s -X POST https://api.ztljudge.com/judge -H 'Content-Type: application/json' -d '{
  "rows": [
    {"name": "xa", "means": "Alice asked question 2 and got minus", "status": "verified", "ground": "run-17-alice"},
    {"name": "xb", "means": "Bob asked question 2 and got minus", "status": "verified", "ground": "run-17-bob"},
    {"name": "za", "means": "Alice'"'"'s answer to question 1 would be 1", "status": "unverified"},
    {"name": "zb", "means": "Bob'"'"'s answer to question 1 would be 1", "status": "unverified"}],
  "claim": "(xa -> zb) & (xb -> za) & ~(za & zb)"}'

The answer contains "disposition": "REFUTED IF STABLE" and lists za and zb to check. Replace them with one name per step (za2, za3, zb1, zb3, claim (xa -> zb1) & (xb -> za2) & ~(za3 & zb3)) and the answer is OPEN. The same documents can be pasted into the studio, which explains the verdict in plain words.

The judge is open source, in inventor1975/ZTL (ztljudge.py). An earlier analysis of the same paradox, with the quantum amplitudes checked in exact whole-number arithmetic in Lean 4, is lean/Hardy.lean there, with the program dilemmas/hardy.py.