Questions tagged [foundations]
Mathematical logic, Set theory, Peano arithmetic, Model theory, Proof theory, Recursion theory, Computability theory, Univalent foundations, Reverse mathematics, Frege foundation of arithmetic, Goedel's incompleteness and Mathematics, Structural set theory, Category theory, Type theory.
330 questions
6
votes
1
answer
993
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 $\...
user103598
47
votes
7
answers
7k
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) ...
- 48.8k
7
votes
2
answers
1k
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 ...
- 3,302
9
votes
1
answer
687
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 ...
- 4,897
12
votes
1
answer
1k
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,648
1
vote
0
answers
101
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, ...
- 121
0
votes
0
answers
96
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, ...
- 121
2
votes
0
answers
305
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 ...
- 11.3k
3
votes
0
answers
283
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 ...
- 31
4
votes
0
answers
215
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 ...
- 1,115
14
votes
1
answer
900
views
A peculiarity of Henkin's 1950 proof of completeness for higher order logic
My question concerns Henkin's original (1950) completeness proof in Completeness in the theory of types for classical higher order logic and type theory relative to so-called general models.
His 1950 ...
- 639
6
votes
3
answers
445
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{U}$,
...
- 1,115
12
votes
1
answer
601
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 ...
- 1,115
5
votes
2
answers
474
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 ...
- 1,115
5
votes
1
answer
309
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{...
- 1,586
5
votes
1
answer
470
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.
$(1)$...
- 1,115
7
votes
1
answer
665
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 \in I}$ ...
- 1,115
7
votes
3
answers
1k
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 ...
- 437
5
votes
3
answers
488
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 ...
- 9,720
28
votes
0
answers
2k
views
Is Feferman's unlimited category theory dead?
In 2013 Solomon Feferman in Foundations of unlimited category theory: what remains to be done (The Review of Symbolic Logic, 6 (2013) pp 6-15, link) laid out three desirable axioms for "...
- 1,446
30
votes
6
answers
3k
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$ ...
- 66.7k
16
votes
3
answers
1k
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 ...
- 21.3k
10
votes
1
answer
1k
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$ ...
- 209
15
votes
2
answers
1k
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 ...
- 21.3k
4
votes
0
answers
424
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 ...
- 773
-2
votes
1
answer
317
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 ...
- 11.3k
39
votes
7
answers
6k
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 ...
- 750
0
votes
1
answer
236
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 ...
- 1,313
36
votes
3
answers
2k
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$-...
- 43.2k
60
votes
7
answers
9k
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 appealing ...
2
votes
0
answers
92
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 ...
8
votes
1
answer
998
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 ...
- 773
13
votes
3
answers
2k
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 "...
- 2,437
6
votes
1
answer
375
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 ...
- 6,353
19
votes
3
answers
1k
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 ...
- 1,115
2
votes
1
answer
317
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 ...
- 233
6
votes
2
answers
998
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:
...
- 1,344
4
votes
2
answers
548
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 ...
- 1,228
8
votes
1
answer
403
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"...
- 81
8
votes
1
answer
1k
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 ...
- 89
2
votes
0
answers
150
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,...
- 21
9
votes
1
answer
1k
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 ...
- 6,132
19
votes
2
answers
2k
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....
user103598
17
votes
1
answer
390
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 ...
- 3,612
5
votes
0
answers
386
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,616
1
vote
0
answers
223
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
456
views
Is the statement "All numbers are counting numbers" independent of $PA$?
In his paper, "Completed versus Incomplete Infinity in Arithmetic" (which can be found here), the late Edward Nelson defines the notion of 'counting number' as follows:
0 is a counting ...
- 6,132
2
votes
3
answers
854
views
What is the largest large-cardinal hypothesis consistent with $ZFC + V=L$?
What is the largest large-cardinal hypothesis consistent with $ZFC + V=L$? The reason for the question is this: under the assumption that all of 'ordinary mathematics' (as reverse mathematics ...
- 6,132
23
votes
3
answers
2k
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 ...
- 3,793
55
votes
10
answers
11k
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 ...
- 1,115