Dependencies

Fuel-indexed structural tableau engine over the generating basis \(\{ \neg ,\wedge ,\vee \} \); heavy connectives reduce by the living identities.

Elements are verified values or marks; the equality atom yields \(Z\) whenever a mark is involved — even a mark with itself.

\(J_T(p) = p\wedge p\) (fallen idempotence is the truth detector), \(J_F(p) = \neg p\wedge \neg p\), \(J_Z = \mathrm{isZ}\): three exact, disjoint value indicators grown from ZTL’s own connectives.

For a classical connective \(f\), its ZTL lift returns \(T\) iff \(f\) is forced to \(T\) under every classical reading of \(Z\); otherwise \(F\). Truth is never granted on credit.

All six connectives are lifts of their classical cores; no table is postulated.

Strict signs \(T,F\) and weak signs \(P=\{ T,Z\} \), \(N=\{ F,Z\} \); weak signs occur only in refutation polarity.

Truth values are \(T\) and \(F\); the third symbol \(Z\) is a mark for an unverified input, not a truth value.

The engine with native signed rules for \(\to ,\oplus ,\leftrightarrow \) is certified by the same induction and returns identical verdicts.

The design anchor cells hold: \(\neg Z=F\), \(\neg \neg Z=T\), \(Z\leftrightarrow Z=F\), \(Z\oplus T=F\), etc.

The same-value detector \(\Delta \) and the truth equation \(p\wedge p \approx \neg (p\wedge \neg p)\) satisfy conditions (i)–(iv) of the Blok–Pigozzi characterization on the matrix: ZTL is algebraizable (kinship: Bochvar algebras, Bonzio–Pra Baldi 2024).

The two-sentence cycle has no eager model over all nine value pairs; the revenge sentence’s content evaluates to \(T\) while the sentence stays quarantined — the price is paid explicitly.

On mark-free lists a verified element certifies its membership and \(S \subseteq S\), \(S = S\) hold — the inheritance boundary is drawn at the mark, kernel-checked from both sides.

The tableau closes iff the signed nodes are unsatisfiable — for all formulas, by induction on weighted size. Zero axioms.

The tableau engine read bottom-up is a cut-free sequent calculus; cut on the covering pair \(\{ T\} ,\{ F,Z\} \) is admissible (semantic cut elimination on top of the engine certificate), weakening admissible, identity derivable.

The definable external implication \(E(p,q)=\neg (p\wedge p)\vee (q\wedge q)\) satisfies \(\Gamma ,\varphi \vDash \psi \iff \Gamma \vDash E(\varphi ,\psi )\) in both directions, over the whole language; the primitive arrow stays one-way.

Liar oscillates with period 2, the carousel with period 4; Curry is homeless without using negation; the finite Yablo truncation has a unique grounded model.

Streams never earn identity while apartness is earned by a finite witness and persists; the diagonal earns strict non-membership; one marked pair collapses the injectivity certificate; a nondegenerate mark does not equal itself; atom verdicts are the modal thresholds.

Excluded middle, De Morgan, contraposition-as-identity and \(p\to p\) fail — all only on \(Z\), all are “truth from form”.

The \(\gamma /\delta \) parameter rules carry the sign discipline to arbitrary domains (fresh witnesses exactly where the weak signs live); soundness measured (\(13/13\) verdicts cross-checked, open branches yield verified countermodels), completeness by Hintikka saturation (argued); undecidability via the J-guard embedding of classical FO. Lean port on the roadmap.

Every compound formula is classical under every valuation: \(Z\) lives only on atoms.

If \(A \vDash B\), the J-DNF of \(A\)’s projection onto the shared atoms interpolates: an external function of the shared atoms is always a formula. Measured totally (\(400/400\) and \(32/32\)); Lean port on the roadmap.

The lazy register is monotone and homes the liar (\(\neg Z=Z\)); the eager register is not monotone: grounding and verdicts require two different registers.

For every finite system: lazy evaluation is monotone over the whole language, the jump is monotone, the iteration from \(\bot \) stabilizes within \(n{+}1\) steps at the least fixed point, and the grounded part is identical in every fixed point — quarantine is well-defined. Zero axioms (information-measure pigeonhole, no WF machinery).

Negation has no fixed point: no value seats the liar; quarantine is irremovable.

A marked set is not provably a subset of itself; reflexivity of set equality fails — inherited from the tables, not postulated.

\(\mathrm{mem}(z, S)=F\) for every mark \(z\) and every list \(S\): membership is an existential fold with strict witnesses.

From \(p=T\) and \(p\to q=T\) follows \(q=T\): earned truth is transported.

\(v(p)=v(\neg p)=T\) is unsatisfiable: ZTL is paracomplete, not paraconsistent.

Per-component diagnosis of ungroundedness: PARADOX (no classical models — refusal permanent), UNDERDETERMINED (models exist — liftable by stipulation), INPUT, DOWNSTREAM with culprits; the stipulation theorem measured totally; parity re-derived \(62/62\). The even two-cycle’s two classical models are kernel-checked.

Finite-domain quantifiers are strict folds in the certified language (a singleton domain collapses both to the \(J_T\) guard); the \(n\)-ary signed rules are preimage-coverage theorems; UI/EG hold in membership form; eight battery verdicts are kernel evaluations of the certified engine.

With the constants \(\top /\bot \) in the certified language, the lazy lfp of the nine-fact membership system computes to \([F,F,T,F,T,F,F,F,Z]\): eight facts grounded, quarantine exactly at \(R\in R\) — containment instead of explosion, by the kernel.

\(p \dashv \vDash p\wedge p\), yet \(\neg (p\wedge p) \nvDash \neg p\): interderivability is not a congruence — the same failure that builds the detectors.

Contraposition survives as an inference rule while failing as an identity; double-negation elimination fails even as a rule. The deduction theorem holds only left-to-right.

The substitution lemma: \(\Gamma \vDash \varphi \) implies \(\sigma \Gamma \vDash \sigma \varphi \); together with reflexivity, monotonicity and cut, \(\vDash \) is a structural Tarskian consequence relation.

\(\Gamma \vdash \varphi \) by the engine iff every valuation making all premises \(T\) makes \(\varphi \) \(T\).

Every unary external function \(V\to \{ T,F\} \) is a J-DNF: one theorem over all eight target tables (binary case \(512/512\) measured in Python).