finite mathematics

Finite mathematics

Finite mathematics


Finite mathematics is the mathematics of finite sets. The term is sometimes used more broadly of discrete mathematics.

We may say that finite mathematics is mathematics done internal to the category FinSet of finite sets or the mathematics of FinSet\Fin\Set itself. The latter (but not the former) includes the basic arithmetic of natural numbers, since these are the cardinalities of finite sets; we can go as far as rational numbers this way, but not real numbers. This also includes a great deal of combinatorics, basic algebra, and elementary logic, although not many advanced topics.


In the foundations of mathematics and in philosophy of mathematics, finitism is the philosophy that one should do only finite mathematics. In a weak sense, one should not assume the axiom of infinity; in a strong sense, one should even deny it by an axiom of finiteness. This makes it impossible to do analysis as we normally understand it.

Finitism (in the weak sense of not accepting an axiom of infinity) is essentially the mathematics that can be done internal to an arbitrary boolean topos (at least if one is not also being predicative or constructive). For constructive mathematics as usually practised, one goes beyond finitism by positing a natural numbers object.

Although often considered an extreme form of constructivism, finitism in the strong sense (actually denying the axiom of infinity) can make excluded middle and even the axiom of choice constructively acceptable (and similarly make power sets predicatively acceptable). This is because even constructivists agree that these are true in FinSet\Fin\Set; it's the extension of them to infinite sets that the first constructivists objected to.

In homotopy type theory, finite mathematics could be said to be the study of only the nn-truncated tame homotopy types for n:n:\mathbb{N}, which have finite homotopy groups, and type operations that preserve finiteness. Finite sets are just finite 0-truncated tame homotopy types in homotopy type theory. Certain type operations do not preserve tameness, such as suspensions, and so wouldn’t be part of finite mathematics. This extends traditional finite mathematics based in set theoretic foundations to more modern fields such as higher category theory and homotopy theory. Just as the cardinalities of finite sets are natural numbers (finite set cardinalities), the cardinalities of these nn-truncated homotopy types are positive rational numbers.

Ultrafinitism is an even more extreme form of finitism, in which one doubts the existence even of very large numbers, numbers which in some sense it is not physically possible to write down. The theory of ultrafinite mathematics is most well developed by Edward Nelson, although foundational systems such as soft linear logic can also be argued to have an ultrafinitist flavor.

For the opinionated espousal of finitism (and much else), one can hardly do better than the Opinions of Doron Zeilberger.


  • Edward Nelson, Warning Signs of a Possible Collapse of Contemporary Mathematics (pdf)

Last revised on April 13, 2021 at 21:39:44. See the history of this page for a list of all contributions to it.