ZTL — Zero-Trust Logic

Try it without installing anything: studio.ztljudge.com — the judge, running, on your own sentence.

A logic built on one principle: truth is never granted on credit. A three-valued logic whose every connective is two-valued: the verdict of every compound is T or F, and the third value Z (zero-trust, "truth not earned"), the mark of a dirty input (not ours: its owner may change it between two reads, so each occurrence is read on its own; verification cleans it), lives only on atoms: it never produces T unless T is forced under every classical reading of the dirty atom. Default deny, ported from security into truth tables; the three-symbol tables are the working calculator of this policy (ontological passport — preprint, §10).

Highlights: machine-checked core in Lean 4 with zero axioms (no propext, no Quot.sound, no choice), including a certified tableau engine (soundness + completeness) and a native-rules engine proven equivalent; an algebraic passport — expressive completeness of the external layer, a definable implication with a two-way deduction theorem, Craig interpolation, machine-checked cut admissibility, and the Blok–Pigozzi conditions verified on the matrix (ZTL is algebraizable, yet not self-extensional); measured bridges to six independent engineering traditions — IEEE NaN, SQL NULL, taint tracking/IFC, abstract interpretation, imprecise probabilities, provenance semirings; quarantine treatment of the liar, Curry, Yablo and Russell (containment instead of explosion); verdicts carry a stability warranty (local answer + supervaluational guarantee).

Honest pedigree: functionally ZTL is a fragment of the external layer of Bochvar's B3 (1938); the {¬,∧,∨} core falls in the 8Kb* class. What is ours: the implication floor (a 7-cell delta, outside the Rosser–Turquette standardness conditions), the generating principle, and the two-register quarantine theorem.

Run (Python 3, no dependencies):

python3 ztl.py         # tables + verification of the anchor axioms
python3 audit.py       # identity audit: which laws hold on the mark, which need ground; MP; greediness
python3 entailment.py  # entailment ⊨: rules vs laws, deduction theorem
python3 tableau.py     # calculus: signed tableaux + check against ⊨ (2462 pairs)
python3 quantifiers.py # quantifiers: strict witnesses, UI/EG asymmetry
python3 tableau_fo.py  # quantifier tableaux + check against enumeration (28 pairs)
python3 paradoxes.py   # liar, carousel, avenger
python3 fixedpoint.py  # quarantine as a fixed point, two registers
python3 zalgebra.py    # algebraic passport: J-operators, DDT for E, Blok–Pigozzi
python3 zinterp.py     # Craig interpolation via expressive completeness
python3 zsequent.py    # sequent reading: cut admissibility (semantic cut elimination)
python3 zfo.py         # first order over arbitrary domains: parameter tableaux
python3 zpassport.py   # quarantine passport: paradox / underdetermined / input
python3 bridge.py      # the stitch: 141 answers, Python against the Lean kernel
python3 zquasi.py      # quasivariety recon: SI generator, clone theorem, Plonka probe
python3 zipc.py        # the delta against intuitionism: G4ip vs the keel, incomparability
python3 zopsets.py     # operational sets (VR Part II): witnessed identity as ZTL atoms
python3 zchoice.py     # choice sequences (VR Part II): the stage court = lawless supervaluation
python3 zzhegalkin.py  # Zhegalkin: the {∧,⊕} basis holds entirely, the GF(2) ring needs ground
cd lean && lake build  # machine check of the core: zero axioms

Full regression: python3 run_all.py (33 stands + Lean build).

ZTLStudio (tool/): a local studio — a human states a paradox or a claim in natural language, the AI only translates (negotiated understanding → ZFL, the Zero-trust Formal Language, with a deterministic Russian back-reading as the non-hallucinating auditor and a validator-driven repair loop), and the measured ZTL core judges: verdicts with warranties, quarantine passports, stipulation options. A public instance runs at https://studio.ztljudge.com — nothing to install. To run your own: the studio lives in its own tree (ztlstudio/ztlstudio.py), not in this repository — python3 ztlstudio.py from there → http://localhost:8190 (no dependencies; without GROQ_API_KEY it runs in pro mode — write ZFL by hand).

For AI agents (MCP). The same judge is an MCP server: https://api.ztljudge.com/mcp (Streamable HTTP, no key, no sign-up; 30 requests a minute per address, 256 KB per request). Three tools: language (the columns and rules of a ZFL table), examples (worked documents) and judge. Your agent's own AI writes the table; ZTL judges it. A compound claim (signed & delivered) is always judged T or F; a claim that is a single name answers with that name's own value, which is Z while it stays dirty or rests on something dirty. In Claude Code:

claude mcp add --transport http ztl https://api.ztljudge.com/mcp

Other MCP clients take the same URL as a remote server. Plain HTTP, for clients without MCP, lives at the same address: /language, /examples, /judge (POST), /health.

Companion papers, both built on this core: The Paradox Docket — a computable classification of the classical paradoxes (zclassify.py, E35; DOI 10.5281/zenodo.21864082), and The Gettier Case File — knowledge as an earned verdict (zgettier.py, E36; DOI 10.5281/zenodo.21877469).

The specification and all design decisions are in SPEC.md; the preprint is publications/ztl/ZTL-draft_2.1.0.md (every publication has its folder under publications/) — published on Zenodo, latest v2.1.3 (10.5281/zenodo.23648237; v2.1.2 10.5281/zenodo.23019513; v2.1.1 10.5281/zenodo.23008041; v2.1.0 10.5281/zenodo.23007861; v2.0.0 10.5281/zenodo.22842725; v1.4.1 10.5281/zenodo.22644261; v1.4 10.5281/zenodo.22643843; v1.3 10.5281/zenodo.21472971; v1.2 10.5281/zenodo.21440066); concept DOI 10.5281/zenodo.21318981 always resolves to the latest version (v1.0: 10.5281/zenodo.21318982; text CC BY 4.0, code MIT — since 2026-08-22 the code is dual-licensed Apache-2.0 OR MIT, at your option). Formalization blueprint (theorem map with dependency graph): https://inventor1975.github.io/ZTL/

The project originated on 2026-07-10 from an analysis of the liar paradox; its shipyard predecessor is VSPL (a temporal paraconsistent logic of streams).

License. The code is dual-licensed Apache-2.0 OR MIT, at your option (LICENSE, LICENSE-APACHE, LICENSE-MIT). Apache 2.0 was added on 2026-08-22 for its explicit patent grant, which is what an organisation's counsel looks for; MIT was kept rather than replaced, so that every earlier statement that this code is MIT-licensed remains true. Nothing was withdrawn from anyone. The preprints on Zenodo are documents and carry CC BY 4.0.

AI participation: designed and written in a dialogue between the curator (Vitaly Reznik) and Claude (Anthropic); all fork decisions are the curator's.

Known limits

What the instrument cannot do (ceilings) and what is unfinished (gaps) is kept in KNOWN-LIMITS.md, apart from the commit log so it cannot dissolve into it.