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.
311
questions
-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:...
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$;
$\...
-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 ...
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)$ ...
-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 ...
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 ...
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 ...
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 ...
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 $\...
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 . \...
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 ...
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
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-...
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 ...
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 ...
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. ...
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....
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 ...
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
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 ...
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 ...
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 $\...
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 ...
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
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 ...
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 ...
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$ ...
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?
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_{...
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 ...
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
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 ...
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 ...
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 ...
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\...
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 (...
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 ...
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$ ...
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}...
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, ...
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$
...
-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 ...
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 ...
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 ...
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 $\...
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 \...