nLab finite mathematics

Idea

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

We may say that finite mathematics is mathematics done internal to the category FinSet of finite sets or the mathematics of $\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.

Finite mathematics also includes a great deal of combinatorics, basic algebra, and elementary formal logic, although not many advanced topics.

Finitism

In the foundations of mathematics and in philosophy of mathematics, finitism is the philosophical sentiment 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 $\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 $n$-truncated tame homotopy types for $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 homotopy pushouts, 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 $n$-truncated homotopy types are positive rational numbers.

Ultrafinitism is an even more extreme form of finitism, in which one doubts the existence of certain very large natural numbers. The theory of ultrafinite mathematics is most well developed by Edward Nelson in Nelson arithmetic. Foundational systems such as soft linear logic can also be argued to have an ultrafinitist flavor.

This is also true of foundational systems using paraconsistent logic, where paraconsistent arithmetics can have only a finite number of natural numbers. In particular, there is a paraconsistent version of the Löwenheim-Skolem theorem, which states:

Any mathematical theory presented in first order logic has a finite paraconsistent model.

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

See also

• predicative mathematics

• constructive mathematics

• paraconsistent mathematics

• Nelson arithmetic

References

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

• Manuel Bremer, Inconsistent Mathematics, (slides)