# Questions tagged [foundations]

The foundations tag has no usage guidance.

207
questions

**2**

votes

**1**answer

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

**17**

votes

**3**answers

718 views

### Examples of improved notation that impacted your research?

The intention of this question is to find practical examples of improved mathematical notation that enabled actual progress in someone's research work.
I am aware that there is a related post ...

**43**

votes

**4**answers

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

**15**

votes

**0**answers

404 views

+400

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

296 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

498 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) $$
...

**10**

votes

**2**answers

676 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

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

**21**

votes

**2**answers

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

**10**

votes

**0**answers

278 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

208 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

180 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

186 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

264 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

356 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

187 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

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

186 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

281 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

126 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

249 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

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

**14**

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

**2**

votes

**0**answers

150 views

### Why not replace reflection by bounded reflection in Muller's approach?

Bounded Reflection: If $\phi$ is a formula in the language of set theory [i.e.; $\small \sf FOL(=,\in)$], in which all and only symbols $``x,x_1,..,x_n"$ occur free, and $\phi^V$ is the formula ...

**22**

votes

**8**answers

3k views

### Good introductory book to type theory?

I don't know anything about type theory and I would like to learn it.
I'm interested to know how we can found mathematics on it.
So, I would be interested by any text about type theory whose angle ...

**1**

vote

**2**answers

211 views

### Cardinals in $ZFC+\neg CH$

Before asking my question I like to admit that i am not an expert in the foundation of mathematics and I am interested in this issue more from a philosophical perspective. So my question may be ...

**7**

votes

**1**answer

223 views

### Logic with “co-relations” - sources?

My question is on a seemingly-natural extension of classical logic that I've been playing around with a bit in the context of generalized recursion theory. I'm sure it's been treated extensively ...

**5**

votes

**1**answer

843 views

### Which branches of mathematics can be done just in terms of morphisms and composition?

Consider the first-order language $L_{\omega\omega}$ of the signature $L:=\{\mathrm{dom}, \mathrm{cod}, \mathrm{comp}\}$, where $\mathrm{dom}$ and $\mathrm{cod}$ are unary function symbols and $\...

**42**

votes

**7**answers

4k views

### What is an explicit bijection in combinatorics?

A standard way of demonstrating that two collections of combinatorial objects have the same cardinality is to exhibit a bijection between them. Browsing through some examples (here, there, yonder) ...

**7**

votes

**1**answer

632 views

### Explaining the consistency of PRA and ZF from predicative foundations

Recently I got interested in predicative foundations, mostly because of Laura Crosilla's work and because Agda employs a predicative type theory.
From the point of view of a predicative foundation to ...

**4**

votes

**1**answer

231 views

### “Surjective cardinals” - using surjections rather than injections to define isomorphism classes of sets

Cantor used the notion of an "injection" to formalize the size of two sets: A is "smaller" than B if A injects into B.
Simply put, the question is - how does this situation change if we use ...

**11**

votes

**1**answer

926 views

### ZF(C) and category theory

Is there an axiomatisation of some kind of category theory and a definition of sets in this framework such that the axioms of ZF resp. ZFC are theorems?

**1**

vote

**0**answers

69 views

### Questions in proof theory (PRA-provability of EA-theorems, Girards book from '87)

I've been working through a textbook, often encountering difficulties with the exercises.
On mathstackexchange, with most of them I haven't arrived yet at a satisfactory solution.
As I understand, ...

**0**

votes

**0**answers

80 views

### Shepherdson's conditions - a shortcut to the second incompleteness theorem?

I've been working through a textbook, often encountering difficulties with the exercises. On mathstackexchange, with most of them I haven't arrived yet at a satisfactory solution.
As I understand, ...

**2**

votes

**0**answers

288 views

### Does this axiomatic system satisfy requirements for founding mathematics?

In this article, the author, F.A.Muller, suggests criteria for a founding theory of mathematics (pp:14-16). The author proposes $ARC$ Class Theory to embody these requirements. The motivation is ...

**3**

votes

**0**answers

256 views

### Formal foundations done properly [closed]

I would want to do mathematics properly, so that the proofs of results can be trusted on instead of them being just suggestions on which results could perhaps apply. This means formulating the math in ...

**4**

votes

**0**answers

147 views

### Formalization and set-theoretic issues in the definition a functor category

Universes are used in a category theory to handle size-issues. Assuming Grothendieck's axiom UA that
every sets is contained in some universe
there are two approaches to $U$-smallness given a ...

**13**

votes

**1**answer

560 views

### A peculiarity of Henkin's 1950 proof of completeness for higher order logic

My question concerns Henkin's original (1950) completeness proof https://projecteuclid.org/euclid.jsl/1183730860 for classical higher order logic and type theory relative to so-called general models.
...

**6**

votes

**3**answers

381 views

### How do we formally construct the successor universe $\mathscr{U}^+$ of a universe $\mathscr{U}$ in $\mathsf{ZFC}$?

A set $\mathscr{U}$ is a universe if the following conditions are met:
For any $x \in \mathscr{U}$ we have $x \subseteq \mathscr{U}$
For any $x,y \in \mathscr{U}$ we have $\{x,y\} \in \mathscr{...

**12**

votes

**1**answer

407 views

### Translating Grothendieck axiom UB into ZFC

In SGA 4, Grothendieck introduced a set-theoretic device called a Grothendieck universe. He and his collaborators worked in Bourbaki set theory, which is practically similar to $\mathsf{ZFC}$ but ...

**4**

votes

**2**answers

331 views

### Limits, colimits and universes

For many purposes in category theory, we consider limit and colimits of diagrams $F\colon\mathsf{J\to C}$ where $\mathsf{J}$ is small category, that is, a category where the classes of objects and ...

**5**

votes

**1**answer

202 views

### Does the notion of a compactly generated space (or $k$-space) depend on the choice of universe?

We recall the notion of a $k$-space (or compactly generated space) to fix our notations. For every topological space $X$, we can define a category $\mathfrak{M}_X$. The class of objects of $\mathfrak{...

**4**

votes

**1**answer

357 views

### What is the definition of a $\mathcal{U}$-category?

Let $\mathcal{U}$ be a universe. The adaptation of the concept of a locally small category to universes is a $\mathcal{U}$-category.
There are two definitions of $\mathcal{U}$ category I've met.
$...

**7**

votes

**1**answer

450 views

### Enhancing Grothendieck's universes and Grothendieck's axiom: Feferman's universe

A Grothendieck's universe is such a set $U$ so that
$\forall x \in U, x \subseteq U$,
$\forall x,y \in U, \{x,y\} \in U$,
$\forall x \in U, \mathcal{P}(x) \in U$,
given a family $(X_i)_{i \...

**7**

votes

**3**answers

883 views

### Are there logical systems where formal proofs are not computer verifiable?

In a set-theoretic system using first-order logic, every proof could be written as a goal followed by a finite sequence of sentence where each one is justified by an axiom or previously established ...

**5**

votes

**3**answers

420 views

### Counting without one-to-one correspondence? [closed]

Ash and Gross in their wonderful book Fearless Symmetry found it worth mentioning (and thus suggesting) another way of counting for which "we do not even need to know how to count" (in the sense of ...

**20**

votes

**0**answers

1k views

### Is Feferman's unlimited category theory dead?

In The prospects of unlimited category theory: doing what remains to be done, 2014 (The Review of Symbolic Logic, 8 (2015) pp 306-327, link), Ernst discusses Feferman's program, described in ...

**20**

votes

**4**answers

1k views

### Mathematics without the principle of unique choice

The principle of unique choice (PUC), also called the principle of function comprehension, says that if $R$ is a relation between two sets $A,B$, and for every $x\in A$ there exists a unique $y\in B$ ...