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 ...

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 ...

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 ...

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 ...

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 ...

Community wiki

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 ...

Community wiki

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 ...

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 ...

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 ...

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 ...

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 ...

Community wiki

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 ...

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 ...

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 ...

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 ...

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 ...

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 ...

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 ...

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, ...

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 ...

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 ...

Community wiki

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 ...

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 ...

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 ...

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{...

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 ...

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 ...

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 ...

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 ...

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 ...

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

#### Related Tags

foundations × 313lo.logic × 186

set-theory × 146

ct.category-theory × 57

mathematical-philosophy × 43

reference-request × 28

soft-question × 26

type-theory × 22

axioms × 22

model-theory × 21

homotopy-type-theory × 18

proof-theory × 17

constructive-mathematics × 15

theories-of-arithmetic × 14

ho.history-overview × 12

reverse-math × 9

ordinal-analysis × 9

mg.metric-geometry × 8

computability-theory × 8

large-cardinals × 8

ordinal-numbers × 8

topos-theory × 7

ultrafinitism × 7

higher-category-theory × 6

metamathematics × 6