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

- 45.1k

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

- 7,777

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

- 7,035

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

- 70.9k

47
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

43
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

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

- 19.1k

40
votes

Accepted

### Why hasn't mereology succeeded as an alternative to set theory?

I have long found this question interesting, and in some recent joint work with Makoto Kikuchi, now available, we consider various aspects of the question of whether a set-theoretic version of ...

- 206k

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

- 70.9k

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

- 206k

38
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

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

- 70.9k

35
votes

### Who needs Replacement anyway?

I think the main reason replacement is seen as an essential part of ZF is that it naturally follows from the ontology of set theory, as do the other axioms of ZF. The ontology of set theory is rooted ...

- 42.9k

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

- 36.8k

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

- 39.9k

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

- 32k

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

- 8,406

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

- 62.4k

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

### 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.4k

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

- 28k

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

- 62.4k

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

- 36.8k

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

- 27.3k

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

- 70.9k

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

- 45.1k

24
votes

### What is the most transparent, rigorous definition of the Univalence Axiom?

I’ll give first a simplicial definition of univalence, and then a type-theoretic one, and discuss the equivalence between them as we go.
The first thing to know is that univalence is a property that ...

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

- 206k

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

- 70.9k

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

- 45.1k

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

#### Related Tags

foundations × 287lo.logic × 167

set-theory × 131

ct.category-theory × 56

mathematical-philosophy × 43

reference-request × 26

soft-question × 25

type-theory × 20

model-theory × 19

axioms × 18

proof-theory × 16

homotopy-type-theory × 16

constructive-mathematics × 14

theories-of-arithmetic × 14

ho.history-overview × 11

ordinal-analysis × 9

ordinal-numbers × 8

reverse-math × 8

mg.metric-geometry × 7

large-cardinals × 7

higher-category-theory × 6

computability-theory × 6

topos-theory × 6

metamathematics × 6

new-foundations × 6