ZTL Blueprint

6 The algebraic passport

Definition 22 J-operators
✓
#

Uses

Lean declarations

\(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.

Theorem 23 Expressive completeness, unary
✓
#

Uses

Lean declarations

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).

Theorem 24 Full deduction theorem for E
✓
#

Uses

Lean declarations

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.

Theorem 25 Blok–Pigozzi witnesses
✓
#

Uses

Lean declarations

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).

Theorem 26 Not self-extensional
✓
#

Uses

Lean declarations

\(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.

Theorem 27 Structurality
✓
#

Uses

Lean declarations

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.

Theorem 28 Craig interpolation
#

Uses

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.