# Tag Info

## Hot answers tagged foundations

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

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

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

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

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

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

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

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

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

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

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

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

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

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