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
-3 votes
0 answers
208 views

Are there known examples like this almost official exposition of ZFC that is very weak?

Pseudo-ZFC is a theory written in the usual language of set theory, i.e. mono-sorted first order logic with equality and membership. The extra-logical axioms are: Extensionality: $\forall x \forall y:...
Zuhair Al-Johar's user avatar
2 votes
1 answer
173 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
171 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
333 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
282 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
87 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
5 votes
1 answer
252 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
188 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
255 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,793
7 votes
3 answers
425 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
312 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
  • 8,947
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
5 votes
0 answers
180 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
274 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
229 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
949 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,140
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
  • 8,947
1 vote
0 answers
90 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
118 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
136 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
247 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
311 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
2 votes
0 answers
256 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,793
6 votes
0 answers
146 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
  • 40.7k
6 votes
1 answer
840 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
462 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
64 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
  • 40.7k
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
223 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
109 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
63 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
  • 40.7k
9 votes
1 answer
367 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
  • 40.7k
3 votes
1 answer
411 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
283 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,823
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
101 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
  • 40.7k
6 votes
1 answer
269 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
  • 40.7k
16 votes
1 answer
476 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
  • 40.7k
5 votes
1 answer
165 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,793
-6 votes
1 answer
364 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
2 votes
1 answer
477 views

Higher inductive types in higher observational type theory

Mike Shulman gave the following set of talks on higher observational type theory earlier this year (part 1, part 2, part 3). However, while he talked about how the identity types are defined and ...
Madeleine Birchfield's user avatar
1 vote
0 answers
51 views

What is the consistency strength of this addition on simple type-set theory?

Language: multi-sorted first order logic with equality and membership, where for each natural $n$ there is a set $x^n$ of sort $n$. Equality "$=$" only occurs between variables of the same ...
Zuhair Al-Johar's user avatar
1 vote
0 answers
117 views

Is $\sf \Gamma_0$ the proof theoretic ordinal of this kind of predicative class theory?

Adopting the approach of Mono-sorted $\sf NBG$, define sets as elements of classes, then axiomatize: Extensionality, Predicative Class comprehension, emptyset, in the usual manner along mono-sorted $\...
Zuhair Al-Johar's user avatar
22 votes
5 answers
2k views

Axiomatic construction of trigonometric functions

I am able to construct functions $\sin,\cos\colon \mathbb R \to \mathbb R$ satisfying the following properties: $\sin^2 x + \cos^2 x = 1$, $\sin(x+y)=\sin x \cos y + \sin y\cos x$, $\cos(x+y)=\cos x \...
Emanuele Paolini's user avatar

1
2 3 4 5
7