The foundations tag has no usage guidance.

**3**

votes

**1**answer

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

**3**answers

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

**3**answers

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

**0**answers

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

**4**answers

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

**2**answers

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

**0**answers

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

**2**answers

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

**0**answers

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

**1**answer

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

**5**answers

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

**1**answer

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

**2**answers

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

**7**answers

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

**0**answers

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

**1**answer

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

**3**answers

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

**1**answer

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

**3**answers

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

**1**answer

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

**2**answers

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

**1**answer

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

**1**answer

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

**1**answer

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

**0**answers

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

**1**answer

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

**2**answers

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

**0**answers

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

**0**answers

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

**0**answers

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

**1**answer

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

**2**answers

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

**3**answers

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

**10**answers

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

**2**answers

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

**6**answers

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

**2**answers

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

**1**answer

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

**1**answer

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

**3**answers

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

**1**answer

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

**0**answers

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

**1**answer

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

**4**answers

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

**3**answers

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

**1**answer

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

**0**answers

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

**4**answers

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

**1**answer

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

**1**answer

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