Proved. The judge's dispositions, their properties and the translation to Bochvar's logic are theorems checked by
the Lean 4 kernel with an empty axiom list — no excluded middle, no choice — in
lean/ZSpeaks.lean,
lean/ZDirty.lean and
lean/ZBochvar.lean. The kernel checks the
statements as formalized; whether the short definitions there match the prose here is for you to judge. The program
is tested against them, not proved.
Nothing new in what it computes. ZTL computes the same two-valued functions as Bochvar's external formulas (1938),
in another basis — proved both ways in ZBochvar.lean. For classical logic a change of basis is cosmetic; for ZTL it
is not, because each connective is one check and its table says what one check may grant.
Two of the judge's readings are known. Readings 1 and 2 are the compositional and the thorough semantics of
three-valued model checking (Bruns and Godefroid, 1999;
2000). Reading 3 is ZTL's.
One measured difference. Our regression pool holds every formula of depth at most two over two atoms, at every
valuation with a dirty atom. Over the true verdicts of its compound formulas, ZTL and Bochvar's external connectives
(in both conventions in use) give the same 2 448 verdicts that every reading forces, and ZTL gives 3 738 that no
reading forces, against 5 090 and 5 358 for Bochvar's. An unforced T is a grant that no reading of the data supports;
ZTL gives fewer, though not none and not in every cell. Per connective this holds by construction; on compound
formulas it does not follow from the definitions, so it is measured.