The judge¶
A cleaning verifies every dirty value, to T or to F. For one claim the judge reports three readings at once:
- per occurrence — is the claim true under every reading of every occurrence? (strong Kleene logic's answer)
- per cleaning — is it true after every cleaning?
- as written — the value of the claim in the tables.
They combine into one disposition:
- EARNED / REFUTED — reading 1 is true / false: settled whatever the dirty values are.
- EARNED IF STABLE / REFUTED IF STABLE — reading 1 is undecided, but reading 2 is true / false: settled once the dirty values are verified, either way. The judge names the values that must stay the same until then.
- ON CREDIT / OPEN — readings 1 and 2 are undecided, and the claim as written is T / not T. ON CREDIT is true now, and some verification would refute it.
| claim, every atom dirty | as written | the judge says | why |
|---|---|---|---|
| p ∨ ¬p | F | EARNED IF STABLE | true after every cleaning; two reads of p may differ |
| p → p | F | EARNED IF STABLE | the same |
| ¬¬p | T | ON CREDIT | true now; verifying p as false refutes it |
| p | Z | OPEN | not established |
The value as written and the disposition can differ, and they answer different questions: p → p as written is F, because a check that reads p twice cannot rely on getting the same value; after verification it is true.
Check it yourself¶
In the browser: the ZTL studio. Through the public API:
curl -s -X POST https://api.ztljudge.com/judge \
-H 'Content-Type: application/json' \
-d '{"claim": "p -> p", "rows": [{"name": "p", "means": "it rains", "status": "unverified"}]}'
The answer's disposition is EARNED IF STABLE, with its meaning and the names to check. Both run on our server; to
run the judge on your own machine, clone the repository and, from its root:
python3 -c "import ztljudge; print(ztljudge.judge('p -> p', {'p': 'Z'})['disposition'])"