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
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 "...
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 ...
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 ...
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 ...
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 $\...
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 ...
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 ...
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). ...
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 ...
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)$ ...
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" (...
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 $\...
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
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$ ...
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 ...
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 ...
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 ...
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 ...
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 ...
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 "...
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 ...
4
votes
0
answers
249
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 ...
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 ...
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 ...
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 ...
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 ...
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 ...
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 $...
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 ...
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, ...
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, ...
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 ...
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 ...
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 ...
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 ...
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 ...
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 ...
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 ...
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 ...
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,...
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 ...
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 ...
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 ...
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 ...
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 ...
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
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 $\...
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....
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 ...
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 ...