A definition is a test¶

Level: 201 · for anyone who has met a definition made of axioms, such as a vector space

One line: In a school book a + b = b + a is a fact about the integers; in Axler's definition of a vector space u + v = v + u is a condition any set can be tested against, and once a set passes, every theorem proved from the conditions is true there without being proved again.

The same sentence, a different job¶

The laws of an operation showed that the school book's rules for the integers and the linear-algebra book's rules for vectors are the same four laws. They are, but the two books use them for different things.

Serge Lang's Basic Mathematics says the integers have these properties. The sentence is about one set, and it is true or false of that set.

Sheldon Axler's Linear Algebra Done Right, definition 1.20, says something else:

A vector space is a set V along with an addition on V and a scalar multiplication on V such that the following properties hold.

Then comes the list. This is not a fact about any particular set. It is an entry test, and any set that meets every condition gets the name vector space. The pay-off comes later: every theorem in the book is proved from the conditions alone, so it is true in every set that passes, including sets nobody had in mind when the theorem was proved.

A programmer knows this move. The definition is an interface: a trait in Rust, an interface in Java, a protocol in Python. Each set that passes is an implementation, and each theorem is a generic function written once against the interface. There is one difference. A compiler checks that the methods exist, but nothing checks that they obey the laws. That is why the program below has to test them.

What the program prints¶

Verified output of a_definition_is_a_test.py — regenerated by tools/run_examples.py, never hand-typed.

1. THE DEFINITION, WRITTEN ONCE AS A CHECK
   commutativity            u + v = v + u
   associativity            (u + v) + w = u + (v + w)   and   (ab)v = a(bv)
   additive identity        some 0 has v + 0 = v
   additive inverse         every v has a w with v + w = 0
   multiplicative identity  1v = v
   distributive             a(u + v) = au + av          and   (a + b)v = av + bv
   Scalars tried: -2, -1, 0, 1, 3

2. FIVE CANDIDATES, ONE TEST
   R^2                        a vector space
                              (pairs of numbers, added entry by entry)
   functions {a, b, c} -> Q   a vector space
                              ((f + g)(x) = f(x) + g(x),  (af)(x) = a f(x))
   positive numbers           a vector space
                              ('u + v' is u*v,  'av' is v**a,  the zero is 1)
   R^2 in floats              fails associativity, distributive
                              (pairs of floats, added entry by entry)
     associativity, at u = (0.1, 0.2), v = (0.2, 0.3), w = (0.3, 0.1):
       (u + v) + w = (0.6000000000000001, 0.6)
       u + (v + w) = (0.6, 0.6000000000000001)
     distributive, at a = 3, u = (0.1, 0.2), v = (0.3, 0.1):
       a(u + v) = (1.2000000000000002, 0.9000000000000001)
       au + av   = (1.2, 0.9000000000000001)
   R^2, a(x, y) = (ax, 0)     fails multiplicative identity
                              (the usual addition, a scalar product that drops y)
     multiplicative identity, at v = (1, 2):
       1v = (1, 0)

3. PROVED ONCE: 0v = 0 IN EVERY VECTOR SPACE
   Proof, from the axioms only:  0v = (0 + 0)v = 0v + 0v;  add -(0v) to both sides.
   R^2                        0(1/3, 2) = (0, 0)
                              is that the zero vector of this space?  True
   functions {a, b, c} -> Q   0{a: 1, b: -2, c: 1/2} = {a: 0, b: 0, c: 0}
                              is that the zero vector of this space?  True
   positive numbers           0(2) = 1
                              is that the zero vector of this space?  True
   In the positive numbers the zero vector is 1, so the theorem says
   2**0 = 1. Once the exponent laws hold, x**0 = 1 is forced, by the same
   proof as 0v = 0, and nobody has to prove it a second time.

4. PROVED ONCE: (-1)v = -v IN EVERY VECTOR SPACE
   Proof:  v + (-1)v = 1v + (-1)v = (1 + (-1))v = 0v = 0,  and inverses are unique.
   R^2                        (-1)(1/3, 2) = (-1/3, -2)
                              is that -v, the additive inverse?  True
   functions {a, b, c} -> Q   (-1){a: 1, b: -2, c: 1/2} = {a: -1, b: 2, c: -1/2}
                              is that -v, the additive inverse?  True
   positive numbers           (-1)(2) = 1/2
                              is that -v, the additive inverse?  True
   In the positive numbers the inverse of 2 is 1/2, because 2 'plus' 1/2
   is 2 * 1/2 = 1, the zero. So the theorem says 2**-1 = 1/2.

5. FAIL ONE AXIOM, LOSE THE THEOREMS THAT USE IT
   R^2, a(x, y) = (ax, 0):  multiplicative identity fails, 1(1, 2) = (1, 0)
     (-1)(1, 2) = (-1, 0),  but -(1, 2) = (-1, -2)
     (1, 2) + (-1, 0) = (0, 2), not (0, 0)
     The proof in section 4 began with v = 1v. Here that step is false,
     and so is the theorem.
   R^2 in floats:  associativity fails, so cancellation (u + v) - v = u is unproved
     ((0.1, 0.2) + (0.2, 0.3)) - (0.2, 0.3) = (0.10000000000000003, 0.2)
     not (0.1, 0.2)
     0v = 0 on these samples: True;  (-1)v = -v: True
     Those two survive, but not because of the proofs: multiplying a float
     by 0 or -1 happens to be exact. A failed axiom does not make every
     theorem false. It makes every theorem that used it unproved.

Five candidates¶

Section 2 runs Axler's conditions against five sets. Three pass, and two of those look nothing like arrows.

ℝ² is the one everybody expects.

Functions from {a, b, c} to ℚ pass too, with functions added and scaled point by point: (f + g)(x) = f(x) + g(x). A vector does not have to be a list of numbers. It can be anything that adds and scales by these rules. Axler makes the same move in the same section: ℝⁿ is the functions from {1, …, n} to ℝ, and a sequence is a function from {1, 2, 3, …}. So one proof, that the functions from any set S form a vector space, covers ℝⁿ, the sequences and much else at once.

The positive numbers pass with a strange addition: "u + v" means u·v, and "a times v" means vᵃ. The zero vector is 1. Every axiom turns out to be an exponent law in disguise:

Axiom	What it says here	The school law
commutativity	u·v = v·u	multiplication commutes
associativity	(u·v)·w = u·(v·w), and v^(ab) = (vᵇ)ᵃ	power of a power
additive identity	v·1 = v	1 is the multiplicative identity
additive inverse	v·(1/v) = 1	reciprocals
multiplicative identity	v¹ = v	first power
distributive	(u·v)ᵃ = uᵃ·vᵃ, and v^(a+b) = vᵃ·vᵇ	power of a product, product of powers

The program tries only whole-number scalars, because 2^(1/2) is not a fraction and the program computes exactly. The space itself is the positive real numbers with any real scalar, and the exponent laws hold there too.

ℝ² in floats fails associativity and distributivity, with the witnesses printed. These are the laws machine numbers found floats lose, for the same reason: each grouping rounds at a different step.

ℝ² with a(x, y) = (ax, 0) fails exactly one axiom, 1v = v. Every other condition holds, which you can check by hand in a line each. That makes this candidate the reason the axiom is on the list: without it, a scalar multiplication could throw the second coordinate away and still count.

Proved once: 0v = 0¶

Section 3 uses a theorem that Axler proves from the axioms alone, a few pages after the definition:

0v = (0 + 0)v = 0v + 0v.

Add the additive inverse of 0v to both sides, and what is left is 0 = 0v. Each step uses one axiom: the distributive property, then the additive inverse, associativity and the additive identity. None of it mentions pairs or functions or numbers.

So the theorem holds in every space that passed, and section 3 shows what it says in each. In ℝ² and in the functions it says what you would expect. In the positive numbers the zero vector is 1, and the theorem says 2⁰ = 1. A school book usually presents x⁰ = 1 as a convention, chosen so that the exponent laws keep working. Here it is a consequence: once the exponent laws hold, the proof of 0v = 0 forces it.

Proved once: (−1)v = −v¶

Section 4 is the next theorem:

v + (−1)v = 1v + (−1)v = (1 + (−1))v = 0v = 0.

So (−1)v is an additive inverse of v, and additive inverses are unique, so it is the additive inverse, −v. In the positive numbers the additive inverse of 2 is 1/2, because 2 "plus" 1/2 is 2 · 1/2 = 1, the zero. So the theorem says 2⁻¹ = 1/2. Negative exponents are reciprocals for the same reason x⁰ = 1: the laws force it.

Fail one axiom, lose the theorems that used it¶

Section 5 goes back to the two candidates that failed.

In ℝ² with a(x, y) = (ax, 0), the theorem of section 4 is false: (−1)(1, 2) = (−1, 0), and (1, 2) + (−1, 0) = (0, 2), which is not zero. Look at the proof. Its first step replaced v by 1v, and 1v = v is the axiom this candidate fails. The theorem breaks exactly where the proof used the missing axiom.

In floats, the cancellation law (u + v) − v = u is proved from associativity, and it fails: (0.1 + 0.2) − 0.2 comes out as 0.10000000000000003. But 0v = 0 and (−1)v = −v both still hold, because multiplying a float by 0 or by −1 happens to be exact. So a failed axiom does not make every theorem false. It makes every theorem that used it unproved. Some survive by luck, and there is no way to tell which without checking each one. That is why computing with floats is a subject of its own, and not a chapter of linear algebra.

The same move, everywhere¶

Vector spaces are one example. Every name in the laws of an operation is a definition of this kind, and every theorem proved from one is proved once:

An identity is unique, in any set with an operation. If e and e′ are both identities, then e = e · e′ = e′. That one line covers 0 for the integers under +, 1 for the integers under ×, the empty string, and the identity matrix.
A polynomial of degree n has at most n roots in any field. Roots of unity uses this to know it has found every solution of zⁿ = 1. It never proves the theorem for the complex numbers. It only needed multiplication as pairs to show that the pairs are a field.

This is the honest answer to "every book repeats itself". A book that states the laws as a definition is doing the opposite of repeating: it is setting up a test, so that each proof after it has to be written only once.

Run it yourself¶

From the root of your clone of this repository:

python3 06_Algebraic_Structures/a_definition_is_a_test/examples/a_definition_is_a_test.py

Auf Deutsch: Stichwörter¶

Eine Definition ist ein Test, den eine Menge mit Verknüpfung besteht oder nicht; die Potenzgesetze beweisen x⁰ = 1 und x⁻¹ = 1/x.

Stichwörter: Definition als Test, Axiom, Vektorraum, Potenzgesetze, Beweis aus Axiomen, Gegenbeispiel.