The 26 laws¶
Twenty-six laws of classical logic: twenty equalities (two formulas always have the same value) and six validities (a formula is always T).
The list is the one fixed in the ZTL repository (audit.py, and the same 26 in lean/ZTL.lean). It is a selection of common laws, not all of them: the dual absorption p ∨ (p ∧ q) = p, for example, is not on it. Any other law can be checked the same way.
On verified inputs all 26 hold. A verified input is one where every atom is T or F (the Lean names call it ground). There ZTL computes exactly what classical logic computes (Lean: evalF_agrees, lean/ClassicalAgreement.lean), so every classical law holds — these 26 included.
When an atom may be Z, 12 of them still hold and 14 do not. For each of the 14 there is an assignment where it breaks; the table shows one. The connectives are in All 16 tables.
How to read an equality with Z: both sides are evaluated with the same assignment of T, F or Z to every atom. A compound is never Z, so an equality with a bare atom on one side breaks at that atom = Z for this reason alone: the compound side is T or F, the atom side stays Z. 6 of the 14 break only for this reason: double negation, idempotence of ∧, idempotence of ∨, absorption, unit of ∧, unit of ∨. The other 8 break with both sides two-valued.
Computed by audit.py (commit 54c773c) over every assignment of T, F, Z to the atoms. For each of the 12, a Lean theorem states the law; for each of the 14, a Lean theorem states that it fails on some input (lean/ZTL.lean, commit 9eda661). The repository's CI checks that every theorem uses no axioms.
12 laws that hold with Z¶
| law | formula | Lean |
|---|---|---|
| implication via ∨ | p→q = ¬p∨q |
imp_def |
| ⊕ in distributive form | p⊕q = (p∧¬q)∨(¬p∧q) |
xor_def |
| ↔ in distributive form | p↔q = (p∧q)∨(¬p∧¬q) |
xnor_def |
| ↔ via two implications | p↔q = (p→q)∧(q→p) |
xnor_imps |
| commutativity of ∧ | p∧q = q∧p |
and_comm' |
| commutativity of ∨ | p∨q = q∨p |
or_comm' |
| associativity of ∧ | (p∧q)∧r = p∧(q∧r) |
and_assoc' |
| associativity of ∨ | (p∨q)∨r = p∨(q∨r) |
or_assoc' |
| distributivity ∧/∨ | p∧(q∨r) = (p∧q)∨(p∧r) |
and_distrib |
| distributivity ∨/∧ | p∨(q∧r) = (p∨q)∧(p∨r) |
or_distrib |
| non-contradiction | ¬(p∧¬p) always T |
no_contradiction |
| transitivity of → | ((p→q)∧(q→r))→(p→r) always T |
imp_trans_law |
14 laws that break with Z¶
Each holds on verified inputs. The table shows one assignment where it breaks; there may be more.
| law | formula | breaks at | Lean |
|---|---|---|---|
| double negation | ¬¬p = p |
p = Z: left T, right Z | double_neg_needs_ground |
| De Morgan 1 | ¬(p∧q) = ¬p∨¬q |
p = T, q = Z: left T, right F | deMorgan1_needs_ground |
| De Morgan 2 | ¬(p∨q) = ¬p∧¬q |
p = F, q = Z: left T, right F | deMorgan2_needs_ground |
| contraposition | p→q = ¬q→¬p |
p = T, q = Z: left F, right T | contraposition_needs_ground |
| ⊕ as negation of ↔ | p⊕q = ¬(p↔q) |
p = T, q = Z: left F, right T | xor_as_not_xnor_needs_ground |
| idempotence of ∧ | p∧p = p |
p = Z: left F, right Z | and_idem_needs_ground |
| idempotence of ∨ | p∨p = p |
p = Z: left F, right Z | or_idem_needs_ground |
| absorption | p∧(p∨q) = p |
p = Z, q = T: left F, right Z | absorption_needs_ground |
| unit of ∧ | p∧T = p |
p = Z: left F, right Z | and_true_needs_ground |
| unit of ∨ | p∨F = p |
p = Z: left F, right Z | or_false_needs_ground |
| excluded middle | p∨¬p always T |
p = Z: F | lem_needs_ground |
| reflexivity of → | p→p always T |
p = Z: F | imp_refl_needs_ground |
| Peirce's law | ((p→q)→p)→p always T |
p = Z, q = F: F | peirce_needs_ground |
| weakening (axiom K) | q→(p→q) always T |
p = T, q = Z: F | k_axiom_needs_ground |
Rules of inference¶
A rule premises ⊢ conclusion holds if, whenever every premise is T, the conclusion is T. Each letter stands for any value T, F or Z — a compound is T or F, so a rule that holds on values holds on formulas too. Every rule is a Lean theorem and is also checked here by brute force over all values.
| rule | statement | with Z | Lean |
|---|---|---|---|
| modus ponens | p, p → q ⊢ q |
holds | modus_ponens |
| modus tollens | p → q, ¬q ⊢ ¬p |
holds | rule_modus_tollens |
| contraposition (rule) | p → q ⊢ ¬q → ¬p |
holds | rule_contraposition |
| disjunctive syllogism | p ∨ q, ¬p ⊢ q |
holds | rule_disj_syllogism |
| ∧ introduction | p, q ⊢ p ∧ q |
holds | rule_and_intro |
| ∧ elimination | p ∧ q ⊢ p |
holds | rule_and_elim |
| ∨ introduction | p ⊢ p ∨ q |
holds | rule_or_intro |
| ¬¬ introduction | p ⊢ ¬¬p |
holds | rule_dn_intro |
| transitivity (rule) | p → q, q → r ⊢ p → r |
holds | rule_transitivity |
| K (rule) | q ⊢ p → q |
holds | rule_K |
| explosion | p, ¬p ⊢ q |
holds | rule_explosion |
| resolution | p ∨ q, ¬p ∨ r ⊢ q ∨ r |
holds | rule_resolution |
| ¬¬ elimination | ¬¬p ⊢ p |
breaks | rule_dn_elim_needs_ground |
| a law in the conclusion | p ⊢ q ∨ ¬q |
breaks | rule_taut_concl_needs_ground |
Contraposition breaks as a law (an equality of two formulas) but holds as a rule: from a T-valued p → q you may always conclude ¬q → ¬p. In classical logic the deduction theorem makes the two the same; in ZTL it works one way only (Z → Z is F, while concluding p from p is trivial).
Recompute¶
python3 audit.py
cd lean && lake build