# Questions tagged [foundations]

The foundations tag has no usage guidance.

232
questions

**14**

votes

**1**answer

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

**9**

votes

**1**answer

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

**32**

votes

**3**answers

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

**10**

votes

**2**answers

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

**1**

vote

**2**answers

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

**11**

votes

**3**answers

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

**1**

vote

**0**answers

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

**33**

votes

**3**answers

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

**114**

votes

**5**answers

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

**15**

votes

**2**answers

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

**7**

votes

**1**answer

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

**8**

votes

**4**answers

580 views

### Self-contained formalization of random variables?

I have not been able to find any formalization of random variables that supports construction of new random variables dependent on previously constructed ones. In what I have found, a random variable $...

**6**

votes

**1**answer

267 views

### Set Theoretic Geology II: The structure of the directed partial order of grounds

In my previous question Set-theoretic geology: controlled erosion?
and the great answer by Jonas Reitz, I have learned a few things, starting from the awareness that I understand the fine-grain ...

**5**

votes

**0**answers

150 views

### Higher order arithmetic, hierarchies and proof theoretic ordinals

I asked this question on MSE some days ago but I have not received any answer so I have decided to post it here.
I would like to consider a generalization of the notation $\Pi$ and $\Sigma$ used for ...

**5**

votes

**0**answers

213 views

### Class theory of ZF-minus-Powerset as classical predicative system?

I've been thinking about some mathematics in weaker foundational systems a little bit, largely from a structural viewpoint, and with particular attention to classes.
Some categories I've been keeping ...

**4**

votes

**0**answers

275 views

### Iterated Gentzen: or, a Sith objection to the proof of consistency of PA

$\DeclareMathOperator\PRA{PRA}\DeclareMathOperator\WF{WF}\DeclareMathOperator\Con{Con}\DeclareMathOperator\PA{PA}$Preamble: In the year … in a galaxy far far away, a nasty Sith named Darth Dubious (...

**11**

votes

**5**answers

689 views

### Emergence of the discrete from the continuum

An almost eternal theme in Mathematics is the approximation of the Continuum by the Discrete. This core idea goes back at least to Archimedes, and remains active to these very days (and quite likely ...

**9**

votes

**1**answer

276 views

### An internalized version of Tennenbaum's Theorem

Tennenbaum's celebrated 1959 theorem (see here for a reference) is certainly one of the key theorems in mathematical logic. Not so much for its proof, but because it helps "isolating" $N$ ...

**1**

vote

**0**answers

130 views

### Complete and consistent first-order logics that contain interesting phenomena

Gödel has shown that a consistent recursively axiomatizable first-order logic that can interpret Robinson arithmetic is incomplete.
I think there is some sentimental value in working with a theory ...

**14**

votes

**2**answers

618 views

### Appearance of proof relevance in “ordinary mathematics?”

I've been wondering recently what—if any—applications proof theory has to ordinary mathematics (by which I mean algebra, analysis, topology, and so on). In particular, I'd be fascinated to see a proof ...

**1**

vote

**1**answer

261 views

### Reference request on Gentzen's proof of the consistency of PA

I've always been interested in having a good understanding of Gentzen's proof of the consistency of arithmetic.
Being more precise, he showed that $PRA + WF(\epsilon_0) \vdash Con(PA)$.
I am ...

**43**

votes

**4**answers

4k views

### When size matters in category theory for the working mathematician

I think a related question might be this (Set-Theoretic Issues/Categories).
There are many ways in which you can avoid set theoretical paradoxes in dealing with category theory (see for instance ...

**1**

vote

**0**answers

153 views

### A syntax independent theory of categories

The classic way to encounter the theory of categories is via Set Theory via the typical definition we see for categories. We see all kinds of categories that are equivalent to the category of small ...

**12**

votes

**2**answers

696 views

### The inconsistency of Graham Arithmetics plus $ \forall n, n < g_{64}$

As you all know, Ronald Graham just passed away. He is famous for many fabulous contributions to finite combinatorics, and much much more, but perhaps none of them is as popular as the infamous ...

**7**

votes

**1**answer

887 views

### Are categories special, foundationally?

Some folks over at nLab want to use categories as a foundation for all of mathematics, I'm guessing as an alternative to sets. Sets work fine, and so do categories, so I have started wondering what ...

**5**

votes

**1**answer

351 views

### Historical origin of the empty set

The question is in the title:
Who first claimed the existence / necessity of the empty set ? When did this happen ?
Of course I know that the notation $\emptyset$ goes back to André Weil, and that ...

**3**

votes

**2**answers

455 views

### What is a good definition of a mathematical structure?

At the moment I am writing a textbook in Foundations of Mathematics for students and trying to give a precise definition of a mathematical structure, which is the principal notion of structuralist ...

**63**

votes

**6**answers

5k views

### Category theory and set theory: just a different language, or different foundation of mathematics?

This is a question to research mathematicians, as well as to those concerned with the history and philosophy of mathematics.
I am asking for a reference. In order to make the reference request as ...

**16**

votes

**1**answer

578 views

### Positive set theory and the “co-Russell” set

This is a more focused version of a question which was asked at MSE a couple years ago, but is still unanswered there. That question asks about a broad range of theories, whereas this version focuses ...

**1**

vote

**1**answer

346 views

### coordinate free foundations of trigonometry [closed]

What axioms for geometry and trigonometry would I have to chose in order to completely avoid coordinates in defining trig functions and showing the equivalence of their geometric (unit circle) and ...

**3**

votes

**2**answers

537 views

### Shortest axiom of infinity for foundationless set theory

Let $T$ be the theory with a binary symbol $\in$, an unary symbol $S$, and the following axioms:
Axiom of extension:
\begin{equation}
\forall x \forall y (\forall z (z \in x \leftrightarrow z \in ...

**5**

votes

**3**answers

2k views

### How strong is this set theory?

In the spirit of this related question, consider a set theory with the following axioms:
Axiom of extension:
$$ \forall x \forall y (\forall z (z \in x \leftrightarrow z \in y) \rightarrow x = y) $$
...

**11**

votes

**2**answers

937 views

### Could Kronecker accept a proof of Goodstein's theorem?

A famous result of Goodstein asserts that the Goodstein sequence of integers terminates.
For a precise statement and a short proof, see https://en.wikipedia.org/wiki/Goodstein%27s_theorem.
A well ...

**0**

votes

**0**answers

187 views

### Is there a foundational approach that takes “structure” as primitive?

As per the title, I'd be curious to know if there have been attempts at constructing a foundation of mathematics taking, somehow, purely the notion of "structure" as primitive, maybe via a system of ...

**22**

votes

**2**answers

2k views

### Could groups be used instead of sets as a foundation of mathematics?

Sets are the only fundamental objects in the theory $\sf ZFC$. But we can use $\sf ZFC$ as a foundation for all of mathematics by encoding the various other objects we care about in terms of sets. The ...

**11**

votes

**0**answers

307 views

### Categorial foundations via “categories of algebras”

There are categorical foundations for mathematics axiomatizing the category of sets (Lawvere's ETCS), cartesian closed categories (type theory), and the category of spaces (homotopy type theory). ...

**0**

votes

**1**answer

268 views

### Set of definable real numbers?

Is there a set theory at least as strong as $KP\omega$ which has as a theorem that there is a set $\mathbb{D}$ of precisely the definable real numbers?

**3**

votes

**0**answers

204 views

### What does second order set theory give us that is new?

There is a natural analogy between the theories PA and ZFC. See the linked question by Gro-Tsen here.
Peano arithmetic (PA) is a first order approximation to the natural numbers. As is well known, ...

**-1**

votes

**1**answer

209 views

### Weak power set - what strength may it have?

In The Consistency of Classical Set Theory Relative to a Set Theory with Intuitionistic Logic in THE JOURNAL OF SYMBOLIC LOGIC Volume 38, Number 2, June 1973 page 316 Harvey Friedman's axiom 8* $Weak \...

**1**

vote

**0**answers

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

**5**

votes

**1**answer

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

**31**

votes

**6**answers

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

**2**

votes

**0**answers

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

**7**

votes

**3**answers

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

**5**

votes

**0**answers

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

**5**

votes

**1**answer

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

**3**

votes

**0**answers

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

**0**

votes

**1**answer

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

**3**

votes

**1**answer

354 views

### Problem Understanding Euclid Book 10 Proposition 1 [closed]

this is embarrassing, but I am having trouble reading through Proposition 1 of Book 10 of Euclid's elements. I'm struggling with Euclid's terminology and don't have a clear picture of what divisions ...

**15**

votes

**4**answers

1k views

### Practical example in using (homotopy) type theory

I have just read Grayson's introduction on homotopy type theory as a possible foundation for mathematics. It is very enlightening about what all the fuss is about, but I am left with some doubts. ...