Questions tagged [foundations]

The tag has no usage guidance.

Filter by
Sorted by
Tagged with
2
votes
1answer
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
3answers
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
4answers
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
0answers
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
1answer
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
2answers
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
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) $$ ...
10
votes
2answers
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
0answers
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
2answers
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
0answers
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
1answer
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
0answers
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
1answer
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
0answers
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
1answer
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
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
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
2answers
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
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
1answer
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
0answers
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
1answer
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
1answer
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
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. ...
2
votes
0answers
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
8answers
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
2answers
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
1answer
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
1answer
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
7answers
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
1answer
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
1answer
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
1answer
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
0answers
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
0answers
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
0answers
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
0answers
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
0answers
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
1answer
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
3answers
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
1answer
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
2answers
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
1answer
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
1answer
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
1answer
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
3answers
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
3answers
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
0answers
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
4answers
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$ ...

1
2 3 4 5