All 16 tables¶
An atom is T, F or Z. Z marks an input that is not yours and not verified: it may turn out T or F, and it may change between two reads. Every connective answers T or F — never Z. One rule makes every table from the classical one: the answer is T if the classical connective gives T under every reading of each Z as T or as F, and F otherwise. Each occurrence of Z is read on its own, independently of the others: that is why Z ↔ Z is F. See the rule.
Rows are the left argument a, columns the right argument b. The tables are written by a script from ztl.py (commit 46c27e0 of inventor1975/ZTL): no cell is typed by hand, and the script checks each cell against a reference file computed from the same code on 2026-09-28 — a check that nothing has drifted since, not an independent proof. The kernel is the classical table on (TT, TF, FT, FF).
One argument¶
All four classical one-argument tables, lifted.
id x — identity (assertion)¶
| x | id x |
|---|---|
| T | T |
| F | F |
| Z | F |
¬x — NOT (negation)¶
| x | ¬x |
|---|---|
| T | F |
| F | T |
| Z | F |
⊤x — always T¶
| x | ⊤x |
|---|---|
| T | T |
| F | T |
| Z | T |
⊥x — always F¶
| x | ⊥x |
|---|---|
| T | F |
| F | F |
| Z | F |
Two arguments¶
All sixteen classical two-argument tables, each lifted by the rule. In the first ten the classical answer depends on both arguments; in the last six it depends on one argument or on none, and a Z in an argument that does not matter changes nothing.
1. a ∧ b — AND (conjunction)¶
Kernel TFFF.
| ∧ | T | F | Z |
|---|---|---|---|
| T | T | F | F |
| F | F | F | F |
| Z | F | F | F |
2. a ∨ b — OR (disjunction)¶
Kernel TTTF.
| ∨ | T | F | Z |
|---|---|---|---|
| T | T | T | T |
| F | T | F | F |
| Z | T | F | F |
3. a → b — IF a THEN b (implication)¶
Kernel TFTT.
| → | T | F | Z |
|---|---|---|---|
| T | T | F | F |
| F | T | T | T |
| Z | T | F | F |
4. a ← b — IF b THEN a (converse implication)¶
Kernel TTFT.
| ← | T | F | Z |
|---|---|---|---|
| T | T | T | T |
| F | F | T | F |
| Z | F | T | F |
5. a ⊕ b — EITHER-OR (exclusive or)¶
Kernel FTTF.
| ⊕ | T | F | Z |
|---|---|---|---|
| T | F | T | F |
| F | T | F | F |
| Z | F | F | F |
6. a ↔ b — SAME (equivalence)¶
Kernel TFFT.
| ↔ | T | F | Z |
|---|---|---|---|
| T | T | F | F |
| F | F | T | F |
| Z | F | F | F |
7. a ↑ b — NOT-AND (NAND, Sheffer stroke)¶
Kernel FTTT.
| ↑ | T | F | Z |
|---|---|---|---|
| T | F | T | F |
| F | T | T | T |
| Z | F | T | F |
8. a ↓ b — NOT-OR (NOR, Peirce arrow)¶
Kernel FFFT.
| ↓ | T | F | Z |
|---|---|---|---|
| T | F | F | F |
| F | F | T | F |
| Z | F | F | F |
9. a ↛ b — a AND NOT b (non-implication)¶
Kernel FTFF.
| ↛ | T | F | Z |
|---|---|---|---|
| T | F | T | F |
| F | F | F | F |
| Z | F | F | F |
10. a ↚ b — NOT a AND b (converse non-implication)¶
Kernel FFTF.
| ↚ | T | F | Z |
|---|---|---|---|
| T | F | F | F |
| F | T | F | F |
| Z | F | F | F |
11. π₁(a, b) — copy a (projection on a)¶
Kernel TTFF.
| π₁ | T | F | Z |
|---|---|---|---|
| T | T | T | T |
| F | F | F | F |
| Z | F | F | F |
12. π₂(a, b) — copy b (projection on b)¶
Kernel TFTF.
| π₂ | T | F | Z |
|---|---|---|---|
| T | T | F | F |
| F | T | F | F |
| Z | T | F | F |
13. π̄₁(a, b) — the opposite of a, b ignored (one connective, not ¬ on top of π₁)¶
Kernel FFTT.
| π̄₁ | T | F | Z |
|---|---|---|---|
| T | F | F | F |
| F | T | T | T |
| Z | F | F | F |
14. π̄₂(a, b) — the opposite of b, a ignored (one connective, not ¬ on top of π₂)¶
Kernel FTFT.
| π̄₂ | T | F | Z |
|---|---|---|---|
| T | F | T | F |
| F | F | T | F |
| Z | F | T | F |
15. ⊤(a, b) — always T¶
Kernel TTTT.
| ⊤ | T | F | Z |
|---|---|---|---|
| T | T | T | T |
| F | T | T | T |
| Z | T | T | T |
16. ⊥(a, b) — always F¶
Kernel FFFF.
| ⊥ | T | F | Z |
|---|---|---|---|
| T | F | F | F |
| F | F | F | F |
| Z | F | F | F |
A negation on top is not the single connective¶
¬(a ∧ b) built from two connectives is not the same table as the single connective a ↑ b, though classically they agree. The inner connective answers first, and its answer is a fixed T or F for the outer one; each connective reads its own Z. This holds for every connective: the table below compares ¬ on top of each of the sixteen with the single connective whose classical table is the negated one.
| ¬ on top of | single connective | cells that differ |
|---|---|---|
¬(a ∧ b) |
a ↑ b |
(T, Z), (Z, T), (Z, Z) |
¬(a ∨ b) |
a ↓ b |
(F, Z), (Z, F), (Z, Z) |
¬(a → b) |
a ↛ b |
(T, Z), (Z, F), (Z, Z) |
¬(a ← b) |
a ↚ b |
(F, Z), (Z, T), (Z, Z) |
¬(a ⊕ b) |
a ↔ b |
(T, Z), (F, Z), (Z, T), (Z, F), (Z, Z) |
¬(a ↔ b) |
a ⊕ b |
(T, Z), (F, Z), (Z, T), (Z, F), (Z, Z) |
¬(a ↑ b) |
a ∧ b |
(T, Z), (Z, T), (Z, Z) |
¬(a ↓ b) |
a ∨ b |
(F, Z), (Z, F), (Z, Z) |
¬(a ↛ b) |
a → b |
(T, Z), (Z, F), (Z, Z) |
¬(a ↚ b) |
a ← b |
(F, Z), (Z, T), (Z, Z) |
¬(π₁(a, b)) |
π̄₁(a, b) |
(Z, T), (Z, F), (Z, Z) |
¬(π₂(a, b)) |
π̄₂(a, b) |
(T, Z), (F, Z), (Z, Z) |
¬(π̄₁(a, b)) |
π₁(a, b) |
(Z, T), (Z, F), (Z, Z) |
¬(π̄₂(a, b)) |
π₂(a, b) |
(T, Z), (F, Z), (Z, Z) |
¬(⊤(a, b)) |
⊥(a, b) |
none |
¬(⊥(a, b)) |
⊤(a, b) |
none |
Where they differ, the composite says T and the single connective F: the inner connective has already answered F, and the outer ¬ turns that into T. Four of them in full:
¬(a ∧ b) against a ↑ b¶
| ¬(…) | T | F | Z |
|---|---|---|---|
| T | F | T | T |
| F | T | T | T |
| Z | T | T | T |
Differs from a ↑ b in 3 cell(s): (T, Z), (Z, T), (Z, Z).
¬(a ∨ b) against a ↓ b¶
| ¬(…) | T | F | Z |
|---|---|---|---|
| T | F | F | F |
| F | F | T | T |
| Z | F | T | T |
Differs from a ↓ b in 3 cell(s): (F, Z), (Z, F), (Z, Z).
¬(a ⊕ b) against a ↔ b¶
| ¬(…) | T | F | Z |
|---|---|---|---|
| T | T | F | T |
| F | F | T | T |
| Z | T | T | T |
Differs from a ↔ b in 5 cell(s): (T, Z), (F, Z), (Z, T), (Z, F), (Z, Z).
¬(a → b) against a ↛ b¶
| ¬(…) | T | F | Z |
|---|---|---|---|
| T | F | T | T |
| F | F | F | F |
| Z | F | T | T |
Differs from a ↛ b in 3 cell(s): (T, Z), (Z, F), (Z, Z).
Recompute¶
From a clone of the ZTL repository:
from ztl import lift2, T, F
nand = lift2(lambda a, b: F if (a, b) == (T, T) else T)
nand('T', 'Z') # 'F'