Stack Exchange Network

Stack Exchange network consists of 174 Q&A communities including Stack Overflow, the largest, most trusted online community for developers to learn, share their knowledge, and build their careers.

Visit Stack Exchange

Questions tagged [foundations]

The tag has no usage guidance.

-6
votes
0answers
150 views

Foundation of topology based on genus? [on hold]

I have heard the following slogan numerous times - Topology is the study of shapes you can do "whatever you want to" (continously) as long as you never tear them. I have also heard, that the ...
3
votes
0answers
179 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
97 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 ...
12
votes
1answer
472 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
331 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{...
11
votes
1answer
353 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 ...
2
votes
1answer
218 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 ...
4
votes
1answer
159 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
311 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. $...
6
votes
1answer
380 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 \...
6
votes
3answers
821 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
403 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 ...
19
votes
0answers
808 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 ...
19
votes
4answers
870 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$ ...
10
votes
2answers
345 views

Consequences of foundation/regularity in ordinary mathematics (over ZF–AF)?

This is a followup question to Does foundation/regularity have any categorical/structural consequences, in ZF? As shown in answers to that question, the axiom of foundation (AF, aka regularity) has ...
7
votes
0answers
184 views

Erroneous proof of recursion theorem examples

In his book Elements of Set Theory, Herbert Enderton defines (p. 70) a Peano system as a triple $(N, S, e)$ where $N$ is a set, $S$ is an $N-$valued function defined on $N$ and $e$ is a member of $N$ ...
13
votes
2answers
589 views

Does foundation/regularity have any categorical/structural consequences, in ZF?

(Prompted by reflection on this old answer, and its suggestion of the “harmlessness” of the axiom of regularity.) In ZFC, one may justify the axiom of foundation (AF, aka the axiom of regularity) as ...
4
votes
0answers
366 views

What are the requirements of a foundational theory?

There are multiple languages to describe all of mathematics, and there are some equivalences between them, some more successful then others. My question is can we describe some requirements (in some ...
-2
votes
1answer
251 views

Is it natural to hold that Ur-elements, small & big sets and proper classes exists? [closed]

The topic of this post was shifted to https://philosophy.stackexchange.com/questions/49504/is-it-natural-to-hold-that-big-sets-and-proper-classes-exist Since it was deemed to be a philosophical ...
28
votes
6answers
3k views

Is V, the Universe of Sets, a fixed object?

When I first read Set Theory by Jech, I came under the impression that the Universe of Sets, $V$ was a fixed, well defined object like $\pi$ or the Klein four group. However as I have read on, I am ...
0
votes
1answer
208 views

The Abstraction of Equality [closed]

In finitely presented groups, we can define equivalence classes simply by writing equations in the generators : $abc=d$. In this equivalence class we find elements like this $a(aa^{-1})bc$. We can ...
35
votes
2answers
1k views

Defining $SU(n)$ in HoTT

From a recent answer by Mike Shulman, I read: "HoTT is (among other things) a foundational theory, on roughly the same ontological level as ZFC, whose basic objects can be regarded as $\infty$-...
46
votes
7answers
5k views

In what respect are univalent foundations “better” than set theory?

It was an ambitious project of Vladimir Voevodsky's to provide new foundations for mathematics with univalent foundations (UF) to eventually replace set theory (ST). Part of what makes ST so ...
2
votes
0answers
80 views

Constructing the Von Neuman Hierarchy at ω+ω in a structural set theory

I'm working in SEAR which is a relatively new structural set theory, and I am trying to prove the existence of big sets. SEAR has the collection axiom which is, loosely speaking, that for every ...
7
votes
1answer
536 views

Category theory without axiom of choice

I'm looking for references on the development of (some of) Category theory without the axiom of choice. One possible axiom system (that, to me, seems the natural setting) is ZF + there are arbitrarily ...
14
votes
3answers
935 views

History of the abstract method in mathematics

Recently I have "finished" a 13-year on and off research on the history of the mathematical notion of equivalence. At the end of which, I learned that we owe the nowadays rather elementary process of "...
5
votes
1answer
226 views

What drawbacks are there to using NF(U) for category theory?

In category theory, you often run into what is known as "size" issues. That is, you run into the issue that the categories you try to define are too "big" to be sets, and so you need to use classes or ...
17
votes
3answers
788 views

Large categories vs. $\mathrm{U}$-categories: why is the loss of category-theoretic information inessential?

I've asked a related question about nine months ago here, however, apparently, I lacked expertise to ask the precise question I want to ask here, as I wish to revisit the matter of universes. I hope ...
2
votes
1answer
252 views

Why are types in type theory unordered collections?

Please excuse my naïveté, I have no higher math education, just a curious observer. In type theories, types are treated as set-like because they're unordered collections. Yet, the putative motive in ...
6
votes
2answers
377 views

Are omega-consistent extensions of PA always consistent with each other?

The question is as in the title. In the edit history you can find my attempt to formalise the question, but that was a failure, for reasons stated clearly in the comments. Thus, my question is just: ...
2
votes
1answer
248 views

Anti-foundational set theory with a universal set

There are alternative set theories that allow for a universal set, e.g. NF(U), positive set theory and and topological set theory. There are also alternative set theories like ZFA that allow for the ...
7
votes
1answer
274 views

Can ETCC/ETCS talk about 'size issues'?

In material set theories (like ZFC), one can prove that there is no set of all sets. Can one prove a similar statement in ETCS? This exact statement "there is no set x such that y in x for every set y"...
7
votes
1answer
454 views

Does equality between sets contradict the philosophy behind structural set theory?

Zermelo-Fraenkel set theory (with choice) is commonly accepted as the standard foundation of mathematics. It is a material set theory. This means that for every two objects/sets $a,b$ one can ask ...
2
votes
0answers
128 views

Is there equality between sets in structural set theory?

In material set theory, the axiom of extensionality defines equality between sets: two sets are equal iff they have the same elements. In structural set theory, one cannot formulate this. But however,...
9
votes
1answer
450 views

How are material set theory and structural set theory related from the point of view of category theory?

In his comments to both cody and Nik Weaver regarding his answer to user7280899's mathoverflow question "What kind of foundation are mathematicians using when proving metatheorems?", Mike Shulman ...
17
votes
2answers
1k views

Which kind of foundation are mathematicians using when proving metatheorems?

Zermelo-Fraenkel set theory (with choice) is commonly accepted as the standard foundation of mathematics. It is a material set theory. For every two objects/sets $a,b$ one can ask whether $a=b$ or not....
11
votes
0answers
189 views

How much can “(recursively) large ordinal axioms” prove?

In "Collapsing functions based on recursively large ordinals: A well–ordering proof for KPM", Michael Rathjen shows that certain notations for the proof-theoretic ordinals of theories, which ...
5
votes
0answers
302 views

Did Kleene constructively prove Brouwer's axioms?

Harvey Friedman's request on the FoM-forum for an overview of current intuitionistic foundations revived the following question, which I have been meaning to ask for five years. (I'm no expert on ...
1
vote
0answers
187 views

What should one know about abstract sets and structural foundations?

Recently I came by accident across the book sets for mathematics by Lawvere. It says: First we deplete the object of nearly all content. We could think of an idealized computer memory bank that ...
2
votes
1answer
297 views

Is the statement “All numbers are counting numbers” independent of $PA$?

In his paper, "Completed versus Incomplete Infinity in Arithmetic" (look under "www.math.princeton.edu/$\sim$nelson/papers.html" under the subheading "Infinity"), the late Edward Nelson defines the ...
2
votes
2answers
392 views

What is the largest cardinal consistent with $ZFC$ + $V$=$L$?

What is the largest cardinal consistent with $ZFC$ + $V$=$L$? The reason for the question is this: under the assumption that all of 'ordinary mathematics' (as reverse mathematics understands the ...
19
votes
3answers
1k views

Why would the category of sets be intuitionistic?

This question is probably really naive. And, I hope the title doesn't come off as too combative. I think that topoi of $\mathbf{Set}$-valued sheaves provide an excellent motivation for higher-order ...
50
votes
10answers
7k views

How should a “working mathematician” think about sets? (ZFC, category theory, urelements)

Note that "a working mathematician" is probably not the best choice of words, it's supposed to mean "someone who needs the theory for applications rather than for its own sake". Think about it as a ...
9
votes
2answers
895 views

Meta-undecidability

Could there be an undecidable statement $S$ in ${\sf ZFC}$ of which one will never be able to prove its undecidability for principal reasons (ie we will never know that $S$ is undecidable)? If this ...
17
votes
6answers
2k views

What is some current research going on in foundations about?

What is some current research going on in the foundations of mathematics about? Are the foundations of mathematics still a research area, or is everything solved? When I think about foundations I'm ...
16
votes
2answers
2k views

Do set theorists work in T?

In the thread Set theories without "junk" theorems?, Blass describes the theory T in which mathematicians generally reason as follows: Mathematicians generally reason in a theory T which (...
4
votes
1answer
425 views

Are the paradoxes of material or strict implication used anywhere to prove theorems in mathematics

In the Stanford Encyclopedia of Philosophy entry "Relevance Logic", the following inference is listed as classically valid: The moon is made of green cheese. Therefore, it is raining in Ecuador ...
0
votes
1answer
313 views

“Co-ordinate-free” mathematics for general structures? [closed]

Edit (15 November 2017): I've just stumbled across this question, which I think is asking essentially the same thing I tried to ask below, but probably worded it more clearly - and got far more ...
3
votes
3answers
491 views

Is a paraconsistent and provably non-trivial foundation for math possible?

Would it be possible to use a paraconsistent logic and axioms similar to ZFC to create a formal sytem, that can be proven to be non-trivial (so that there are some statements which can´t be proven in ...
0
votes
1answer
419 views

Why do we try to encode every mathematical object as a set? [closed]

Probably everyone of us has seen set-theoretic encodings of mathematical objects which we wouldn't naturally consider to be sets. May it be the "definition" of a function from $A$ to $B$ as a relation ...