I used to think of axioms within an axiomatic systems as the basis vectors. In this view, every theorem is analogous to a linear combination of the basis vectors, and the proof is analogous to the coefficient matrix. The collection of all theorems is thus analogous to the span of the basis.
Later I realized there are at least two problems with this analogy:
- There could be several distinct proofs for a theorem.
- The Gödel's incompleteness theorem.
Is there anyway to reconcile these problems and make a meaningful analogy, or it's better to forget all about it as it's a misleading analogy?
I don't know of any, and there's a more damning problem with the axioms as basis vectors: there is no reasonable meaning that can be attached to scaling and addition, because:
What one may claim is that what we have is some kind of a partial monoid generated by our axioms, where there is an identity element (applying no axiom), and two sequences of axioms can be joined together if they can be legally applied in sequence. The application of these "proof chunks" is associative.
So we consider a set $S$ where $S$ contains all legal strings of axiom applications, and the monoid operator is concatentation of legal axiom applications.