The rule¶
An atom is T (true), F (false) or Z — dirty: not ours, it may change between two reads. Each occurrence of a dirty atom is read on its own. That is a modelling choice, and it is yours to make: if your program reads a value once into a variable, write that value once. Which atoms are dirty is also your input.
One rule generates every connective:
A connective is false whenever some reading of its arguments makes the classical connective false, and true otherwise.
An argument that is a dirty atom can be read as 1 or 0; an argument that is itself a compound is read as the verdict it already recorded. So every compound is T or F, and Z occurs only on atoms: the atoms have three values, the connectives answer with two. Negation: ¬T = F, ¬F = T, ¬Z = F. Three binary connectives (rows: the left argument):
| ∧ | T | F | Z |
|---|---|---|---|
| T | T | F | F |
| F | F | F | F |
| Z | F | F | F |
| ∨ | T | F | Z |
|---|---|---|---|
| T | T | T | T |
| F | T | F | F |
| Z | T | F | F |
| → | T | F | Z |
|---|---|---|---|
| T | T | F | F |
| F | T | T | T |
| Z | T | F | F |
A T says: every reading of what this check reads makes it true. An F says: not established — not that the data are false. Because a check reads the recorded verdict of a compound, ¬¬p on a dirty p is T: the inner check records F (p might be true), and the outer check negates that record. Whether such a T survives verification is the judge's question.