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

The tag has no usage guidance.

3
votes
1answer
117 views

Enhancing Grothendieck's universes and Grothendieck's axiom: Shulman-Feferman 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
732 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
396 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
789 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 ...
18
votes
4answers
845 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
330 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
181 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
556 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
363 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
5answers
2k 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
205 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
519 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
919 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
218 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
756 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
249 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
362 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
242 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
269 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
450 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
430 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
185 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
301 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
186 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
290 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
389 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
892 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
421 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
312 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
484 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
415 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 ...
0
votes
0answers
147 views

A universal framework for Game Theory?

Ever since the seminal work of Von Neumann and Morgestern Game Theory has grown into a formidable sector of pure and applied mathematics. There are all sorts of games: perfect information, ...
4
votes
1answer
423 views

HoTT without Funext, Univalence

Are there any models of Martin-Löf's intensional type theory in which univalence or function extensionality fails? In the HoTT book, axioms like $\mathsf{LEM}_{\infty}$ (in Section 3.4) are proved to ...
40
votes
4answers
3k views

Do set-theorists use informal set theory as their meta-theory when talking about models of ZFC?

Here, Noah Schweber writes the following: Most mathematics is not done in ZFC. Most mathematics, in fact, isn't done axiomatically at all: rather, we simply use propositions which seem "intuitively ...
2
votes
3answers
463 views

Compactness of existential second order logic and definability of certain quantifiers

It is known (as a slogan) that the "existential fragment of second-order logic (ESO) is compact". My first question is: (1) Is ESO compact for: (a) uncountable languages (b) languages with ...
6
votes
1answer
340 views

What do we call this quantifier (“binder”)?

There's a quantifier ("binder", whatever), call it $\alpha$, defined as follows: $\alpha x.\tau$ is the (usually infinite) expression obtained by applying the substitution $\{x \mapsto \tau\}$ to the ...
2
votes
0answers
228 views

About the limitation by size

This could be a big post, so I'll try to summarize my thoughts and divide them into several questions. When working in category theory, I used to choose the following definition. A category $C$ is ...
7
votes
4answers
660 views

Direct axiomatization of ordinal and cardinal numbers

Again, this question is related (**) to a previous one: in standard books on basic set theory, after stating the axioms of ZFC, ordinal numbers are introduced early on. Afterwards cardinals appear: ...
7
votes
1answer
576 views

Taller models of ZFC

This question is somewhat related to a previous one, where I asked for new forms of infinite beyond the cardinal hierarchy. Using forcing techniques, at least the ones I know of, one starts from a ...
1
vote
1answer
217 views

What restriction(s) of Goedel's primitive recursive functionals is (are) necessary and sufficient to prove the consistency of $PRA$

It is well known that one can use Goedel's primitive recursive functionals of finite type to prove the consistency of $PA$ (Peano Arithmetic). As such, one can certainly use them to prove the ...