ZTL — Zero-Trust Logic

ZTL (Zero-Trust Logic) is a two-valued logic over marked inputs, generated by one principle: truth is never granted on credit — aconnective returns T only if T is forced under every classical readingof the unverified. There are exactly two truth values (verdicts arealways classical) ; the third symbol Z is a mark on an unverified input, not a truth value. The mark is barred from the value of any compound (the greediness theorem, machine-checked): above the atoms the algebraicvalue already is the logical value, so — beyond Suszko's logicaltwo-valuedness, which every structural logic has — ZTL is bivalent oncompounds by construction. Its identity among the three-valued matricesis precise and machine-checked at its cause: a single rule, ¬¬p ⊨ p, separates its consequence relation from each of its fourinvolutive-negation neighbours (K3, LP, weak Kleene, Łukasiewicz Ł₃), and by one lemma from any three-valued matrix with involutive negation. That the logic is not arbitrary is evidenced case by case: sixindependent engineering traditions — IEEE 754 NaN, SQL NULL, tainttracking, abstract interpretation, imprecise probabilities, andprovenance semirings — have each reinvented a fragment of the samediscipline, and for each the core reproduces its central move on aworked case (we argue, and do not claim to have proved, that eachimplements a fragment of one logic). For this logic the preprint builds: the measured price list of classicallaws (12 survive, including modus ponens; 14 fall — all "truth fromform") ; the split between rules and laws with a one-directional deductiontheorem for the primitive arrow; a signed tableau calculus withmachine-proven soundness, completeness and cut admissibility; analgebraic passport — expressive completeness of the external layer, adefinable implication with the full deduction theorem, Craiginterpolation, and the Blok–Pigozzi conditions verified on the matrix (ZTL is algebraizable, yet not self-extensional) ; quantifiers over finiteand arbitrary domains; first-order identity (a = predicate whosereflexivity is an earned verdict — self-identity falls to Z on anunverified reference — while Leibniz's law licenses substitution onlythrough an earned equality) and free logic with definite and indefinitedescriptions (a non-denoting term takes the mark, not F and not a gap;existence is earned self-identity; excluded middle on a non-denoting atomis F — the greedy collapse setting ZTL apart from the neutral free-logicschool; Hilbert's ε earns denotation exactly when a witness exists) ;modal and probabilistic identifications, including the necessity ofidentity for earned equalities and rigid designation as the modal face ofexistence; a theory of verification (a verdict is a pair "value +warranty": sound — never lies; hereditary — never revoked) and ofevidence combination (conflict is never renormalized) ; and a quarantinepassport typing every refusal by its genesis — paradox, intrinsic, underdetermined, unverified input, inherited — with a measured stipulationtheorem. The classical paradoxes (the liar, Jourdain's carousel, Curry, Yablo, the crocodile, Russell) receive a uniform diagnosis: pointwisequarantine instead of explosion. The entire development — twenty-one Lean 4 modules — is machine-checkedwith an EMPTY axiom list (no classical choice, no quotients, not evenpropositional extensionality; definitions included): 371 theorems, eachaudited individually. Every numerical claim is reproducible by therepository's regression (62 test stands) ; an interactive studio (naturallanguage → the ZFL formal language → the measured core) ships with therepository. Functionally the not, and, or fragment coincides, cell by cell, withthe external layer of Bochvar's logic (1938) — a kinship found in theliterature search after the tables had been generated, not a source; thecontribution is the generating principle, an implicational floor outsidethe Rosser–Turquette standardness conditions, the calculus, the machineverification, and the bridges to the engineering traditions. What is new in v1. 3 — the preprint is reframed to lead with the logicand its precise identity, presenting the six engineering traditions asevidence that it is not arbitrary rather than as the opening motivation. Two positioning results settle the "is it really its own bivalent logic"question. First, the SUSZKO POSITIONING (§4): Z is a mark, not a thirdtruth value; every structural logic is logically two-valued (Suszko'sthesis), and ZTL's stronger, truth-functional fact is that the mark neverreaches the value of a compound at all (the greediness theorem, evalFclassical, empty axiom list) — the reduction has nothing left to doabove the atoms. Second, the SIGNATURE (§4): a single rule, ¬¬p ⊨ p, separates ZTL's consequence relation from each of its fourinvolutive-negation neighbours — and, by one lemma (involutiongivesdne, empty axiom list), from any three-valued matrix with involutive negation;the cause is a broken involution, ¬¬Z = T. The scope is kept honest: thenon-involutive kin, external Bochvar, shares the broken involution, so thetwo part in the implication fragment, not on this rule. Also new in v1. 3, extending the first-order layer, all machine-checked onthe empty axiom list: FIRST-ORDER IDENTITY (§24, ZEq. lean) — a = predicatewhose reflexivity falls to Z on an unverified reference (self-identity isearned), whose symmetry splits into a surviving rule and a failingbiconditional law, and whose Leibniz substitution is salva veritate butnever through the mark; FREE LOGIC WITH DESCRIPTIONS (§25, ZDesc. lean, ZEps. lean) — a non-denoting term takes the mark; existence is earnedself-identity ("no entity without identity", made literal) ; excludedmiddle on a non-denoting atom is F, not the supervaluational super-true;the definite description ι denotes by earned uniqueness and Hilbert'sindefinite ε by an earned witness (ε denotes exactly when the existentialis earned), the empty choice earning only the mark; and MODAL IDENTITY —the necessity of identity (Kripke) holds for every earned equality, rigiddesignation is the modal face of existence, and once more ZTL parts fromsupervaluation. The corpus grows to 371 theorems across twenty-one Leanmodules, all on the empty axiom list; regression now 62 stands + Lean. What is new in v1. 2 — first, the TEMPORAL LAYER. ZTL's only clock is thearrival of ground: one tick = one verification. The warranty ladder isread as a system of temporal quantifiers — until-verification = truenow, sound = true at every ending, hereditary = true always along everypath — with the absorption and arrow theorems machine-checkedstructurally (ZTime. lean, empty axiom list; every completedverification path ends hereditary). An expiry event returns earnedground to the mark and splits time into epochs — the knowledgechronology (learning about the same world) versus the validitychronology (the world changing) — and the EPOCH BOUNDARY THEOREM (EpochBoundary. lean, empty axiom list, structural for every formula ofthe language) states: a verdict invariant across unrestricted epochcrossing is constant — it reads none of its grounds; non-trivialguarantees require the boundary, which is thereby a logical necessity, not an administrative convenience. The layer is priced for use: earlysettlement (once hereditary, remaining checks buy nothing), expiry-insurance (a shortcut's savings are a loan against itsexpirable ground), the ungrounded verification event (the closed-worldloan "no proof of revocation, hence not revoked" cannot enter thelogic — an argument from absence never yields T — and is exposed inthe event ledger). And a price list of DERIVATIONS: forward chainingover the 12 alive rules shows they are transport, not creation — fromthe empty premise set nothing is derivable even with the fallen rulesas loans, ZTL's own guarded tautologies included; the classicalstep invisible from inside (double-negation elimination) becomes apriced borrowing with a named creditor. New sections 21-23; theZFL language gains a verification timeline played into chronicles;regression now 40 stands + Lean. Also new in v1. 2: the central construction is named — thezero-trust lift (§2), with its disambiguation from the strict (Kleene) lift; §3. 8, an explicit Lean-verified census of the sixteen lifted binaryconnectives that re-derives Finn's completeness landscape for theexternal-Bochvar class (Studia Logica 1974): solo-completeness tracksnon-commutative directionality — Sheffer's stroke and Peirce's arrowfall (both stall in one shared 18-table cage), both implications andboth abjunctions survive — with the kernel clone equalitiesmachine-checked on the empty axiom list (lean/ZClone. lean), thesurviving basis read as the credit detector; thefence-depth theorem (§19): the hereditary warranty is checkable atdepth exactly m−1 and no constant-depth fence exists (the guardfamily over the fallen law of identity) ; the warranty ladderstress-tested at scale (151. 8M pairs, 0 violations) ; the three-lawscapstone (§3. 1): of the classical triad only non-contradictionsurvives the lift — a denial is free, an affirmation is on credit;§11 opened by the paradox engine: paradox (f) = ground (S = f (S) ), theexpeditions as the range of one construction, with the verifiedcontainment (ZTL-settled nets are a strict subset of the classicallycategorical ones; stand pengine. py) ; the honestBochvar ledger (§4): the ¬, ∧, ∨ coincidence found post hoc, not asource, now joined by the Łukasiewicz pedigree — the tables areBochvar's, the MEANING of the mark Z descends from Ł₃'s "possible /not yet determined" (ref 36), and the genetic order of the alphabetreads N, Z, F, T: nothing → doubt → free denial → earned affirmation;and the passport's phase letter glossed (§10): read N asNot-yet — Kleene's undefined by intent housed as a phase — with errorstyped as interface events (the premature read of a phase; signalingNaN is the cousin), not as a logical letter. What was new in v1. 1 (same-day self-correction): §19 is correc