230 votes
Accepted

What makes dependent type theory more suitable than set theory for proof assistants?

I apologize for writing a lengthy answer, but I get the feeling the discussions about foundations for formalized mathematics are often hindered by lack of information. I have used proof assistants for ...
Andrej Bauer's user avatar
89 votes
Accepted

When size matters in category theory for the working mathematician

Very often one has the feeling that set-theoretic issues are somewhat cheatable, and people feel like they have eluded foundations when they manage to cheat them. Even worse, some claim that ...
Ivan Di Liberti's user avatar
73 votes
Accepted

How should a "working mathematician" think about sets? (ZFC, category theory, urelements)

Set theory provides a foundation for mathematics in roughly the same way that Turing machines provide a foundation for computer science. A computer program written in Java or assembly language isn't ...
Henry Towsner's user avatar
51 votes

Category theory and set theory: just a different language, or different foundation of mathematics?

I think that Penelope Maddy's article What Do We Want a Foundation to Do? is a good starting point if you want to read some literature. I don't agree with all of Maddy's conclusions but the ...
Timothy Chow's user avatar
  • 78.7k
49 votes
Accepted

In what respect are univalent foundations "better" than set theory?

I like your analogy with programming languages. If we think of ST as a low-level programming language and UF as a high-level one, then one advantage of UF is obvious: it is more convenient to write ...
45 votes

In what respect are univalent foundations "better" than set theory?

This is a question that has been discussed a lot on the Foundations of Mathematics mailing list (unfortunately with more polemics than necessary IMO—though I confess that I may have been guilty ...
45 votes
Accepted

Category theory and set theory: just a different language, or different foundation of mathematics?

Category theory and set theory are complementary to one another, not in competition. I think this 'debate' is a bit of academic controversialising rather than an actual difference. If you've done a ...
Harry Gindi's user avatar
  • 19.4k
40 votes

What makes dependent type theory more suitable than set theory for proof assistants?

EDIT: Since this question has gotten so much interest, I have decided to substantially rewrite my answer, stating explicitly here on MO some of the more important points rather than forcing the reader ...
Timothy Chow's user avatar
  • 78.7k
40 votes

Top-down mathematics, or "Where it all begins"

One approach, mentioned by Pace Nielsen in the comments, is to start with what I call strict formalism. The only substantive assumption required for strict formalism is that you are capable of ...
Timothy Chow's user avatar
  • 78.7k
39 votes

Do set-theorists use informal set theory as their meta-theory when talking about models of ZFC?

The main fact is that a very weak meta-theory typically suffices, for theorems about models of set theory. Indeed, for almost all of the meta-mathematical results in set theory with which I am ...
Joel David Hamkins's user avatar
39 votes
Accepted

What is some current research going on in foundations about?

It is quite difficult to answer this question comprehensively. It's a bit like asking "so what's been going on in analysis lately?" It is probably best if logicians who work in various areas each ...
37 votes
Accepted

Could groups be used instead of sets as a foundation of mathematics?

The answer is yes, in fact one has a lot better than bi-interpretability, as shown by the corollary at the end. It follows by mixing the comments by Martin Brandenburg and mine (and a few additional ...
Simon Henry's user avatar
  • 40.2k
32 votes

What makes dependent type theory more suitable than set theory for proof assistants?

I still find it very surprising that this random talk I gave attracts so much attention, especially as not everything I said was very well thought out. I am more than happy to engage with people in ...
Kevin Buzzard's user avatar
32 votes
Accepted

How much of the axiom of choice do you need in mathematics?

Your hypothesis is in a sense stronger than just assuming ZFC outright. Namely, if we have $\lambda$-DC for some inaccessible cardinal $\lambda$, and ZF in the background, then in particular, we will ...
Joel David Hamkins's user avatar
30 votes

Lists as a foundation of mathematics

Andreas Blass has already provided a good reference in the literature, but unfortunately I cannot read German, so I've had to make do with writing my own answer. As you observed, you're clearly not ...
James Hanson's user avatar
  • 10.3k
29 votes

Defining $SU(n)$ in HoTT

I think Noah's answer is mostly right, but partly misleading, and explaining why will take too much space for a comment, so I'm posting a separate answer. As Noah says, the main conceptual point is ...
Mike Shulman's user avatar
  • 65.1k
29 votes

When size matters in category theory for the working mathematician

Here's an example that links more to mathematical practice outside category theory proper. Recall that for a small site $(C,J)$, where I take $J$ to be a Grothendieck pretopology on the small category ...
David Roberts's user avatar
  • 33.9k
29 votes
Accepted

Building algebraic geometry without prime ideals

Actually, you have rediscovered a nice motivation of using prime ideals as points. Indeed, your collection of points are triples $(R, k_x, \mathrm{ev}_x)$ where , $\mathrm{ev}_x \colon R \to k_x$ is a ...
Leo Alonso's user avatar
  • 8,944
27 votes

How should a "working mathematician" think about sets? (ZFC, category theory, urelements)

I prefer to think of ZFC as a proposed model of mathematics. I want to emphasize both words "proposed" and "model". For comparison, consider quantum mechanics. It can be modeled — as far as we know, ...
Theo Johnson-Freyd's user avatar
27 votes

What is an explicit bijection in combinatorics?

This is not at all intended as a complete answer to the question, but one criterion that feels important is that for a bijection $f$ to count as explicit, one shouldn't need to know in advance that ...
gowers's user avatar
  • 28.7k
27 votes

Learning roadmap for Foundations of Mathematics (for the working mathematician)

One feature of the foundations of mathematics that poses a special challenge (compared to other branches of mathematics) is that it is very easy to get confused about certain distinctions—truth ...
27 votes

Can the opposite of an elementary topos be an elementary topos?

The answer to the question in the title is no, assuming you want to exclude the trivial case of the terminal category. Let $E$ be an (elementary) topos whose opposite is also a topos. The initial ...
Tom Leinster's user avatar
  • 27.2k
26 votes
Accepted

Defining $SU(n)$ in HoTT

This isn't easy to do, and the reason it isn't easy is because of the step "$\infty$-groupoids are the same thing as spaces." Of course the homotopy hypothesis tells you that any $\infty$-groupoid ...
Noah Snyder's user avatar
  • 27.8k
26 votes

When size matters in category theory for the working mathematician

The other answers are good, but I would like to point out that Ivan's "uncheatable" lemma can in fact be cheated. The proof of that lemma (due to Freyd) makes inescapable use of classical ...
Mike Shulman's user avatar
  • 65.1k
26 votes
Accepted

Why do we care about small sets?

First, it is important to distinguish between the problem related to the foundation you are using from the problems that are inherent to category theory. For example, the distinction between $\mathbb{...
Simon Henry's user avatar
  • 40.2k
25 votes

Do set-theorists use informal set theory as their meta-theory when talking about models of ZFC?

You asked: When set-theorists talk about models of ZFC, are they using an informal set theory as their meta-theory? The short answer is yes. A set theorist is doing mathematics and hence is ...
Timothy Chow's user avatar
  • 78.7k
25 votes
Accepted

Is V, the Universe of Sets, a fixed object?

As you noticed, the iterative conception of sets requires a pre-existing universe of sets, and ordinals with which we can label the stages. So if you work within ZFC itself, in other words within an ...
user21820's user avatar
  • 2,733
25 votes
Accepted

Formal definition of homotopy type theory

Here are some resources: The appendix of the homotopy type theory book gives two formal presentations of homotopy type theory. Martín Escardó wrote lecture notes Introduction to Univalent Foundations ...
Andrej Bauer's user avatar
24 votes
Accepted

Large categories vs. $\mathrm{U}$-categories: why is the loss of category-theoretic information inessential?

Let me try to answer as a set theorist, rather than as a category theorist, since I think that your question concerns at bottom a matter often considered in set theory. Namely, the essence of your ...
Joel David Hamkins's user avatar
23 votes
Accepted

Why would the category of sets be intuitionistic?

You wrote: Suppose our intuition for the phrase "subset of $X$" comes from the idea of having an effective total function $X \rightarrow \{0,1\}$ that returns an answer in a finite amount ...
Andrej Bauer's user avatar

Only top scored, non community-wiki answers of a minimum length are eligible