Skip to main content

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.

Filter by
Sorted by
Tagged with
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 ...
Zuhair Al-Johar's user avatar
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, ...
Municipal-Chinook-7's user avatar
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 ...
Zuhair Al-Johar's user avatar
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 ...
Mike Battaglia's user avatar
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 ...
Zuhair Al-Johar's user avatar
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$; $\...
Wenchuan Zhao's user avatar
-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 ...
Zuhair Al-Johar's user avatar
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)$ ...
Zuhair Al-Johar's user avatar
-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 ...
Zuhair Al-Johar's user avatar
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 ...
Zuhair Al-Johar's user avatar
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 ...
Christopher King's user avatar
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 ...
Christopher King's user avatar
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 $\...
Noah Schweber's user avatar
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 . \...
user76284's user avatar
  • 1,803
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 ...
Alex Appel's user avatar
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. ...
Bugs Bunny's user avatar
  • 12.1k
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-...
Alec Rhea's user avatar
  • 9,047
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 ...
Martin Brandenburg's user avatar
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 ...
Arshak Aivazian's user avatar
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. ...
Arshak Aivazian's user avatar
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....
parallelogram's user avatar
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 ...
truebaran's user avatar
  • 9,180
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 ...
Someone211's user avatar
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 ...
Alec Rhea's user avatar
  • 9,047
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 ...
Keshav Srinivasan's user avatar
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 ...
Darren Li's user avatar
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 $\...
Robin Saunders's user avatar
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 ...
Keshav Srinivasan's user avatar
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 ...
Y.Z.'s user avatar
  • 231
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 ...
ViHdzP's user avatar
  • 281
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 ...
LOCOAS's user avatar
  • 363
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 ...
user76284's user avatar
  • 1,803
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$ ...
Taras Banakh's user avatar
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?
Carlos Freites's user avatar
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_{...
ViHdzP's user avatar
  • 281
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 ...
Taras Banakh's user avatar
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 ...
LOCOAS's user avatar
  • 363
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 ...
Keshav Srinivasan's user avatar
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 ...
Kruppe's user avatar
  • 13
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 ...
Taras Banakh's user avatar
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\...
Taras Banakh's user avatar
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 (...
Arshak Aivazian's user avatar
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 ...
saolof's user avatar
  • 1,833
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$ ...
Taras Banakh's user avatar
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}...
Taras Banakh's user avatar
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, ...
Taras Banakh's user avatar
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$ ...
user76284's user avatar
  • 1,803
-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 ...
Frank Quinn's user avatar

1
2 3 4 5
7