Questions tagged [foundations]

The tag has no usage guidance.

Filter by
Sorted by
Tagged with
14
votes
1answer
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
1answer
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
3answers
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
2answers
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
2answers
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
3answers
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
0answers
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
3answers
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
5answers
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
2answers
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
1answer
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
4answers
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
1answer
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
0answers
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
0answers
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
0answers
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
5answers
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
1answer
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
0answers
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
2answers
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
1answer
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
4answers
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
0answers
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
2answers
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
1answer
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
1answer
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
2answers
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
6answers
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
1answer
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
1answer
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
2answers
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
3answers
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
2answers
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
0answers
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
2answers
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
0answers
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
1answer
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
0answers
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
1answer
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
0answers
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
1answer
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
6answers
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
0answers
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
3answers
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
0answers
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
1answer
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
0answers
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
1answer
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
1answer
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
4answers
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. ...

1
2 3 4 5