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.

65 questions with no upvoted or accepted answers
Filter by
Sorted by
Tagged with
28 votes
0 answers
2k views

Is Feferman's unlimited category theory dead?

In 2013 Solomon Feferman in Foundations of unlimited category theory: what remains to be done (The Review of Symbolic Logic, 6 (2013) pp 6-15, link) laid out three desirable axioms for "...
ziggurism's user avatar
  • 1,436
19 votes
0 answers
693 views

The cofinality of $(\mathbb{N}^\kappa,\le)$ for uncountable $\kappa$?

For a partially ordered set $P$, a set $A\subseteq P$ is cofinal if for each element of $P$ there is a larger element in $A$. The cofinality of $P$, ${\rm cof}(P)$, is the minimal cardinality of a ...
Boaz Tsaban's user avatar
  • 3,104
17 votes
0 answers
434 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
13 votes
0 answers
355 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
12 votes
0 answers
191 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
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
12 votes
0 answers
531 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,793
11 votes
0 answers
339 views

Categorial foundations via "categories of algebras"

There are categorical foundations for mathematics axiomatizing the category of sets (Lawvere's ETCS), cartesian closed categories (type theory), and the category of spaces (homotopy type theory). ...
Ronald J. Zallman's user avatar
10 votes
1 answer
2k views

Order theory as a foundation of mathematics?

I know the followings kinds of formalization of mathematics: based on set theory (e.g. ZFC) based on type theory (e.g. the formalism of Coq proof assistant, as an advanced example) based on category ...
porton's user avatar
  • 739
9 votes
0 answers
245 views

Is there a notion analogous to separability but requiring definable rather than countable sets?

Among models of $\lambda$-calculus, some like the Bohm tree model have the property that every element is a directed sup of definable elements, whereas others like the $D_\infty$ and $P(\omega)$ ...
fritzo's user avatar
  • 221
9 votes
0 answers
939 views

Has anyone pursued Frege's idea of numbers as second-order concepts?

Gottlob Frege was a pivotal figure in the history of mathematical logic. He gave an analysis of numbers that proceeded along roughly the following lines, in his books "The Foundations of Arithmetic" (...
Keshav Srinivasan'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
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.8k
6 votes
0 answers
102 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.8k
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
5 votes
0 answers
234 views

Higher order arithmetic, hierarchies and proof theoretic ordinals

I asked this question on MSE some days ago but I have not received any answer so I have decided to post it here. I would like to consider a generalization of the notation $\Pi$ and $\Sigma$ used for ...
user115415's user avatar
5 votes
0 answers
259 views

Class theory of ZF-minus-Powerset as classical predicative system?

I've been thinking about some mathematics in weaker foundational systems a little bit, largely from a structural viewpoint, and with particular attention to classes. Some categories I've been keeping ...
David Roberts's user avatar
  • 33.8k
5 votes
0 answers
216 views

Are any formal systems based upon the idea of "iterated characterization pushing" currently in existence? If not, is anyone working on them?

I had an idea in regards to the design of formal systems with foundational aspirations. To convey the idea, let's talk a bit about the second-order Peano axioms. The way these axioms work, we have a ...
goblin GONE's user avatar
  • 3,693
5 votes
0 answers
379 views

Did Kleene constructively prove Brouwer's axioms?

Harvey Friedman's request on the FoM-forum for an overview of current intuitionistic foundations revived the following question, which I have been meaning to ask for five years. (I'm no expert on ...
Franka Waaldijk's user avatar
5 votes
0 answers
236 views

What useful admissible rules does ZFC have beyond the deduction theorem?

I'm interested in formal proof verification, and one of the surprisingly difficult parts of this is dealing with proofs by contradiction. The issue is that the final step of such proofs is typically "...
Alexander Smith's user avatar
5 votes
1 answer
383 views

What structure do all kinds of theories, models, interpretations, proofs and all that form?

This is a question about a structure that can be used to investigate all kind of structures that can be investigated. Many years ago with Joseph Gubeladze we discussed something similar but I only ...
მამუკა ჯიბლაძე's user avatar
4 votes
0 answers
248 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
4 votes
0 answers
297 views

Can this graph theory serve as a foundational theory of mathematics?

Working in mono-sorted first order logic, add primitives of equality and its axioms, set membership $\in$, a partial ternary relation $\to$ denoting is the direction from to, and at last a total unary ...
Zuhair Al-Johar's user avatar
4 votes
0 answers
138 views

Is well-pointedness the reason that the internal/external distinction seems not to apply to $\mathbf{Set}$?

When reasoning about the category of sets, we usually don't have to worry about the internal/external distinction. For example, if $f : X \rightarrow Y$ is a morphism of sets, then $f$ is either ...
goblin GONE's user avatar
  • 3,693
4 votes
0 answers
201 views

Formalization and set-theoretic issues in the definition a functor category

Universes are used in a category theory to handle size-issues. Assuming Grothendieck's axiom UA that every sets is contained in some universe there are two approaches to $U$-smallness given a ...
Jxt921's user avatar
  • 1,075
4 votes
0 answers
420 views

What are the requirements of a foundational theory?

There are multiple languages to describe all of mathematics, and there are some equivalences between them, some more successful then others. My question is can we describe some requirements (in some ...
Omer Rosler's user avatar
4 votes
0 answers
666 views

Is there a notion of "predicative given the real numbers"?

A definition is called impredicative if it involves quantification over a domain that contains the thing being defined. For instance, if you define hereditary property to be a property which applies ...
Keshav Srinivasan's user avatar
3 votes
0 answers
265 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
3 votes
0 answers
175 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
  • 416
3 votes
0 answers
275 views

What does second order set theory give us that is new?

There is a natural analogy between the theories PA and ZFC. See the linked question by Gro-Tsen here. Peano arithmetic (PA) is a first order approximation to the natural numbers. As is well known, ...
Pace Nielsen's user avatar
3 votes
0 answers
137 views

Hilb as a Colimit in the Category of Scott Complete Categories (foundations)

Here is a paper I found by Adamek that generalizes Domain theory into categories of categories called Scott Complete Categories. The category of Scott Complete categories is denoted SCC. For years, ...
Ben Sprott's user avatar
  • 1,281
3 votes
0 answers
821 views

What is the role of the (formalized) omega rule in Ramified Analysis?

In the 1960's, Feferman and Schutte did groundbreaking proof-theoretic work to find out the strength of predicative systems of second-order arithmetic. They used the ramified theory of types, a ...
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
2 votes
0 answers
257 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
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.8k
2 votes
0 answers
231 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,551
2 votes
0 answers
158 views

Why not replace reflection by bounded reflection in Muller's approach?

Bounded Reflection: If $\phi$ is a formula in the language of set theory [i.e.; $\small \sf FOL(=,\in)$], in which all and only symbols $``x,x_1,..,x_n"$ occur free, and $\phi^V$ is the formula ...
Zuhair Al-Johar's user avatar
2 votes
0 answers
300 views

Does this axiomatic system satisfy requirements for founding mathematics?

In this article, the author, F.A.Muller, suggests criteria for a founding theory of mathematics (pp:14-16). The author proposes $ARC$ Class Theory to embody these requirements. The motivation is ...
Zuhair Al-Johar's user avatar
2 votes
0 answers
92 views

Constructing the Von Neuman Hierarchy at ω+ω in a structural set theory

I'm working in SEAR which is a relatively new structural set theory, and I am trying to prove the existence of big sets. SEAR has the collection axiom which is, loosely speaking, that for every ...
Kile Kasmir Asmussen's user avatar
2 votes
0 answers
149 views

Is there equality between sets in structural set theory?

In material set theory, the axiom of extensionality defines equality between sets: two sets are equal iff they have the same elements. In structural set theory, one cannot formulate this. But however,...
user105099's user avatar
2 votes
0 answers
258 views

About the limitation by size

This could be a big post, so I'll try to summarize my thoughts and divide them into several questions. When working in category theory, I used to choose the following definition. A category $C$ is ...
C. Dubussy's user avatar
2 votes
0 answers
168 views

Some questions regarding an alteration of Grzegorczyk's theory of concatenation, $\operatorname{TC}$

Consider Grzegorczyk's concatenation theory $\operatorname{TC}$, a "weak theory of words over the two letter alphabet $\Sigma=\{a,b\}$" (this from Grzegorczyk and Zdanowski's paper Undecidability and ...
Thomas Benjamin's user avatar
2 votes
0 answers
147 views

Hosting Category Theory in a "universe" that is non-LFP

WHen I did my MSc, I was trained by a very talented topologist. I had a passion for the subject before and since. Now I am interested in category theory, but I seem to be very interested in the ...
Ben Sprott's user avatar
  • 1,281
2 votes
0 answers
165 views

Multitype approaches to choice?

I wonder if anyone has developed a set theory which approaches the issue of the non-emptiness of products of non-empty sets via a hierarchy of types (comparable to how Von Neumann–Bernays–Gödel set ...
David Feldman's user avatar
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
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
118 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
1 vote
0 answers
123 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
1 vote
0 answers
109 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
92 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