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
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 ...
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 ...
1 vote
0 answers
186 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$ ...
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 ...
62 votes
4 answers
6k views

When size matters in category theory for the working mathematician

I think a related question might be this (Set-Theoretic Issues/Categories). There are many ways in which you can avoid set theoretical paradoxes in dealing with category theory (see for instance ...
3 votes
1 answer
181 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 ...
7 votes
1 answer
402 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 ...
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 ...
6 votes
1 answer
441 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$ ...
4 votes
2 answers
515 views

Applications of ZFA-Set Theory

The set theory with atoms (ZFA), is a modified version of set theory, and is characterized by the fact that it admits objects other than sets, atoms. Atoms are objects which do not have any elements. ...
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 ...
6 votes
2 answers
363 views

Resource request on "$\in$-homomorphisms" in Set Theory

Very loosely put, this is the intuitive idea behind an $\in$-homomorphism: Let $\mathcal{U}$ and $\mathcal{W}$ be universes of sets. A function $f \colon \mathcal{U} \to \mathcal{W}$ is said to be an $...
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 ...
35 votes
3 answers
2k views

Defining $SU(n)$ in HoTT

From a recent answer by Mike Shulman, I read: "HoTT is (among other things) a foundational theory, on roughly the same ontological level as ZFC, whose basic objects can be regarded as $\infty$-...
1 vote
1 answer
308 views

Complete and consistent first-order theories that contain interesting phenomena

Gödel has shown that a consistent recursively axiomatizable first-order theory that can interpret Robinson arithmetic is incomplete. I think there is some sentimental value in working with a theory ...
9 votes
1 answer
769 views

Practical Benefits of HTT/univalent foundations for assisted proofs

I'm trying to understand what the claimed practical benefits of HTT/univalent foundations are for doing computer assisted proofs and while I've seen a lot of claims of benefits they all seem to be ...
14 votes
4 answers
2k views

Where is the end of universe?

In some sense the empty set ($\emptyset$) and the global set of all sets ($G$) are the ends of the universe of mathematical objects. The world which $ZFC$ describes has an end from the bottom and is ...
22 votes
1 answer
3k views

Proof-Theoretic Ordinal of ZFC or Consistent ZFC Extensions?

Let the proof theoretic ordinal $\alpha$ of a theory $T$ be the least recursive ordinal such that $T$ does not prove that $\alpha$ is well-founded. This ordinal is intended to quantify in some sense ...
21 votes
2 answers
3k views

Do set theorists work in T?

In the thread Set theories without "junk" theorems?, Blass describes the theory T in which mathematicians generally reason as follows: Mathematicians generally reason in a theory T which (...
10 votes
1 answer
1k views

Erroneous proof of recursion theorem examples

In his book Elements of Set Theory, Herbert Enderton defines (p. 70) a Peano system as a triple $(N, S, e)$ where $N$ is a set, $S$ is an $N$-valued function defined on $N$ and $e$ is a member of $N$ ...
20 votes
4 answers
4k views

Is there a categorical proof of Gödel's incompleteness theorem?

A significant result in set theory was shown by Cohen when he showed that the continuum hypothesis was independent of ZFC using a new technique called forcing. In Topos theory, this result has a new ...
15 votes
1 answer
821 views

Can the opposite of an elementary topos be an elementary topos?

This question is not really about elementary topoi, it is much more about a category $(\mathcal{E}, \Omega)$ admitting a subobject classifier, or about a category with power objects, you can choose ...
12 votes
3 answers
1k views

Elementary theory of the category of groupoids?

One axiomatisation of set theory, the Elementary Theory of the Category of Sets, or ETCS for short, comes from category theory and states that sets and functions form a locally cartesian-closed, ...
33 votes
3 answers
5k views

Top-down mathematics, or "Where it all begins"

Sorry if this is off-topic. It was my attempt to take a top-down approach to mathematics. Being an inexperienced undergraduate (so please take my writing here lightly), I've been presented with ZFC as ...
10 votes
1 answer
433 views

Is material set theory conservative over structural set theory?

Suppose a statement $\phi$ that doesn't use the global $\in$-relation or the global $=$-relation in an essential way is provable in some material set theory, say bounded Zermelo with choice. (So that ...
10 votes
1 answer
331 views

An internalized version of Tennenbaum's Theorem

Tennenbaum's celebrated 1959 theorem (see here for a reference) is certainly one of the key theorems in mathematical logic. Not so much for its proof, but because it helps "isolating" $N$ ...
0 votes
2 answers
1k views

Has there been any serious attempt at a "circular" foundation of mathematics?

As far as I know, there is no published attempt at a "circular" foundations of mathematics though I'ave seen it noted by many category theorists and logicians without in-depth analysis, e.g ...
35 votes
2 answers
3k views

Building algebraic geometry without prime ideals

$\DeclareMathOperator\Spec{Spec}\DeclareMathOperator\ev{ev}$Teaching algebraic geometry, in particular schemes, I am struggling to provide intuitive proofs. In particular, I find it counter-intuitive ...
2 votes
1 answer
450 views

Is the statement "All numbers are counting numbers" independent of $PA$?

In his paper, "Completed versus Incomplete Infinity in Arithmetic" (which can be found here), the late Edward Nelson defines the notion of 'counting number' as follows: 0 is a counting ...
11 votes
7 answers
1k views

(Non?)-linearity of the consistency strength ordering in ZF

Much of the research taking place in set theory, is related to the classification of sentences according to their consistency strength relative to ZF. In order to be more specific, we say that for all ...
1 vote
0 answers
488 views

Is this a good way of conceptualising the current status of Foundation of Maths projects?

I have been reading 'A Very Short Introduction to Mathematics' by Timothy Gowers and at one point he mentions that most of the mathematical proofs can be finally resolved to a set of logical ...
152 votes
5 answers
27k views

What makes dependent type theory more suitable than set theory for proof assistants?

In his talk, The Future of Mathematics, Dr. Kevin Buzzard states that Lean is the only existing proof assistant suitable for formalizing all of math. In the Q&A part of the talk (at 1:00:00) he ...
15 votes
2 answers
2k views

Formal definition of homotopy type theory

The HoTT community is quite friendly, and produces many motivational introductions to HoTT. The blog and the HoTT book are quite helpful. However, I want to get my hands directly onto that, and am ...
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 ...
7 votes
1 answer
302 views

What is difference between working with small and large category of spaces?

The following construction have always bugged me. This is p328, Remark 5.1.6.1 in Lurie's Higher Topos Theory. Lurie begins with the following: Construction: Let $C$ be a simplicial set. $S$ denote ...
11 votes
5 answers
981 views

Emergence of the discrete from the continuum

An almost eternal theme in Mathematics is the approximation of the Continuum by the Discrete. This core idea goes back at least to Archimedes, and remains active to these very days (and quite likely ...
6 votes
1 answer
293 views

Set Theoretic Geology II: The structure of the directed partial order of grounds

In my previous question Set-theoretic geology: controlled erosion? and the great answer by Jonas Reitz, I have learned a few things, starting from the awareness that I understand the fine-grain ...
8 votes
4 answers
748 views

Self-contained formalization of random variables?

I have not been able to find any formalization of random variables that supports construction of new random variables dependent on previously constructed ones. In what I have found, a random variable $...
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 ...
10 votes
4 answers
958 views

On a weak choice principle

[PLEASE SEE EDITS AT BOTTOM OF QUESTION] Consider the following set-theoretic axiom: For each set $X$ there exists a set-indexed collection $\{C_i \to X\}_{i\in I_X}$ of surjections such that for ...
16 votes
2 answers
796 views

Appearance of proof relevance in "ordinary mathematics?"

I've been wondering recently what—if any—applications proof theory has to ordinary mathematics (by which I mean algebra, analysis, topology, and so on). In particular, I'd be fascinated to see a proof ...
2 votes
1 answer
359 views

Reference request on Gentzen's proof of the consistency of PA

I've always been interested in having a good understanding of Gentzen's proof of the consistency of arithmetic. Being more precise, he showed that $PRA + WF(\epsilon_0) \vdash Con(PA)$. I am ...
12 votes
2 answers
832 views

The inconsistency of Graham Arithmetics plus $ \forall n, n < g_{64}$

As you all know, Ronald Graham just passed away. He is famous for many fabulous contributions to finite combinatorics, and much much more, but perhaps none of them is as popular as the infamous ...
15 votes
2 answers
1k views

Could Kronecker accept a proof of Goodstein's theorem?

A famous result of Goodstein asserts that the Goodstein sequence of integers terminates. For a precise statement and a short proof, see https://en.wikipedia.org/wiki/Goodstein%27s_theorem. A well ...
0 votes
0 answers
178 views

A syntax independent theory of categories

The classic way to encounter the theory of categories is via Set Theory via the typical definition we see for categories. We see all kinds of categories that are equivalent to the category of small ...
8 votes
3 answers
1k views

How much of concrete mathematics can be expressed in the language of category theory?

Question 1 How much of group/ring/lattice/... theory can be expressed in purely categorical terms (only using the notions object, morphism, identity morphism, and composition), that is, as properties ...
7 votes
1 answer
1k views

Are categories special, foundationally?

Some folks over at nLab want to use categories as a foundation for all of mathematics, I'm guessing as an alternative to sets. Sets work fine, and so do categories, so I have started wondering what ...
6 votes
1 answer
494 views

Historical origin of the empty set

The question is in the title: Who first claimed the existence / necessity of the empty set ? When did this happen ? Of course I know that the notation $\emptyset$ goes back to André Weil, and that ...
8 votes
2 answers
743 views

weakening naive comprehension to avoid the paradoxes

Weakening the axiom of naive comprehension has not been a popular way of escaping from the set-theoretic paradoxes because no consistent weakenings seem to be particularly well motivated or even to ...
28 votes
2 answers
2k views

Age of Stochasticity?

One user on MSE made an interesting question, which was unanswered so I suggested him to post it here but he refused for personal reasons and said I could ask it here. The question is this: Today ...

1 2
3
4 5
7