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.
350 questions
4 votes
2 answers
423 views
Can custom functions be defined in Peano Arithmetic or the language of First-order Arithmetic?
Can we specify custom recursively-defined functions in the language of First-order Arithmetic? I know that we can define functions in Second-order Arithmetic ($Z_2$). For example, we could define ...
- 183
33 votes
1 answer
2k views
What is the consistency strength of Russell & Whitehead's ‘Principia Mathematica’?
Russell and Whitehead's Principia Mathematica is of mostly historical interest (e.g., in that Gödel's incompleteness theorem was originally formulated against it), and I must admit never having read ...
- 38.1k
8 votes
1 answer
583 views
Measurable cardinals and $HOD$
Let $\kappa$ be some measurable cardinal and let $j:V \rightarrow M \cong Ult_U(V)$ be the canonical embedding with critical point $\kappa$ for some $\kappa$-complete non principal normal ultrafilter ...
- 183
13 votes
2 answers
768 views
Universal delta-functors and ZFC
I am certainly not an expert in foundations, although when I see some mathematics I usually feel like I would be able to formally write it down in theory in a formal system like ZFC or Lean's ...
- 42.1k
8 votes
1 answer
676 views
Are Mike Shulman's "stack semantics" complete?
In Shulman's Stack semantics and the comparison of material and structural set theories, he defines the stack semantics for a Heyting pretopos. He notes that (1) the stack semantics validate the ...
- 467
-2 votes
1 answer
535 views
Is this theory of bottomless hierarchy, consistent?
Language: mono-sorted ${\sf FOL}(=,\in,S)$, where $S$ is a unary predicate standing for ".. is a stage". Axioms: Extensionality: $\forall z \, (z \in x \leftrightarrow z \in y) \to x=y$ ...
- 13k
-4 votes
2 answers
368 views
Formal theory of structure [closed]
I use the concept of structure in my physics research. In particular, I would say things like "We probe structure with functors into a local structured system as a category", or "the ...
- 1,289
8 votes
1 answer
549 views
In praise of Replacement, type-theoretically
A type-theoretic version of replacement says that given a set $A$ in a universe $U$, and another set $B$ with no universe constraints, the image of any function $A \to B$ is essentially in $U$. (Let ...
- 2,166
20 votes
3 answers
2k views
Ordinary mathematics intrinsically requiring unbounded replacement/specification?
Encouraged by some users on MO, I'm going to ask this question that I have had for years. I have always felt that the iterative conception of sets makes some sense for justifying BZFC (i.e. ZFC with ...
- 3,122
2 votes
0 answers
154 views
A special name for Hilbert's Axiom I.7?
The famous Hilbert's Axioms of Geometry include the Axiom I.7: If two planes have a common point, then they have another common point. Question 1. Was David Hilbert the first mathematician who ...
- 44.2k
2 votes
0 answers
105 views
Can this salvage Cyclic Stratified Comprehension?
This is an endeavor to salvage the approach presented at earlier posting. Is there a clear inconsistency with this axiom schema? Cyclic Stratified Comprehension: if $\varphi$ is a stratified formula ...
- 13k
6 votes
1 answer
606 views
A form of reverse mathematics that works with hereditarily finite sets instead of numbers
Does anyone know of any texts where reverse mathematics is developed using hereditarily finite sets and subsets of $V_\omega$? Reverse mathematics is typically carried out in the framework of second-...
1 vote
1 answer
519 views
Why not begin studying sets with Hierarchy Theory?
By $\sf HT^\psi$ I mean the Hierarchy Theory of $\psi$ height. This is a set theory written in mono-sorted first order logic with equality and membership, with the following axioms: Specification: $\...
- 13k
3 votes
0 answers
252 views
Can this extension of ZC evade having distinct bi-interpretable extensions?
What property should an extension of $\sf ZC$ have in order for it to evade having distinct yet bi-interpretable extensions. Which might be seen as a merit by some, foundationally speaking. Is ...
- 13k
12 votes
0 answers
316 views
Realizability ∞-topos
This is my first question on MathOverflow, so it is possible it is poorly composed. My interests lie in the field of the type theory and (higher) category theory, specifically I am interested in the ...
- 121
0 votes
0 answers
174 views
Higher-Order Analogues of Gödel’s First Incompleteness Theorem
I was playing with ideas around Gödel’s first incompleteness theorem which, roughly speaking, says that for every ($\omega$-)consistent, recursively axiomatizable formal system $F$ that is ...
- 137
0 votes
0 answers
317 views
A monad-style proof that Set is the right place to have a presentation of The Theory of Categories
When I attended my first Category Theory class, I asked the professor the following question. "It seems you are giving a presentation of the theory of categories IN set. Can you elaborate on ...
- 1,289
0 votes
0 answers
95 views
Can Singleton augmented Mereology provide a truth argument for set theory?
Let "$ \phi \text { is one-to-one between } \pi, \psi $", stands for meeting both of: $$ \forall x \pi(x) \exists!y \psi(y): \phi(x,y) \\ \forall y \psi(y) \exists!x \pi(x): \phi(x,y) $...
- 13k
14 votes
2 answers
2k views
Why are quotients so much trickier in constructive type theory than in constructive set theory?
Quotients in constructive type theory are a bit of a pain. My understanding is that the first type theory that supported them well was cubical type theory, and in previous type theories the ...
- 7,128
10 votes
2 answers
744 views
What's the deal with predicative foundations?
The working mathematician and layperson's reasons for caring about constructive foundations are well-documented. Topos theory, in particular, gives an abundance of examples in nature of settings where ...
- 551
9 votes
1 answer
406 views
Formalizing Cantorian finitism
Section 1.5 of [1] describes "Cantorian finitism" (CF) as the "rule of thumb" that "infinite sets are like finite ones". My questions are the following: Is it possible ...
- 2,440
2 votes
0 answers
125 views
How strong is separation + reflection without transitivity?
Consider a theory $T$ with a binary relation $\in$ and the following axiom schemas: $\exists u \forall x (x \in u \leftrightarrow x \in a \land \phi)$ where $u$ is not free in $\phi$. This is the ...
- 2,440
15 votes
0 answers
469 views
Can the axiom of choice be expressed in 4 quantifiers?
This 2007 paper presents a 5-quantifier $(\in, =)$-expression that is ZF-equivalent to the axiom of choice, but leaves open the 4-quantifier case: Thus the gap is reduced to the undecided case of a 4 ...
- 2,440
12 votes
1 answer
309 views
Is there a $\Pi_2$ sentence $A$ such that $\text{ZFC}^- + A$ proves powerset?
This is a follow-up to this question. Let $\text{ZFC}^-$ be ZFC without powerset and with collection rather than replacement, as described here. Is there a $\Pi_2$ (or perhaps $\Sigma_2$) sentence $A$ ...
- 2,440
7 votes
2 answers
512 views
Set theoretical foundations for derived categories
A modern approach to derived functors, that has been shown to be useful in a number of different circumstances, is that of a derived category (see the book by Yakutieli, for example, here). However, ...
- 3,758
16 votes
2 answers
1k views
CH in non-set theoretic foundations
I asked this question on stack exchange and got little attention, barring a nice example I intend to look into. The original post can be found here: https://math.stackexchange.com/q/4941233/1053681 I ...
- 261
13 votes
1 answer
1k views
Consistency strength of HoTT
What is the consistency strength of Homotopy type theory (HoTT) relative to various set theories (e.g., are there any known set theories that it can interpret)? Does this question even make sense?
- 5,493
8 votes
0 answers
206 views
How to define Dedekind reals and Eudoxus reals such that they are equivalent to unmodulated Cauchy reals
In constructive mathematics without choice, we have three different versions of the real numbers (each embedding into the next). Regular Cauchy reals (functions $f : \mathbb N \to \mathbb Q$ such ...
- 7,128
25 votes
2 answers
3k views
Foundations and contradictions of Scholze's work: the category of presentable infinity categories contains itself
Preface: I am not an expert in the work of Scholze, or anything for that matter. Question Has Scholze stated what axioms he is using to develop his theory of motives and analytic geometry. In the ...
- 485
3 votes
1 answer
322 views
Can these short set-building expressions of the finite set world extend to the infinite set world?
A formula of the form $\forall \vec{p}\, \exists x \, \forall y\, (y \in x \leftrightarrow \phi(y,\vec{p}))$ is to be named a "set-building" formula. Now, when $\vec{p}$ includes a predicate ...
- 13k
15 votes
2 answers
2k views
Type vs. Set Theory: Expressive Ability
In the modern mathematical arena, the two primary contenders for the ‘correct’ foundation of mathematics are set and type theory. Set theory, very roughly, captures the intuition that we frequently ...
- 10.4k
10 votes
2 answers
489 views
How big can function spaces get without extensionality?
In what follows we work in the usual formulation of Martin-Löf Type Theory including Axiom K [1]. Boldface numbers $\mathbf{n}$ denote the usual finite type with $n$ elements. Motivation Postulating ...
- 783
5 votes
3 answers
842 views
Negating fundamental axioms
It is commonplace to consider standard axiomatic systems (e.g. $ZF$) with one of the 'less essential' axioms negated, like infinity, 'less essential' here having some ambiguous definition related to ...
- 10.4k
8 votes
2 answers
673 views
Completing half of Hilbert's program: Foundations that are conservative over Peano Arithmetic
The goal of the Hilbert program was to find a complete and consistent formalization of mathematics. Gödel's first incompleteness theorem establishes that completeness is impossible with first-order ...
- 7,128
31 votes
3 answers
3k views
Are there substantive differences between the different approaches to "size issues" in category theory?
In category theory, there are different ways to approach the "size issues" that crop up when we try to formalise the subject in axiomatic set theory. As far as I can tell, there are two main ...
- 1,538
4 votes
0 answers
229 views
Recording of 2009 lecture on Harvey Friedman's work
On December 13--20 2009 at Bristol, there was a meeting devoted to thorough dissection of Harvey Friedman's work on the foundations of mathematics and his statements claimed to be equivalent to ...
- 2,858
2 votes
0 answers
253 views
Which is richer Set or Graph Theory?
This theory about structures, defined as abstractions over isomorphic graphs, can interpret Set Theory in a rather creepy manner. Though the theory is largely technical, yet it is not far from being ...
- 13k
12 votes
3 answers
3k views
What governs our "perception?" about the platonic realm of sets?
Here, I want to delve into what do we exactly feel about what constitutes a platonic existence of a set? Or what makes us think or actually a kind of feel or sense the existence of a set in the ...
- 13k
5 votes
1 answer
747 views
The "first-order theory of the second-order theory of $\mathrm{ZFC}$"
$\newcommand\ZFC{\mathrm{ZFC}}\DeclareMathOperator\Con{Con}$It is often interesting to look at the theory of all first-order statements that are true in some second-order theory, giving us things like ...
- 5,005
4 votes
1 answer
759 views
Why not $\sf ZFC+[V=HOD]$?
Why not $\sf ZFC+[V=HOD]$ as the standard set theory? It implies the existence of a definable global choice and well-order, and it is compatible with all large cardinal axioms extending $\sf ZFC$, so ...
- 13k
2 votes
1 answer
249 views
Does inductive definitions must be supported by the set theoretical definition of natural numbers?
In page 4 of Gödel's book The Consistency Of The Axiom Of Choice and Of The Generalized Continuum Hypothesis With The Axioms Of Set Theory, Gödel defined the $n$-tuple as $\langle x \rangle = x$; $\...
- 115
-4 votes
1 answer
250 views
Is Bounding Reflection consistent?
Working in the first order language of set theory. Let $\varphi^{*B}$ be the formula obtained from $\varphi$ by merely bounding all open quantifiers in $\varphi$ by the symbol "$B$". Here a ...
- 13k
4 votes
1 answer
402 views
What is the proof of consistency of anterior reflection?
Let Anterior Reflection be the following principle: $$\forall \vec{v}~ \exists X: \operatorname {transitive} (X) \land \, (\varphi \to \varphi^{X"}) $$ where $\varphi$ is a formula in $\sf FOL(=,\in)$ ...
- 13k
-3 votes
1 answer
351 views
Can this form of reflection be consistent?
Is this form of reflection consistent? First I'll begin by clarifying the notation I'm using here: By a quantifier being relativized or bounded it means that the first occurrence of the quantified ...
- 13k
3 votes
1 answer
128 views
Is this form of replacement suitable for ZF - Powerset + well-ordering principle?
The following scheme can be understood as a form of replacement. Axiomatizing $\sf ZF$ with it instead of the usual replacement schema renders it immune to removal of extensionality; see here. In an ...
- 13k
18 votes
3 answers
3k views
What's the earliest result (outside of logic) that cannot be proven constructively?
Although mathematicians usually do not work in constructive mathematics per se, their results often are constructively valid (even if the original proof isn't). An obvious counter-example is the law ...
- 7,128
6 votes
1 answer
393 views
Is univalence equivalent to every type function being a functor over equivalence?
Introduce a rule in type theory that if $\Gamma \vdash f : \text{Type} \to \text{Type}$ and $\Gamma \vdash e : A \simeq B$ then $\Gamma \vdash f[e] : f(A) \simeq f(B)$. It may seem like such a rule is ...
- 7,128
12 votes
0 answers
254 views
Are there times when replacement is "more natural" than collection?
There are a couple examples I'm aware of where choosing to axiomatize $\mathsf{ZF(C)}$ using collection instead of replacement results in a much nicer (or at least less surprising) picture: Let $\...
- 19.5k
6 votes
1 answer
476 views
Bounded alternatives to powerset that interpret ZFC
In set theory, many properties/relations of interest can be expressed as $\Delta_0$ formulas (formulas with only bounded quantifiers): \begin{align} \text{empty}(a) &\equiv \forall x \in a . \...
- 2,440
7 votes
3 answers
585 views
How much Dependent Choice is provable in $Z_2$? And what about Projective Determinacy?
So, second order arithmetic, $Z_2$, is capable of proving quite a few things. One thing which would be of use is dependent choice for $\mathbb{R}$. Basically, dependent choice on $\mathbb{R}$ says ...
- 353