210

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 a while now, and also worked on their design and implementation. While I will be quick to tell jokes about set theory, I am bitterly aware of the shortcomings ...


81

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 foundations are irrelevant because each time they dare to be relevant, they can be cheated. What these people haven't understood is that the best foundation is the one ...


71

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 actually a Turing machine, and there are lots of good reasons not to do real programming in Turing machines - real languages have all sorts of useful higher ...


47

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 proofs (programs) in a high-level language. It is feasible to write proofs in UF, but it's virtually impossible to write down even statements of theorems in plain ...


43

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 terminology that she introduces in this article is exceedingly helpful, as well as the very simple but often overlooked point that the concept of a "foundation of ...


42

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 of stoking the flames somewhat because I love to watch a good argument!). My feeling is that to ask whether univalent foundations or set theory is the "better ...


39

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 recognizing and manipulating finite strings of symbols in certain simple ways, and can understand what a syntactic rule is at the level of being able to confirm or ...


38

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 mereology can form a foundation of mathematics. In particular, for our main thesis we argue that the particular understanding of mereology by means of the inclusion ...


35

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 to follow links and chase down references. To begin with, it is important to distinguish between what currently existing proof assistants can do versus what ...


34

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 familiar, using only PA or considerably less in the meta-theory is more than sufficient. Consider a typical forcing argument. Even though set theorists consider ZFC ...


33

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 answer what is going on in their area. I will speak about logic in computer science. I am very curious to see what logicians from other areas have to say about ...


32

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 in the idea that sets are obtained by an iterative process along a wellordered "ordinal clock", where at each step all the sets whose elements were generated ...


30

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 discussions about what I said and whether or not some things I said were ill-informed. But onto my answer to your question: whilst I am not an expert in proof ...


28

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 homomorphism. The collection of all such triples is a class rather a set. In any case, you should not change the universe to get the underlying topological ...


27

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, perfectly — by the theory of Hilbert spaces. But the state right now of the electron in your retinal cell being excited by photon being emitted by the leftmost ...


27

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 that HoTT forces us to un-confuse ourselves about the difference between a topological space and an $\infty$-groupoid, which are conceptually distinct but ...


27

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 $C$, any presheaf $C^{op} \to \mathbf{Set}$ has a sheafification, and this extends to give us a functor $[C^{op},\mathbf{Set}] \to Sh(C,J)$ from presheaves to ...


26

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 there exists a bijection in order to prove that $f$ is a well-defined bijection. So for example if you order the elements of two sets $A$ and $B$ in some way that ...


26

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 details I found on MO). The key observation is the following: Theorem: The category of co-group objects in the category of groups is equivalent to the category ...


25

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 is equivalent to the fundamental $\infty$-groupoid of a space, but that doesn't mean that they're literally the same thing. The way that HoTT approaches about $\...


24

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 of Mathematics with Agda which are at the same time written as traditional mathematics and formalized in Agda (so as formal as it gets). Designed for teaching ...


24

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 object of a topos is strictly initial (any map into it is an iso), so the terminal object $1$ of $E$ is strictly terminal. Since there is a map from $1$ to the ...


23

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 reasoning informally, just like any other mathematician. It's important, at least when you're first wrapping your mind around these concepts, to distinguish between ...


23

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 versus provability, theory versus meta-theory, formal versus informal, syntax versus arithmetic, etc. One book that I think is helpful in this regard is Torkel ...


22

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 of time. In this case, the subsets of $X$ ought to form a Boolean algebra. Unfortunately, this is not a workable intuition at all. If you insist that all subsets be ...


22

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 question, to my way of thinking, revolves around the fact that Grothendieck universes (or Grothendieck-Zermelo universes, as one might call them) need not all ...


22

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 existing model of ZFC, you can perform that iterative construction to obtain $V$. Like Asaf Karagila says here, you cannot get nothing from nothing. Typically, ...


22

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 logic, and in constructive mathematics it is possible to have a non-poset that is complete for the size of its own set of objects (a complete small category). ...


21

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 can be defined for any family of types, or in models, for any fibration. The Univalence Axiom then says that a particular family of types — a “universe” — is ...


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