ZTL — Zero-Trust Logic

ZTL (Zero-Trust Logic) is a three-valued logic whose every connective is two-valued, generated by one principle: truth is never granted on credit — a connective returns T only if T is forced under every classical reading of the unverified. Its values are T, F and Z, the mark of an unverified atom; Z is barred from the value of any compound (the greediness theorem, machine-checked): above the atoms the algebraic value already is the logical value, so — beyond Suszko's logical two-valuedness, which every structural logic has — ZTL is bivalent on compounds by construction, and the reduction's non-truth-functionality is confined to connectives applied directly to atoms. The one asymmetric cell, ¬Z = F, gives the values an order of birth, proved over the whole language: under pure doubt F is born first and T only through an F (lean/ZOrigin.lean, empty axiom list) — an order classical logic, whose negation is an involution, does not have. Versions up to 2.0.0 called ZTL "two-valued with a mark"; 2.1.0 corrects the name, not a single measured or proved fact. Its identity among the three-valued matrices is precise and machine-checked at its cause: a single rule, ¬¬p ⊨ p, separates its consequence relation from each of its four involutive-negation neighbours (K3, LP, weak Kleene, Łukasiewicz Ł₃), and by one lemma from any three-valued matrix with involutive negation. Its relation to classical logic has two halves, both machine-checked, and a name. On verified data the two logics are the same: every formula takes the same value under every mark-free valuation (evalF_agrees, empty axiom list), and on the regression pool of 2926 formulas over two atoms the two validate the same 588 formulas, element for element — not one classical law is given up. On unverified data ZTL decides where classical logic cannot take the input: of twenty-six classical laws, twelve continue to hold on a marked atom and fourteen are refuted with an exhibited witness, none left open — fourteen theorems about unverified data (*_needs_ground in Lean), where classical logic decides none of the twenty-six. The mark is expressible inside the language (isZ(x) = ¬(x↔x)), and on 1840 of 2924 compounds of the pool the verdict depends on whether an atom is unverified or false — a distinction the usual substitution "unverified := false" cannot draw at all. That substitution is shown to be Bochvar's external logic of 1938, cell for cell on every binary connective; ZTL parts from it in eight cells, each a place where a verdict is derived from the absence of information. No default replaces the mark: in the taint-sink case both classical defaults grant a pass to an unverified sink, and a rule with one atom in both polarities has no conservative default at all. Hence, as a decision procedure, ZTL strictly dominates classical logic; as a system of proofs on classical logic's own domain the two are exactly equal (ztl_taut_is_classical) — "stronger", which in logic means "proves more", is a word the paper does not use of itself. That the logic is not arbitrary is evidenced case by case: six independent engineering traditions — IEEE 754 NaN, SQL NULL, taint tracking, abstract interpretation, imprecise probabilities, and provenance semirings — have each reinvented a fragment of the same discipline, and for each its own semantics is formalised as the tradition states it, with a theorem on the empty axiom list placing ZTL's verdict inside it — an embedding of the algebraic core, not of the whole tradition; the unformalised remainder is named in each case. For this logic the preprint builds: the census of the twenty-six classical laws on a marked atom (twelve hold there, modus ponens among them; fourteen are refuted with a witness, every one a law of "truth from form"; none is left undecided); the split between rules and laws with a one-directional deduction theorem for the primitive arrow; a signed tableau calculus with machine-proven soundness, completeness and cut admissibility, and a syntactic cut-elimination procedure with its bound as a function; an algebraic passport — expressive completeness of the external layer, a definable implication with the full deduction theorem, Craig interpolation, and the Blok–Pigozzi conditions verified on the matrix (ZTL is algebraizable, yet not self-extensional); quantifiers over finite and arbitrary domains, with the parameter tableaux ported to Lean — every rule proved sound, a search built and proved sound, the finite half of completeness a theorem and the infinite half stated and left argued; first-order identity (a = predicate whose reflexivity is an earned verdict — self-identity falls to Z on an unverified reference — while Leibniz's law licenses substitution only through an earned equality) and free logic with definite and indefinite descriptions (a non-denoting term takes the mark, not F and not a gap; existence is earned self-identity; excluded middle on a non-denoting atom is F — the greedy collapse setting ZTL apart from the neutral free-logic school; Hilbert's ε earns denotation exactly when a witness exists), both now proved for an arbitrary domain; modal and probabilistic identifications, the latter a theorem for every finite frame and every proper mass assignment; a theory of verification (a verdict is a pair "value + warranty": sound — never lies; hereditary — never revoked) whose receipt is bounded from both sides and whose three uncomputed grades are proved hard — the hereditary grade is a tautology check (coNP-hard), the exact width of an inquiry and the exact receipt are NP-hard — so the judge's cheap cuts are forced rather than chosen; evidence combination (conflict is never renormalized; Zadeh's paradox is a theorem); and a quarantine passport typing every refusal by its genesis — paradox, intrinsic, underdetermined, unverified input, inherited — with a measured stipulation theorem. The classical paradoxes (the liar, Jourdain's carousel, Curry, Yablo — now at the limit, without a classical step — the crocodile, Russell) receive a uniform diagnosis: pointwise quarantine instead of explosion. The entire development — seventy-one Lean 4 modules — is machine-checked with an EMPTY axiom list (no classical choice, no quotients, not even propositional extensionality; definitions included): 1194 theorems, each audited individually; no section of the paper rests on measurement alone. Every numerical claim is reproducible by the repository's regression (162 test stands). As of v2.0.0 the repository is the logic itself — the Lean corpus, the papers, and the ZFL formal language with its tooling; the seven-language taint analyzer and the natural-language studio that translates into ZFL (both of which vendor a copy of this core) have moved to their own repositories, github.com/inventor1975/introspect and github.com/inventor1975/ztlstudio. Functionally the {not, and, or} fragment coincides, cell by cell, with the external layer of Bochvar's logic (1938) — a kinship found in the literature search after the tables had been generated, not a source; the contribution is the generating principle, an implicational floor outside the Rosser–Turquette standardness conditions, the calculus, the machine verification, and the bridges to the engineering traditions. What is new in v2.1.1 (same day) — the header only: the v2.1.0 PDF went out with the working draft's header ("draft", "not published", "Version DOI: minted on upload"); v2.1.1 carries its own DOI. No line of the text changed. What is new in v2.1.0 — HOW MANY VALUES, WHERE THE VALUES COME FROM, and the numeric floor kernel-checked. The logic is unchanged; its name and what is proved about it changed. First, THE NAME: versions up to 2.0.0 called ZTL "a two-valued logic with a mark, not a three-valued logic"; that denied the atom its value — an atom is an assertion, and an unverified atom has the value Z. ZTL is a three-valued logic whose every connective is two-valued: three values on the atoms, two on everything built from them (the greediness theorem is exactly that the third value never climbs above the atoms); Suszko's reduction is non-truth-functional only in connectives applied directly to atoms. No previously measured or proved fact changes. Second, THE ORDER OF BIRTH (§3.9, ZOrigin.lean, seven theorems, empty axiom list): under pure doubt — every atom unverified, no constant — F is produced first and T only through an F; classical logic, whose negation is an involution, has no such order. Third, THE NUMERIC FLOOR (§15): a name is one number across the whole claim (ZNumNames), a negative discriminant leaves no root (ZParabola), where an integer quadratic takes its extremes on a box (ZIntExtremes). Fourth, THE WARRANTY GRADE WITHOUT THE WALK (§19, ZOnly). Fifth, CORRECTIONS: a constant is not an atom; 584 validities as a set; the 2.0.0 sentence "every mark-sensitive verdict is a refusal" was false — of 1840, 742 at least once assert where the substitution refuses (¬¬p); "unless P = NP" where hardness says "cannot"; seven missing references added. The corpus now holds seventy-one modules and 1194 theorems (v2.0.0: 66 and 1112), all on the empty axiom list. What is new in v2.0.0 — THE RELATION TO CLASSICAL LOGIC, stated and measured, in the header, abstract, §1, §3.1, §4, §7 and §10. First, ON VERIFIED DATA THE TWO ARE THE SAME LOGIC: evalF_agrees for every formula, and on the depth-≤2 pool of 2926 formulas the two validate the same 588, element for element — zero classical laws lost. Second, ON UNVERIFIED DATA ZTL DECIDES: the twenty-six classical laws on a marked atom — twelve hold (modus ponens, non-contradiction, transitivity, commutativity, associativity, both distributivities, the three positive definitions), fourteen are refuted with an exhibited witness (the four that are formulas take the value F: excluded middle, p→p, Peirce, q→(p→q); the ten identities have both sides defined and different), undecided outcomes zero; classical logic decides none, having no input f