nLab foundations and philosophy

The boundary between philosophical and logical foundational studies of mathematics is very unclear indeed – one has only to think of Russell’s part in Principia Mathematica. For a discussion of more obviously logical foundational aspects of category theory see foundations.

To be done

Foundations and the philosophy of language in mathematics

Different foundations of mathematics provide different languages to use for presenting concepts in mathematics, and the symbols and words used in various foundations have different meanings? from each other.

We work in a deductive system with hypothetical judgments, and give examples of how different foundations of mathematics written in natural deduction result in different meanings of symbols used in the judgments used in each foundation.

For example, take the symbol $\in$ denoting membership in set theory and set-level dependent type theories. In unsorted set theory and simply sorted set theory, $\in$ is a proposition in the context of an element variable and a set variable. The formal judgment $a \in A \; \mathrm{prop}$ means that “‘the element $a$ is in the set $A$’ is a proposition”, and the judgment $a \in A \; \mathrm{true}$ is commonly abbreviated as $a \in A$ and means that “the proposition that the element $a$ is in the set $A$ is true”. In dependently sorted set theory, and in unlayered set-level dependent type theories, $\in$ is a metatheoretic judgment, rather than being part of the actual structure of the theory. The formal judgment $a \in A$ simply means that “$a$ is in the set $A$”, rather than “the proposition that the element $a$ is in the set $A$ is true”; there is no propositional truth value attached to $a \in A$. Thus, the foundational notion of membership in unsorted and simply sorted set theories is semantically different from the notion of membership in dependently sorted set theories and unlayered set-level dependent type theory.

Similarly, the symbol $=$ denoting equality have different meanings in different theories.

Philosophical papers

Jean-Pierre Marquis, 1995, Category Theory and the Foundations of Mathematics: Philosophical Excavations. Synthese 103 (3).

Jean-Pierre Marquis, 2008, From a Geometrical Point of View

Steve Awodey, 2004, An Answer to Hellman’s Question: “Does Category Theory Provide a Foundation for Mathematical Structuralism?”

Ralph Krömer, 2007, Tool and Object: A History and Philosophy of Category Theory

Colin McLarty, 2005, Learning from Questions on Categorical Foundations

Colin McLarty, 2004, ‘Exploring Categorical Structuralism’, Philosophia Mathematica, 12, 37–53.