ZTL and other logics¶

This page states how ZTL relates to its neighbors: what is the same, what differs, and where. It ranks nothing. The counts compare definable functions and validities only; they say nothing about which logic is better. Each statement names the Lean theorem or the script behind it. A theorem is checked by the Lean kernel; a count marked MEASURED comes from running a script, and is not a theorem. The counts below were produced on 2026-10-30 by publications/core-logic/paper_numbers.py, publications/ztl/core_logic_checks.py and audit.py, on a checkout of inventor1975/ZTL at commit 4622dbe. The last commit that changed lean/ is b84526e; 4622dbe changes only CI workflow files.

The regression pool. Most counts are over one pool, generated by core_logic_checks.py: every formula of depth at most two over the atoms p and q, built with ¬, ∧, ∨, →, ⊕ and ↔ — 2 926 entries, 2 906 distinct formulas (MEASURED, paper_numbers.py, section A). It is exhaustive for that family, not a sample of logic as a whole, and a count of validities over it describes the pool; it is not a measure of a logic.

The words decisive register (ZTL's own tables, the value as written) and cautious register (strong Kleene logic) are used as in useful theorems.

Same input, different logics¶

One atom p, unverified. Classical logic has no value for an unverified atom, so its column shows the value under each of the two readings, p = T and p = F. In the strong and weak Kleene columns, Z is the middle value (Kleene's u, Bochvar's ½).

formula	classical (p = T / p = F)	ZTL, as written	strong Kleene	weak Kleene (Bochvar internal)	Bochvar external, ¬ = "is false"	Bochvar external, ¬ = "is not true"	the judge
`p ∨ ¬p`	T / T	F	Z	Z	F	T	EARNED IF STABLE
`¬¬p`	T / F	T	Z	Z	T	F	ON CREDIT
`p → p`	T / T	F	Z	Z	T	T	EARNED IF STABLE
`p ∧ ¬p`	F / F	F	Z	Z	F	F	REFUTED IF STABLE
`¬(p ∧ ¬p)`	T / T	T	Z	Z	T	T	EARNED IF STABLE

How each column was computed, on 2026-10-30:

classical, strong Kleene, weak Kleene and both Bochvar external columns: the connective tables defined in paper_numbers.py (its classical table, its strong Kleene evaluation by readings, its weak Kleene table, and its two conventions for Bochvar's external connectives), applied to each formula;
ZTL, as written: ev in ztl.py;
the judge: judge in ztljudge.py, with p marked unverified.

The ZTL, strong Kleene and weak Kleene columns were computed a second time in Lean, by #eval of evalF, of kev (lean/ZDirty.lean) and of Bochvar's weak Kleene connectives in lean/ZBochvar.lean, with the same results. The ZTL column was also evaluated as the B^e formula Boch.zeta φ with Boch.beval, and agreed with evalF on p ∨ ¬p, p → p and ¬¬p, as V.Boch.zeta_exact says it must.

Classical logic¶

On verified inputs ZTL computes exactly what classical logic computes. If every atom is T or F, every formula has the same value in both, for the whole language (evalF_agrees, lean/ClassicalAgreement.lean, a proof by induction on formulas, not a sample). MEASURED instance: over the regression pool, classical logic and ZTL have the same 584 validities on verified valuations, the same set (paper_numbers.py, section A).

Over its own valuations, where an atom may be Z, ZTL's set of tautologies is a proper subset of classical logic's. Every ZTL tautology is a classical tautology (ztl_taut_is_classical), and not conversely: p → p is classically valid and is F at p = Z (not_conversely). These theorems compare tautologies only; they do not compare the two consequence relations. This follows from admitting Z valuations: a tautology must be T at every valuation, and ZTL has valuations classical logic does not have. MEASURED: of the same pool, ZTL validates 212 formulas over all valuations with T, F or Z (paper_numbers.py, section D).

What changes with Z is set out law by law in the 26 laws: 12 still hold, 14 break, and the deduction theorem works in one direction only (V.dt_one_way). Of the inference rules listed there, 12 hold with Z and two (¬¬ elimination, a tautology in the conclusion) do not (MEASURED, core_logic_checks.py, section 4; each rule is also a Lean theorem, named on that page).

Telling unverified from false. The usual engineering move is to pick one default for an unverified atom, say "unverified := false", and compute classically. Under such a default an unverified atom is the same input as a false one, so no formula can tell them apart. ZTL, like Bochvar's external logic with ¬ read as "is false", can: ¬(p ↔ p) is T when p is Z and F when p is T or F (MEASURED, core_logic_checks.py, section 5). MEASURED, paper_numbers.py, sections C and H: the binary functions definable in ZTL are the 2 projections plus all 512 functions from pairs of T, F, Z into T and F, 514 in all; Bochvar's external connectives with ¬ = "is false" define the same 514; under "unverified := false" there are 18 (2 + 16). These are exact enumerations of all binary functions, not counts over the pool. With "unverified := false", classical logic is cell for cell Bochvar's external connectives in the "is not true" convention (MEASURED, all 48 cells, paper_numbers.py, section H).

Strong Kleene logic (K3): the cautious register¶

Strong Kleene is what the judge's first reading computes. Reading every occurrence of a dirty atom on its own, as T or as F, and asking what the formula can then be, gives exactly strong Kleene's value (V.rd_is_kleene, lean/ZDirty.lean). In the cautious register Z passes through to compounds; in ZTL's tables it never does: every compound formula is T or F (V.evalF_classical, lean/ZTL.lean).

Where the tables differ. MEASURED: ZTL's tables and strong Kleene's differ in 20 of the 48 cells of ¬ and the five binary connectives (paper_numbers.py, section J). Three of them:

cell	ZTL	strong Kleene
¬Z	F	Z
Z ∨ Z	F	Z
Z → Z	F	Z

Strong Kleene keeps the middle value; ZTL answers F, "not established", at the first connective.

Two consequences.

Strong Kleene's connectives are monotone: verifying an atom never takes back a T or an F already reached (V.kleene_not_monotone, V.kleene_and_monotone, V.kleene_or_monotone). ZTL's are not: ¬¬p is T with p unverified and F once p is verified F (V.eager_not_not_monotone, V.eager_and_not_monotone).
As consequence relations the two are incomparable. Strong Kleene keeps the rule ¬¬p ⊨ p, because its negation is an involution and an involutive negation forces that rule (Signature.involution_gives_dne); ZTL does not (V.rule_dn_elim_needs_ground). In the other direction ZTL validates ¬(p ∧ ¬p) (V.no_contradiction), while strong Kleene gives it Z at p = Z (the table above).

A function strong Kleene does not define. No strong Kleene formula in one atom computes "T unless the atom is Z, and then F" (V.kleene_cannot_say_established). Uniqueness of ZTL's tables, in a precise sense: any compositional semantics that agrees, at every valuation, with "strong Kleene value, then T if T and F otherwise" on ¬p and on each binary connective applied to two atoms agrees with ZTL on every formula (V.ztl_unique_compositional). Why the judge needs both registers is in section IV-bis of useful theorems.

Weak Kleene and Bochvar¶

Weak Kleene logic is Bochvar's internal logic (1938): the middle value is contagious, and any compound with a Z argument is Z. In the table above it gives Z on every row. ZTL's tables are not these.

Bochvar's external logic B^e adds to the weak Kleene connectives three operators, "is false", "is undefined" and "is true", and the constants. The relation to ZTL is proved in both directions (lean/ZBochvar.lean):

every ZTL formula translates into a B^e formula with the same value at every valuation (V.Boch.zeta_exact), so consequence is the same on both sides, with T designated (V.Boch.zeta_consequence);
every B^e formula that never takes the middle value has, at every valuation, the value of some ZTL formula (V.Boch.external_is_ztl).

So, up to bare atoms (which take the middle value in both), the truth functions of ZTL's formulas coincide with those of B^e's two-valued fragment, in another basis. This is a statement about truth functions and, by V.Boch.zeta_consequence, consequence; it does not cover the judge's readings. What is proved says where the reading differs.

Bochvar's own external connectives (a classical connective applied to "is true", with negation read as "is false" or as "is not true") are particular functions of that fragment, and they are not ZTL's. MEASURED, paper_numbers.py, section H: ZTL's ¬, ∧, ∨, →, ⊕, ↔ differ from them in 7 cells with ¬ = "is false" (→ at (Z, F) and (Z, Z); ↔ at (F, Z), (Z, F) and (Z, Z); ⊕ at (T, Z) and (Z, T)), and in 8 with ¬ = "is not true" (those seven and ¬Z). Over the regression pool, Bochvar's external connectives validate 548 formulas with ¬ = "is false" and 584 with ¬ = "is not true", against ZTL's 212 (section H). The p → p row of the table shows one of the seven cells: Z → Z is T for Bochvar's external implication and F for ZTL's.

SQL's NULL¶

SQL's NOT, AND and OR over NULL are strong Kleene's connectives, cell for cell, and not ZTL's: NOT NOT UNKNOWN is UNKNOWN, where ZTL's ¬¬Z is T (ZNull.toV_not, ZNull.toV_and, ZNull.toV_or, ZNull.not_the_greedy_register, lean/ZNull.lean). By those theorems and the strong Kleene column, a SQL evaluation would give UNKNOWN on every row of the table above, writing p → p as NOT p OR p. No SQL evaluation was run for this page; the statement rests on the theorems. What SQL then does with UNKNOWN depends on where it stands: WHERE drops the row, CHECK lets it pass. At WHERE, SQL and the ZTL verdict agree on every condition in negation normal form (ZNull.where_agrees_nnf); at CHECK they part already on TRUE AND NULL (ZNull.check_departs_on_conjunction). Details, with IEEE NaN and taint tracking beside it, are in section XV of useful theorems.

The judge's place¶

The judge does not pick one of these logics. It reports three readings of one claim and combines them:

EARNED and REFUTED are strong Kleene's T and F. In ztljudge.py this holds by construction: judge assigns them from the cautious-register value that check computes. MEASURED over the 14 530 dirty cells of the regression pool, against an independent strong Kleene evaluation in paper_numbers.py: the judge said EARNED on 2 450 cells, every one strong Kleene T, and REFUTED on 1 274, every one strong Kleene F (section P).
EARNED IF STABLE and REFUTED IF STABLE are classical logic over the cleanings: T (or F) under every replacement of the dirty atoms by T or F, where strong Kleene is undecided. The judge's grant, EARNED or EARNED IF STABLE, is exactly "T in every cleaning" (V.Speak.grant_iff_enum, lean/ZSpeaks.lean).
ON CREDIT and OPEN are the rest, told apart by ZTL's value as written.
The program has one more disposition, E, for a claim that rests on a subject declared missing; it is not in the Lean model.

Each of the six dispositions of the Lean model is itself the T value of some ZTL formula over the claim's atoms (V.Speak.judge_speaks_ztl). These theorems are about the Lean model of the judge; the program is tested, not proved (see what ZTL does not do).

Recompute¶

From a clone of the ZTL repository, at its root:

python3 publications/core-logic/paper_numbers.py   # sections A, C, D, H, J, P
python3 publications/ztl/core_logic_checks.py     # sections 4 and 5
python3 -c "import ztl, ztljudge; print(ztl.ev(('imp', 'p', 'p'), {'p': 'Z'}), ztljudge.judge('p -> p', {'p': 'Z'})['disposition'])"

The last line prints F EARNED IF STABLE.