Should axioms be seen as "building blocks of definitions"?

Question

This question is about the difference between a definition and an axiom.

However, it does not address the following point:

Whenever we define something, this is often written as a series of axioms. e.g.

Definition. A sigma algebra $\sigma$ over $X$ is a subset of $\mathcal P(X)$, s.t.

Axiom 1.

Axiom 2.

Axiom 3.

Moreover, I don't think we ever apply axioms without then defining a term as that which satisfies those axioms, unless my memory fails me.

But since objects, such as sigma algebra's, most often are characterized by multiple axioms, it makes sense to see those axioms as different things in and of themselves, so that we can talk about "the commutativity axiom" as a separate thing, and apply them to multiple definitions.

So does it make sense to think of axioms as building blocks of definitions?

Or are we losing something if we look at axioms and definitions like this?

Answer 1

I don't really understand the question, in that I don't really understand what it would mean for the answer to the question to be "no," but it is common to think of certain axioms like commutativity and associativity as things which can be added or subtracted from other definitions, e.g. imposing commutativity on rings to get commutative rings, or removing the existence of additive inverses on rings to get semirings. Does that answer to your question?

Answer 2

To use programming terminology, some "definitions" define interfaces and some define objects. The definition of $\sigma$-algebra that you've alluded to is a definition of an interface. For you to give me a $\sigma$-algebra means you are going to give me a set $X$, and collection of subsets of $X$, $\Sigma$, and a proof for each of the axioms.

On the other hand, I can define a specific $\sigma$-algebra. For example, the discrete $\sigma$-algebra on a set $X$ consists of the set $X$ and $\Sigma=\mathcal{P}(X)$. The proofs of the axioms are trivial. This is like defining an object implementing an interface. This is not an axiom or a theorem, though it involves theorems. This is often referred to as a "construction". (In a propositions-as-types context, "theorems" and "constructions" get identified, as a theorem is just a certain type of construction in that context.)

To directly answer your question, while axioms may be parts of definitions corresponding to "interfaces", those aren't the only definitions around and even in that case there are things other than axioms involved. For example, even in your definition of $\sigma$-algebra, you have the first line which is not an axiom. So I would say axioms can be called "building blocks" of "interface" definitions, they are not the sole "building blocks" of such. (If you really wanted to, in a set-theoretic context, I guess you could state that an "interface" definition is a collection of formulas with one free variable that will be taken as axioms. Your $\sigma$-algebra example would then have an additional axiom that $\exists X,\Sigma.Z=(X,\Sigma)\land \Sigma\subseteq\mathcal{P}(X)$ where $Z$ is the free variable. The other axioms would need to be modified to project out $X$ and $\Sigma$ from $Z$.)

If we look at mechanized proof assistants (many of which are based on the proposition-as-types principle), definitions in them usually involve a collection of parameters, a collection of new names each of which may or may not have a concrete definition (i.e. a [parameterized] construction) and which may require theorems to be proven of their own to be well-defined, and a collection of axioms involving the parameters and the newly introduced names. In proof assistants like Agda and Coq, defined notions induce definitional equalities that cannot be postulated as axioms and have a significant bearing what is or isn't provable.

Answer 3

The usual order of things is somewhat different from what you outline in your question. When one wishes to formalize a subfield of mathematics one (1) starts with a bunch of primitive notions that are left undefined, (2) proceeds to postulate certain axioms formalizing how they are interrelated, (3) gives definitions of further "compound" notions, (4) formulates theorems in the language thus developed, etc.

For example, in the field of geometry, one could use point and line as undefined primitive notions, then formulate axioms of, say, affine geometry (a unique line through a pair of distinct points, etc.), then define a further compound notion of a pencil of lines, etc.