nLab effects of foundations on core mathematics

Contents

Context

Foundations

foundations

The basis of it all

 Set theory

set theory

Foundational axioms

foundational axioms

Removing axioms

Mathematics

Contents

Idea

The foundations of mathematics may seem to be a topic curiously disconnected from the core of mathematical practice. But in fact, the foundations of mathematics has a significant impact upon core mathematics; different foundational rules and axioms included in the foundations of mathematics would result in certain theorems being true in one foundation of mathematics, false in another foundation of mathematics, and independent? in a third foundation of mathematics. This page lists numerous examples where questions of foundations do affect questions and problems in core mathematics.

The term “core mathematics” is discussed in Quinn 2012.

Examples

Large cardinal axioms

Large cardinal axioms, traditionally not assumed in various foundations, have effects in real mathematics:

  • That every extremally disconnected profinite set has a hypercover whose terms are extremally disconnected requires that beth cardinals exist. See Peter Scholze’s comment here. In particular, it is provable in Zermelo-Frankel set theory, but not provable in Zermelo set theory or ETCS, because replacement implies that beth cardinals exist, and while Zermelo-Frankel set theory has replacement, neither Zermelo set theory nor ETCS have replacement or beth cardinals.

Excluded middle

Axiom of choice

See the nLab’s list of statements equivalent to the axiom of choice.

See also Wikipedia’s list of statements equivalent to the axiom of choice.

There are a number of theorems that are strictly weaker than the axiom of choice but traditionally proved using the axiom of choice; these could be assumed as foundational axioms of intermediate strength between nothing and the axiom of choice. Wikipedia has a list of them here.

The Consequences of the Axiom of Choice Project provides an interactive data base that can be used to search for implications between various (weakened) forms of the Axiom of Choice. Choiceless grapher builds on this data and provides a graphical presentation.

See also Wikipedia's list of statements undecidable in ZFC.

Whitehead’s theorem

In set theory, Whitehead's theorem is a theorem valid for all infinity-groupoids, modeled as Kan complexes or CW-complexes. However, in homotopy type theory, Whitehead’s theorem is not provable when regarded as a statement about types in homotopy type theory, since it admits models in non-hypercomplete (∞,1)-toposes. As a result, the truth of Whitehead’s theorem is a foundational axiom that may be regarded as a “classicality” property, akin to excluded middle or the axiom of choice, and is usually called Whitehead’s principle by homotopy type theorists.

Univalence

Whitehead problem

The following question is called the Whitehead problem

Every free abelian group AA satisfies Ext 1(A,)=0Ext^1(A,\mathbb{Z}) = 0. Is, conversely, every abelian group AA that satisfies Ext 1(A,)=0Ext^1(A,\mathbb{Z}) = 0 a free abelian group?

When formalizing group theory within ETCS as a set theory, then this question is undecidable. (It is still undecidable in ZFC, equivalently in ETCS + Collection.) In some models it is true, while other models have counterexamples. As a result, it is also undecidable in homotopy type theory.

Fermat’s last theorem

It was conjectured by Harvey Friedman that all theorems involving finitary objects published in Annals of Mathematics (for argument’s sake) can be proved in Elementary Function Arithmetic (EFA), a weak fragment of Peano arithmetic. One implication is that Fermat's last theorem is provable in PA. There is a current program of research by Angus MacIntyre to show this last fact directly. From a category theoretic point of view, Colin McLarty has shown that all of the material in SGA relies only on quite weak foundations, namely MacLane set theory (McLarty 2020) with one universe (weaker than the theory V ω3V_{\omega\cdot 3} considered in ZFC).

McLarty 2010 comments extensively on the possibility of proving Fermat’s last theorem, and more generally the Modularity theorem, in PA.

See also

References

Last revised on June 9, 2022 at 03:16:07. See the history of this page for a list of all contributions to it.