An axiom of a theory \(T\) is a well-formed sentence in the language of the theory that we assume to be true without a formal justification.

Models

Models of a certain theory are going to be those mathematical objects in which the axioms hold, so they can be used to pin down the mathematical structures we want to talk about.

Normally, when we want to reason about a particular aspect of the world we have to try to figure out a sufficiently descriptive set of axioms which are satisfied by the thing we want to reason about. Then we can use deduction rules to deduce consequences of those axioms, which will also be satisfied by the thing in question.

For example, we may want to model how viral videos spread across the internet. Then we can make some assumptions about this situation. For example, we may consider that the internet is a graph in which each node is a person, and its edges are friendships. We may further assume that the edges have a weight between 0 and 1 representing the probability that in a time step a person will tell its friend about the video. Then we can use this model to figure out how kitten videos end up on your twitter feed.

This is a particularly complex model with many assumptions behind. Formalizing all those assumptions and turning them into axioms would be a pain in the ass, but they are still there, albeit hidden.

For example, there might be an axiom in the language of first order logic stating that \(\forall w. weight(w)\rightarrow 0; that is, every weight in the graph is between \(0\) and \(1\).

In the ideal case, we want to write down enough axioms so that the only model satisfying them is the one we want to study. However, when dealing with first order logic there will be many occasions in which this is simply not possible, no matter how many axioms we add to our theory.

One result showing this is the Skolem-Löwenheim theorem.

Axiom schematas

For proper deduction to work as intended, the set of axioms of a theory do not have to be strictly finite, but just computablenoteIncidentally, a theory whose set of axioms is computable is called axiomatizable.

In particular, we can specify an infinite amount of axioms in one go by specifying an axiom schemata, or particular form of a sentence which will be an axioms.

For example, in Peano Arithmetic you specify the induction axiom schemata, stating that every sentence of the form \([P(0) \wedge \forall n. P(n)\rightarrow P(n+1)]\rightarrow \forall n. P(n)\) is an axiom of \(PA\).

The reason why first order logic can handle infinite sets of axioms is due to its compactness, which guarantees that every consequence of the theory is a consequence of a finite subset of the theory.