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
7 votes
0 answers
96 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
165 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
243 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 ...
discretizer's user avatar
2 votes
1 answer
56 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
  • 269
22 votes
2 answers
997 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
277 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
207 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,671
6 votes
0 answers
138 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
  • 38.7k
6 votes
1 answer
809 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
5 votes
2 answers
381 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
  • 269
2 votes
0 answers
63 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
  • 38.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
7 votes
1 answer
159 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
91 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
55 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
  • 38.7k
9 votes
1 answer
358 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
  • 38.7k
2 votes
1 answer
345 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
7 votes
1 answer
252 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,733
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 ...
5 votes
0 answers
78 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
  • 38.7k
6 votes
1 answer
255 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
  • 38.7k
14 votes
0 answers
271 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
  • 38.7k
5 votes
1 answer
147 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,671
-6 votes
1 answer
268 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
339 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
41 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
100 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
3 votes
0 answers
231 views

Principle of unique choice in homotopy type theory

In the MathOverflow thread Mathematics without the principle of unique choice, Mike Shulman defines the principle of unique choice to be if $R$ is a relation between two sets $A$, $B$, and for every $...
Madeleine Birchfield's user avatar
1 vote
0 answers
116 views

What is the proof theoretic ordinal of this kind of predicative type-set theory?

The following is a kind of Predicative Type Set Theory. The question is about what is exactly the proof theoretic ordinal of this theory? Is it lower than the one expected for predicative theories, i....
Zuhair Al-Johar's user avatar
6 votes
1 answer
347 views

Joyal arithmetic universes and the Box operator

Last month @godelian, alias Christian Espíndola, in a FOM post has mentioned Joyal's proof of Godel's second incompleteness via the so-called Arithmetic Universes, introduced by Joyal around 1973, ...
Mirco A. Mannucci's user avatar
1 vote
0 answers
103 views

Can this type theory interpret second order arithmetic?

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

Is definability in $V$ in $\sf Ack+MK$ expressible in its language?

Recall Ackermann set theory. If we extend Ackermann's set theory by adding all axioms of $\sf MK$ to it. We shall denote the universe of all elements by $W$, while $V$ is the primitive constant symbol ...
Zuhair Al-Johar's user avatar
7 votes
2 answers
564 views

Consistency strength of an attempt at higher order set theory

Work in a theory with (deep breath) a countable number of primitives denoted with capital letters from the end of the alphabet with numerical subscripts $\{X_n,Y_n,Z_n,\dots\}_{n<\omega}$ ...
Alec Rhea's user avatar
  • 8,294
1 vote
0 answers
191 views

Can Frege set extensions of second order unary predicates serve as a foundation for mathematics?

To second order logic, add a primitive partial one place function symbol "$\epsilon$" from unary predicate symbols [upper cases] to object symbols [lower cases]. Define: $ x=y \equiv_{df} \...
Zuhair Al-Johar's user avatar
2 votes
0 answers
217 views

A formal definition of a useful theorem?

Sorry if this feels a bit squishy, but I'm wondering if there is any published work trying to give a fully formal definition of the notion of a useful theorem. I mean, in mathematics we all know that ...
Peter Gerdes's user avatar
  • 2,261
6 votes
1 answer
764 views

An axiomatic approach to the multiverse of sets

Work in a theory where the primitives are classes $X,Y,Z,\dots$, and class membership $X\in Y$, and add an individual constant $\mathcal{M}$ called 'the multiverse'. Classes $V$ which are members of ...
Alec Rhea's user avatar
  • 8,294
10 votes
2 answers
372 views

Is there a purely constructive presentation of the HK integral?

Treating the Riemann integral in a constructive setting is easy and straightforward. Treating the closely related but much more powerful Henstock-Kurzweil integral constructively is almost easy, ...
saolof's user avatar
  • 1,733
4 votes
1 answer
285 views

Consistency of Generalised Continuum Hypothesis and univalence in HoTT

In homotopy type theory, propositional excluded middle and the axiom of choice sets are both consistent with univalence, both of which yields type theoretic models for classical mathematics. However, ...
user avatar
0 votes
0 answers
67 views

'Maximising interpretative power entails maximising consistency strength'?

I'm hoping there is a clear mathematical answer to this question (hence asking it here) rather than anything more exegetical (in which case it's presumably not appropriate for this site). In his paper ...
aidangallagher4's user avatar
25 votes
1 answer
1k views

Coinduction for all?

Every undergraduate in mathematics learns about proofs by mathematical induction. Moreover, every undergraduate taking a course in theoretical computer science or logic learns about inductive ...
user984603's user avatar
4 votes
1 answer
350 views

Homotopical realizability

After a long story of dancing around the effective topos $ \mathcal{Eff}$, I finally resolved to get to the bottom of it. To this effect, working as it were backward, I ended up revisiting Kleene's ...
Mirco A. Mannucci's user avatar
13 votes
0 answers
368 views

The free complete lattice on three generators, beyond ZF

This was originally asked at MSE; although it is still under bounty it seems unlikely to be answered there. $\mathsf{ZF}$ proves that there is no free complete lattice on three generators since any ...
Noah Schweber's user avatar
12 votes
0 answers
479 views

Harvey Friedman's minimalist axioms for set theory

[This is a question on the FOM mailing list.] In 1997, Harvey Friedman introduced the following theory: Let $\in$ be a binary predicate and $U$ be a constant. Add the following axioms: Subworld ...
user76284's user avatar
  • 1,671
1 vote
0 answers
181 views

Does foundationless Ackermann set theory prove replacement?

From Ackermann's set theory equals ZF (1970) by William N. Reinhardt: Let A be the theory determined by the following axioms: Extensionality: $\forall z (z \in x \leftrightarrow z \in y) \to x = y$ ...
user76284's user avatar
  • 1,671
2 votes
0 answers
156 views

Can we interpret ZFC in GEM?

I have long held similar views as put forth here. As professor Hamkins points out though, $(M,\subseteq)$ is insufficient to model most of mathematics. However, this is unsatisfactory to me, as this ...
tox123's user avatar
  • 392
3 votes
1 answer
167 views

0-valued and 1-valued logics?

In addition to classic two-valued logic, there are many many-valued logics, including Łukasiewicz's and Kleene's three-valued logics, Gödel's many-valued logic $G_k$, and infinite-valued fuzzy logic ...
rtsss's user avatar
  • 477
7 votes
1 answer
361 views

Does the small object argument need replacement?

Does one need the axiom of replacement in the small object argument and in the transfinite construction of free algebras? My motivation for the question is that I heard that the axiom of replacement ...
user333306's user avatar
13 votes
0 answers
353 views

Context of set theory in which one doesn't have to worry about size issues

In this beautiful talk by Colin McLarty, McLarty quotes Grothendieck: It would be nice to have a context where one doesn't add any real axioms to set theory, and yet one can work with categories ...
user333306's user avatar
6 votes
1 answer
437 views

What do you call the generalisation of the direct image?

This question was posted on Math Stack Exchange, but did not attract an answer. Here is the question: Informal Description Let me start with an example. Let $X$ be the set $\{a, b, c, d, e\}$ and $E$ ...
Yes's user avatar
  • 105

1
2 3 4 5 6