ZTL — Zero-Trust Logic

Six independent engineering traditions — IEEE 754 NaN, SQL NULL, tainttracking, abstract interpretation, imprecise probabilities, andprovenance semirings — have each solved a fragment of one problem: howto compute honestly over unverified data. This preprint shows that allsix implement fragments of a single logic generated by one principle: truth is never granted on credit. There are exactly two truth values (verdicts are always classical) ; the third symbol Z is a mark on anunverified input, not a truth value. For this logic (ZTL) the preprint builds: the measured price list ofclassical laws (12 survive, including modus ponens; 14 fall — all ofthem "truth from form") ; the split between rules and laws with aone-directional deduction theorem for the primitive arrow; a signedtableau calculus with machine-proven soundness, completeness and cutadmissibility; an algebraic passport — expressive completeness of theexternal layer, a definable implication with the full deductiontheorem, Craig interpolation, and the Blok–Pigozzi conditions verifiedon the matrix (ZTL is algebraizable, yet not self-extensional) ;quantifiers over finite and arbitrary domains; modal and probabilisticidentifications; a theory of verification (a verdict is a pair "value + warranty", where the warranty is a two-grade ladder: sound — never lies;hereditary — never revoked) and of evidence combination (conflict is neverrenormalized) ; and a quarantine passport typing every refusal by itsgenesis — paradox, intrinsic, underdetermined, unverified input, inherited — with a measured stipulation theorem. The classicalparadoxes (the liar, Jourdain's carousel, Curry, Yablo, the crocodile, Russell) receive a uniform diagnosis: pointwise quarantine instead ofexplosion. The entire development — fourteen Lean 4 modules — is machine-checked withan EMPTY axiom list (no classical choice, no quotients, not evenpropositional extensionality; definitions included). Every numericalclaim is reproducible by the repository's regression (40 test stands) ;an interactive studio (natural language → the ZFL formal language →the measured core) ships with the repository. 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;the contribution is the generatingprinciple, an implicational floor outside the Rosser–Turquettestandardness conditions, the calculus, the machine verification, andthe bridges to the engineering traditions. 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 corrected —the verdict warranty is a two-grade ladder (sound / hereditary). Thev1. 0 claim "stability-by-supervaluation ⟺ invariance underverifications" (90/90) was a fact about that section's 10-formulapool, not a law: it is falsified by the or (ladder, gap) cells, e. g. ¬¬p ∨ (q∨¬q), found by the identity atoms of the operational-setsexpedition (E21) on a 3303-formula pool and cross-checked with thesection's own instruments. The sound half of the warranty survives (a sound verdict never lies) ; only hereditary invariance buys shelflife. The correction was found the day of v1. 0's publication and isreleased after three further expeditions leaned on the correctedmachinery and it held. AI disclosure: this work was carried out with the substantialparticipation of the AI system Claude (Anthropic) in a dialoguesetting; all design decisions, fork choices, and final responsibilityrest with the human author. The reliability of the results does notdepend on trusting the AI: every claim is checkable by the repositorycode and the Lean 4 kernel.