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

315
questions

1
vote

0
answers

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

3
votes

0
answers

131
views

### Suitability of formal type theory for mathematical thinking (vs. traditional set theory)

Type theory has advantages over set theory for the (computer) formalisation of mathematics, but has anybody who does mathematics with pen and paper found proof assistants or automated theorem provers, ...

11
votes

3
answers

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

5
votes

1
answer

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

4
votes

1
answer

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

2
votes

1
answer

184
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$;
$\...

-4
votes

1
answer

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

5
votes

1
answer

337
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)$ ...

-3
votes

1
answer

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

3
votes

1
answer

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

18
votes

3
answers

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

6
votes

1
answer

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

12
votes

0
answers

197
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 $\...

4
votes

1
answer

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

7
votes

3
answers

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

11
votes

1
answer

1k
views

### Existence of skeletons in ZFC

Influenced by this question from a fellow lagomorph, I would like to get to the bottom of existence of a skeleton of a category. I want to stay in ZFC, so I do not assume the global axiom of choice. ...

3
votes

1
answer

319
views

### Second order theory of a real-closed field

It is well known that the first-order theory of any real-closed field is complete, and consequently not capable of interpreting the majority of modern mathematics.
Is this still true for the second-...

43
votes

4
answers

4k
views

### Lists as a foundation of mathematics

I am wondering if there is a foundation of mathematics where not sets or "set-like objects" (such as objects of a suitable topos as in ETCS) are the primitive notion, but rather lists. These ...

6
votes

0
answers

182
views

### Is Vopěnka's principle inherited by Grothendieck topoi?

I call the Vopěnka's principle:
Every subfunctor of an accessible functor is accessible
but other formulations (which may lose equivalence in weak contexts?) are also interesting to me.
If this is ...

6
votes

1
answer

283
views

### In HoTT with LEM, are sets and pointed sets the same thing?

The operations of adding and removing a point (where removing is a consideration of a subset of elements x such that $(x = *) \to 0$) implements the equivalence of these 1-types, as far as I can see. ...

7
votes

1
answer

241
views

### How did Szmielew prove that Pasch's axiom is a consequence of the circle axiom?

It is alleged that Szmielew proved that Pasch's axiom is a consequence of the circle axiom. The source is said to be
The Pasch axiom as a consequence of the circle axiom, Bull.Acad.Polon.Sci.Sér.Sci....

7
votes

1
answer

983
views

### Propositional calculus, first order theories, models, completeness

In the usual context of model theory one studies first order theories: the Gödel completeness theorem asserts that $\varphi$ is a theorem of a theory $T$ (i.e. $\varphi$ is provable from the axioms of ...

21
votes

4
answers

4k
views

### How much of the axiom of choice do you need in mathematics?

Say we have DC-λ where λ is some inaccessible cardinal. Is that enough to develop all of ordinary mathematics? If not, is there a strengthening that is but that nevertheless does not assume full ...

12
votes

3
answers

2k
views

### Real reverse mathematics

Standard mathematical developments, be they set theoretic, type theoretic, synthetic, etc. all follow the same basic pattern:
Lay out a language, assume some stuff in this language, then prove that ...

1
vote

0
answers

93
views

### What computable pseudo-ordinals are there with initial segment $\omega_1^{CK}(1+\eta+1)$?

The notion of a “computable pseudo-ordinal”, i.e. a computable linear order with no hyperarithmetical descending chains, is an old one going back to Stephen Kleene. Joe Harrison wrote the definitive ...

2
votes

0
answers

119
views

### Higher-order oracle computation of reals and axiom of constructibility

Certain real numbers can be approximated arbitrarily well by computable functions. If we introduce halting oracles, then more real numbers can be "computed", like Chaitin's constant or the ...

8
votes

0
answers

142
views

### How strong is exponentiation with only open induction? (Or: "how low can we go?")

Do the strongest theories currently known to be unconstrained by Tennenbaum's theorem ($IOpen$ and some modest extensions) remain so when augmented with a definition of exponentiation and axiom $\...

4
votes

0
answers

257
views

### What is the meaning and proof of Harvey Friedman’s ultrafinite incompleteness sentence?

On page 7 of his paper “Adventures in Incompleteness”, Harvey Friedman states the following:
IN ANY LONG ENOUGH SEQUENCE $x_1,...,x_n$ FROM $\{1,2,3\}$, SOME $(x_i,...,x_{2i})$ IS A SUBSEQUENCE OF ...

12
votes

0
answers

262
views

### Freiling's question

(I've asked this question at Math StackExchange here but haven't gotten any response, so I decided to take a shot here as well.)
In his paper "Axioms of Symmetry: Throwing Darts at the Real ...

2
votes

1
answer

64
views

### Infinite decreasing sequence for class relation without minimal elements

Let us assume $<$ is some class relation without minimal elements, meaning $\forall a, \exists b, b< a$. This means that for every $n\in\omega$, one can build a decreasing function $f$ with ...

22
votes

2
answers

1k
views

### Statements in differential geometry independent from ZFC

It is well known that some problems in functional analysis and in general topology are independent from ZFC: to name a few, Kaplansky's conjecture, the existence of outer automorphisms of the Calkin ...

3
votes

2
answers

316
views

### On the definition of small categories in SGA4

We assume ZFC+U.
A category is an ordered pair $(\operatorname{Ob} \mathcal{C},\operatorname{Mor} \mathcal{C},\operatorname{dom},\operatorname{codom},e,∘)$ of sets (not classes) and maps satifying ...

3
votes

1
answer

474
views

### Harvey Friedman: The expanding mind

In reference 1, Friedman writes:
I discuss my efforts concerning 3 crucial issues in the foundations of mathematics that are deeply connected with the great work of Kurt Gödel.
[...]
B. Are there ...

6
votes

0
answers

147
views

### Does every Tarski plane embed into a 3-dimensional Tarski space?

By a Tarski space I understand a mathematical structure $(X,B,\equiv)$ consisting of set $X$, a betweenness relation $B\subseteq X^3$ and a congruence relation ${\equiv}\subseteq X^2\times X^2$ ...

6
votes

1
answer

845
views

### Can the axiom of choice be proved with ZF+Tarski axiom?

Can choice be proved with ZF+Tarski axiom?

6
votes

2
answers

476
views

### Replacement axiom and the von Neumann hierarchy

Within ZFC, the von Neumann hierarchy consists of sets $V_\alpha$ indexed by ordinals, subject to the following conditions:
$V_0=\varnothing$.
$V_{\alpha+1}=\mathcal P(V_\alpha)$.
$V_\lambda=\bigcup_{...

2
votes

0
answers

65
views

### Is the centroid property equivalent to the middle line property of the triangle?

By a Tarski plane I understand a set $X$ endowed with a betweenness relation $\mathsf B\subseteq X^3$ and a congruence relation ${\equiv}\subseteq X^2\times X^2$ satisfying all Tarski axioms except ...

16
votes

2
answers

2k
views

### Why do we care about small sets?

I have been a user of category theory for a long time. I recently started studying a rigorous treatment of categories within ZFC+U. Then I become suspecting the effect of the smallness of sets.
We ...

6
votes

1
answer

231
views

### Does $\text{ACA}_0$ + True Arithmetic prove the well-foundedness of every recursive ordinal?

As discussed in Noah Schweber's answer to What is the proof-theoretic ordinal of true arithmetic?, it is somewhat ambiguous what “the proof-theoretic ordinal of True Arithmetic” might mean. In one ...

1
vote

1
answer

114
views

### Is it possible to set up multiple automorphisms over a structureless object inside single-sort defined category?

I was trying to understand the behaviour of the primitive equality (=) in the axiomatization of category, which takes morphisms as primitives and objects as derivatives in bijection to identity ...

3
votes

1
answer

64
views

### Comparing the areas of polygons via equidecomposability in the hyperbolic plane

It is well-known that in the Euclidean plane two simple polygons have the same area if and only if they are equidecomposable, i.e., can be decomposed into congruent triangles.
Question. Is an ...

9
votes

1
answer

368
views

### A name for a mathematical structure of geometric type

I am looking for (maybe existing) name for a mathematical structure $(X,\leqslant)$ consisting of a set $X$ and a transitive relation ${\leqslant}\subseteq X^2\times X^2$ such that $xx\leqslant yz\...

3
votes

1
answer

418
views

### Does the concept of a $\infty$-category have a natural definition in the $\infty$-world?

I start with a thesis: the natural notion of equality is additional data (paths/morphisms), not a binary relation (the fact that they exist). So, in particular, with such a constructivization (...

8
votes

1
answer

288
views

### For which Sheaf topoi is Brouwer's fan theorem true?

Brouwer's fan theorem is the standard result that the Cantor space is compact, or equivalently that the Cantor space viewed as a locale is spatial. Since it is a compactness result for a countable ...

7
votes

3
answers

3k
views

### Are the categories of sets, abelian groups, and commutative rings unique?

Are the categories of sets, abelian groups, and commutative rings unique? Independence results like the independence of the generalized continuum hypothesis, the Whitehead problem, and the global ...

6
votes

0
answers

104
views

### Does the Segment-Circle Axiom imply the Circle-Circle Axiom in a non-Euclidean Tarski plane?

By a Tarski plane I understand a mathematical structure $(X,B,\equiv)$ consisting of set $X$, a betweenness relation $B\subseteq X^3$ and a congruence relation ${\equiv}\subseteq X^2\times X^2$ ...

6
votes

1
answer

271
views

### The algebraic structure of a line in a (Tarski) plane

By a Tarski plane (resp. plane) I understand a mathematical structure $(X,B,\equiv)$ consisting of a set $X$, a ternary betweenness relation $B\subseteq X^3$ and the 4-ary congruence relation ${\equiv}...

16
votes

1
answer

498
views

### A textbook on foundations of geometry in spirit of Tarski

I am interested in a textbook for studying (and teaching) foundations of geometry in the spirit of Tarski. I know that there is a rather old German book [W. Schwabhäuser, W. Szmielew, A. Tarski, ...

5
votes

1
answer

167
views

### How strong is separation + reflection of unbounded quantifiers?

Consider a set theory with the following axioms:
separation: $\exists y \forall x (x \in y \leftrightarrow \phi \land x \in a)$ where $y$ is not free in $\phi$
reflection: $\phi \to \exists u \phi^u$
...

-6
votes

1
answer

375
views

### Is ZFC set theory a satisfactory foundation for mathematics?

The conventional wisdom seems to be that it is, but there are problematic mismatches. Some are well-known: the use of first-order logic, and the many different implementations of the axioms, neither ...