# Questions tagged [foundations]

The tag has no usage guidance.

232 questions
Filter by
Sorted by
Tagged with
543 views

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

This question is not really about elementary topoi, it is much more about a category $(\mathcal{E}, \Omega)$ admitting a subobject classifier, or about a category with power objects, you can choose ...
349 views

### Is material set theory conservative over structural set theory?

Suppose a statement $\phi$ that doesn't use the global $\in$-relation or the global $=$-relation in an essential way is provable in some material set theory, say bounded Zermelo with choice. (So that ...
3k views

### Top-down mathematics, or “Where it all begins”

Sorry if this is off-topic. It was my attempt to take a top-down approach to mathematics. Being an inexperienced undergraduate (so please take my writing here lightly), I've been presented with ZFC as ...
881 views

### When the definition of a set starts to matter in category theory

In most introductory courses to category theory, the precise definition of a set is more-or-less ignored. The idea being that all basic results in the subject hold for any reasonable definition of a ...
948 views

### Has there been any serious attempt at a “circular” foundation of mathematics?

As far as I know, there is no published attempt at a "circular" foundations of mathematics though I'ave seen it noted by many category theorists and logicians without in-depth analysis, e.g ...
662 views

### Elementary theory of the category of groupoids?

One axiomatisation of set theory, the Elementary Theory of the Category of Sets, or ETCS for short, comes from category theory and states that sets and functions form a locally cartesian-closed, ...
344 views

### Is this a good way of conceptualising the current status of Foundation of Maths projects?

I have been reading 'A Very Short Introduction to Mathematics' by Timothy Gowers and at one point he mentions that most of the mathematical proofs can be finally resolved to a set of logical ...
2k views

### Building algebraic geometry without prime ideals

$\DeclareMathOperator\Spec{Spec}\DeclareMathOperator\ev{ev}$Teaching algebraic geometry, in particular schemes, I am struggling to provide intuitive proofs. In particular, I find it counter-intuitive ...
19k views

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

In his talk, The Future of Mathematics, Dr. Kevin Buzzard states that Lean is the only existing proof assistant suitable for formalizing all of math. In the Q&A part of the talk (at 1:00:00) he ...
1k views

### Formal definition of homotopy type theory

The HoTT community is quite friendly, and produces many motivational introductions to HoTT. The blog and the HoTT book are quite helpful. However, I want to get my hands directly onto that, and am ...
273 views

### What is difference between working with small and large category of spaces?

The following construction have always bugged me. This is p328, Remark 5.1.6.1 in Lurie's Higher Topos Theory. Lurie begins with the following: Construction: Let $C$ be a simplicial set. $S$ denote ...
580 views

270 views

### A countable set theory providing choice?

Instead of Zermelo set theory $Z$ take $Y$ = $Z$ minus the power set axiom plus Enumerability: $\forall x(x\neq \emptyset \to\exists f[f:\mathbb{N}\overset{onto}{\frown}x ])$ $\imath$ is the ...
388 views

### Is ETCS well-founded?

I can't find a statement about the axiom of regularity anywhere in treatments of ETCS. Perhaps this is due to the unfortunate clash of terminology with 'foundations'.
3k views

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

(At the risk of being vapulated and downvoted, I'll ask this here.) Suppose you work in a field that has nothing to do with the foundations of mathematics, but thanks to MO, you are becoming more and ...
195 views

### Smallest ordinal modelling $\aleph_1$?

Let $X_1$ be the class of all ordinals $\alpha$ such that there exists a transitive model $M$ of ZF(C) such that $M$ thinks that $\alpha$ is $\aleph_1$. Every class of ordinals has a minimum element (...
1k views

### How much of concrete mathematics can be expressed in the language of category theory?

Question 1 How much of group/ring/lattice/... theory can be expressed in purely categorical terms (only using the notions object, morphism, identity morphism, and composition), that is, as properties ...
194 views

### Are any formal systems based upon the idea of “iterated characterization pushing” currently in existence? If not, is anyone working on them?

I had an idea in regards to the design of formal systems with foundational aspirations. To convey the idea, let's talk a bit about the second-order Peano axioms. The way these axioms work, we have a ...
326 views

### Can set-like objects obeying ZFC be constructed in Euclidean geometry?

Is it possible to base set theory on Euclidean geometry, by carefully defining various notions from set theory in terms of geometric objects, so that the ZFC axioms can be shown to hold for them? ...
130 views

### Is well-pointedness the reason that the internal/external distinction seems not to apply to $\mathbf{Set}$?

When reasoning about the category of sets, we usually don't have to worry about the internal/external distinction. For example, if $f : X \rightarrow Y$ is a morphism of sets, then $f$ is either ...
257 views

### Formalizing ontological optimism

Inform speaking ontological optimisms means that everything that possibly exists in the abstract reality actually exists. From this principle we (again informally) get the Axiom of infinity, the Power ...