basic constructions:
strong axioms
further
In the context of foundations of mathematics or mathematical logic one studies formal systems – theories – that allow us to formalize much if not all of mathematics (and hence, by extension, at least aspects of mathematical fields such as fundamental physics).
There are two different attitudes to what a desirable or interesting foundation should achieve:
In proof-theoretic foundations the emphasis is on seeing which formal systems, however convoluted they may be conceptually, allow us to formalize and prove which theorems.
The archetypical such system is ZFC set theory. Other formal systems of interest here are elementary function arithmetic and second order arithmetic, because they are proof-theoretically weak, and still can derive “almost all of undergraduate mathematics” (Harrington).
In practical foundations (following a term introduced in (Taylor)) the emphasis is on conceptually natural formalizations that concentrate the essence of practice and in turn use the result to guide practice (Lawvere), as in (Eilenberg-Steenrod, Harper).
Formal systems of interest here are ETCS or flavors of type theory, which allow natural expressions for central concepts in mathematics (notably via their categorical semantics and the conceptual strength of category theory).
For a philosophical treatment of foundations see foundations and philosophy.
Almost all foundations of mathematics are expressed in some foundational deductive system.
One versatile deductive system natural deduction, which could be used to define certain foundation of mathematics using logic over type theory, such as all set theories, including categorical set theories like ETCS, as well as the foundations of mathematics using only type theory, including set-level type theories as well as higher foundations such as homotopy type theory, as well as typed higher-order logic.
Alternatives include sequent calculus for logic over untyped theories, such as unsorted set theory and untyped higher-order logic, as well as lambda-calculus for type theories.
Dependent type theory itself supports various foundations of mathematics via the propositions as some types interpretation of dependent type theory. Suppose that a dependent type theory has a separate type judgment as well as dependent product types, dependent sum types, identity types, weak function extensionality, propositional truncations, empty type, unit type, sum types. All the operations in predicate logic are derivable from said type formers. Then:
One can add a cumulative hierarchy to the dependent type theory and work entirely in the cumulative hierarchy for material set theory
One can add a category of sets to the dependent type theory and work entirely in the category of sets for structural set theory
One can add a type universe satisfying certain axioms and axiom schemata, such as universe extensionality, closure under identity types, closure under dependent sum types, closure under dependent product types, propositional resizing, replacement, infinity, and choice, to the dependent type theory and work entirely in the universe for univalent type theory or univalent foundations. Adding internal universe types as small object classifiers as well as all higher inductive and coinductive types to the universe results in homotopy type theory.
One can add a Russell type of all propositions and a natural numbers type and work in the dependent type theory itself for higher-order logic.
In most foundations of mathematics, there are basic notions of objects and collections of objects.
Note that in certain foundations, the objects, collections, and membership are derived notions from some other notion. Collections are referred to a number of names, such as set, class, type, et cetera. Objects could be referred to as element or term.
For example, in pure set theories like ZFC and Mostowski set theory, elements and sets are the same notion, and thus elements could be considered to be a derived notion from set, or sets could be considered to be a derived notion from element. In material set theory with urelements, such as ZFA, elements are the basic notion and sets are derived from elements. In ETCS, while sets are basic, elements are derived from a basic notion of function, and in fully formal ETCS, both sets and elements are derived notions from a basic notion of function. In SEAR and structural ZFC, sets and elements are both basic distinct notions.
Something similar occurs with class theories, such as Morse-Kelley class theory and the framework of algebraic set theory, where classes play the role of sets.
In type theory, there are also a distinction to be made. In most type theories, both terms and types are basic foundational notions. However, in book HoTT, terms are the basic notion, and types are derived from terms.
In higher-order logic, the domain of discourse and higher-order predicates play the role of collections, while the objects in the domain of discourse play the role of the elements.
In most foundations, there is a basic notion of membership, of an “object being in a collection”.
Foundations could be contrasted between those foundations where membership is a membership relation, and those foundations where membership is a typing judgment?. This distinction is largely the same distinction as the distinction between unsorted set theories and simply sorted set theories on one hand, and dependently sorted set theories and dependent type theories on the other hand.
For theories with a membership relation, one could further distinguish between homogeneous membership relations (for relations on the same sort) and heterogeneous membership relations (for relations between two different sorts), as well as membership relations which are primitive to the theory, and membership relations which are derived from some other existing structure in the theory.
For theories with a typing judgment, one simply judges the object, element, or term a to be in the collection, set, or type A, () or a:A. This is in contrast to membership relations, where () is a proposition with some truth value, and thus one could say whether the proposition that the object, element, or term a is in collection, set, or type A is true or not.
Formally, there are also a difference in the contexts. When () or a:A is a judgment, then it lies in the type layer, but when () is a true proposition, then it lies in the proposition layer Φ while the typing judgment a:Set lies in the type layer.
In most foundations such as dependent type theory and logic over type theory, one distinguishes various different notions of equality or equivalence of the terms of the language.
There are broadly three different notions of equality which could be distinguished: judgmental equality, propositional equality, and typal equality, each of which applies for both objects (elements, terms) and collections (sets, classes, types). Judgmental equality is defined as a basic judgment in the foundations. Propositional equality is defined as a proposition in any typed predicate logic. Typal equality is defined as a type in type theory, and is also called the identity type or path type for elements, and the type of equivalences for types.
The equality of elements used in most set theories and class theories are propositional equalities. The equality of elements used in dependent type theories are typal equality. If the dependent type theory is not an objective type theory, most likely it also either has one of judgmental equality or propositional equality to use for definitions.
The equality of collections differs from theory to theory. There are set theories and class theories where propositional equality is used as the notion of equality between sets and classes, while for other set theories and class theories, the notion of equality between sets and classes is rather bijection of sets and classes, rather than equality of sets and classes. Something similar happens in dependent type theory, depending on whether one uses a separate type judgment, or Russell universes without a separate type judgment: for Russell universes, the identity type is used for the equality of types in the universe, since types are terms of Russell universes. On the other hand, the dependent type theories with a separate type judgment, there is no identity type between two types, and one has to use the type of equivalences instead.
A mathematical foundation is said to respect the principle of equivalence if there is no strict propositional equality between sets. Thus, any unsorted set theory like fully formal ETCS violates the principle of equivalence.
In most foundations of mathematics, there is no way to talk about the collection of all collections; this is known as size issues in mathematics. However, there is a way around it, by the usage of universes. Essentially, instead of trying to talk about the collection of all sets, one instead talks about the collection U, whose elements are called U-small sets or U-small types, and whose subsets or subtypes are called U-classes. The objects not in U are called U-large sets or U-large types, and the subsets or subtypes which are not singleton subsets or subtypes are called U-proper classes. Each foundations of mathematics has their own approach to universes:
In set theory, one usually either uses Grothendieck universes, or some internal model of set theory or class theory, whether well-pointed Heyting categories, well-pointed division allegories, sets with extensional well-founded transitive relations, categories with class structure, et cetera.
In class theory, the notion of universe is already in the theory via the universal class, which is by definition a class universe. The basic primitive in class theory are classes, and the U-small classes are called sets.
In dependent type theory, one uses univalent Russell universes or Tarski universes, which are basically internal models of dependent type theory.
It may seem on first sight that foundational questions in mathematics are remote from “real mathematics”. This is not quite so. For a list of “real world” problems that do depend on foundations see
William Lawvere, Foundations and applications: axiomatization and education, Bulletin of Symbolic Logic 9 (2003), 213-224 (ps, Euclid)
L. A. Harrington (ed.), Harvey Friedman’s Research on the Foundations of Mathematics, Studies in Logic and the Foundations of Mathematics (2012)
Stefania Centrone, Deborah Kant, Deniz Sarikaya (editors), Reflections on the Foundations of Mathematics, Synthese Library 407 Springer (2019) [doi:10.1007/978-3-030-15655-8]
Practical foundations in terms of type theory language are laid out in
Under computational trinitarianism this corresponds to a practical foundation in programming, laid out in
A classification of material set theories and structural set theories is in
A foundation for algebraic topology in this practical spirit is laid out in
A big picture intro to the comparison between set theory, type theory and topos/category theory as approaches to foundations is in
A comparative discussion of complexities of different foundations is in
Freek Wiedijk, Is ZF a hack? Comparing the complexity of some (formalist interpretations of) foundational systems for mathematics (pdf)
Abstract This paper presents Automath encodings (which also are valid in LF/P) of various kinds of foundations of mathematics. Then it compares these encodings according to their size, to find out which foundation is the simplest.
The systems analyzed in this way are two kinds of set theory (ZFC and NF), two systems based on Church’s higher order logic (Isabelle/Pure and HOL), three kinds of type theory (the calculus of constructions, Luo’s extended calculus of constructions, and Martin-Löf predicative type theory) and one foundation based on category theory. The conclusions of this paper are that the simplest system is type theory (the calculus of constructions) but that type theories that know about serious mathematics are not simple at all. Set theory is one of the simpler systems too. Higher order logic is the simplest if one looks at the number of concepts (twenty-five) needed to explain the system. On the other side of the scale, category theory is relatively complex, as is Martin-Löf’s type theory.
Colin McLarty, Set theory for Grothendieck’s number theory, pdf
Last revised on January 7, 2024 at 14:47:27. See the history of this page for a list of all contributions to it.