# Questions tagged [foundations]

The tag has no usage guidance.

207 questions
Filter by
Sorted by
Tagged with
250 views

### What is a good definition of a mathematical structure?

At the moment I am writing a textbook in Foundations of Mathematics for students and trying to give a precise definition of a mathematical structure, which is the principal notion of structuralist ...
718 views

### Examples of improved notation that impacted your research?

The intention of this question is to find practical examples of improved mathematical notation that enabled actual progress in someone's research work. I am aware that there is a related post ...
4k views

### Category theory and set theory: just a different language, or different foundation of mathematics?

This is a question to research mathematicians, as well as to those concerned with the history and philosophy of mathematics. I am asking for a reference. In order to make the reference request as ...
404 views
+400

### Positive set theory and the “co-Russell” set

This is a more focused version of a question which was asked at MSE a couple years ago, but is still unanswered there. That question asks about a broad range of theories, whereas this version focuses ...
296 views

### coordinate free foundations of trigonometry [closed]

What axioms for geometry and trigonometry would I have to chose in order to completely avoid coordinates in defining trig functions and showing the equivalence of their geometric (unit circle) and ...
498 views

### Shortest axiom of infinity for foundationless set theory

Let $T$ be the theory with a binary symbol $\in$, an unary symbol $S$, and the following axioms: Axiom of extension: \begin{equation} \forall x \forall y (\forall z (z \in x \leftrightarrow z \in ...
2k views

### How strong is this set theory?

In the spirit of this related question, consider a set theory with the following axioms: Axiom of extension: $$\forall x \forall y (\forall z (z \in x \leftrightarrow z \in y) \rightarrow x = y)$$ ...
676 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 ...
146 views

### Is there a foundational approach that takes “structure” as primitive?

As per the title, I'd be curious to know if there have been attempts at constructing a foundation of mathematics taking, somehow, purely the notion of "structure" as primitive, maybe via a system of ...
1k views

### Could groups be used instead of sets as a foundation of mathematics?

Sets are the only fundamental objects in the theory $\sf ZFC$. But we can use $\sf ZFC$ as a foundation for all of mathematics by encoding the various other objects we care about in terms of sets. The ...
278 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). ...
208 views

### Set of definable real numbers?

Is there a set theory at least as strong as $KP\omega$ which has as a theorem that there is a set $\mathbb{D}$ of precisely the definable real numbers?
180 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, ...
186 views

4k views

### What is an explicit bijection in combinatorics?

A standard way of demonstrating that two collections of combinatorial objects have the same cardinality is to exhibit a bijection between them. Browsing through some examples (here, there, yonder) ...
632 views

### Explaining the consistency of PRA and ZF from predicative foundations

Recently I got interested in predicative foundations, mostly because of Laura Crosilla's work and because Agda employs a predicative type theory. From the point of view of a predicative foundation to ...
231 views

### “Surjective cardinals” - using surjections rather than injections to define isomorphism classes of sets

Cantor used the notion of an "injection" to formalize the size of two sets: A is "smaller" than B if A injects into B. Simply put, the question is - how does this situation change if we use ...
926 views

### ZF(C) and category theory

Is there an axiomatisation of some kind of category theory and a definition of sets in this framework such that the axioms of ZF resp. ZFC are theorems?
69 views

### Questions in proof theory (PRA-provability of EA-theorems, Girards book from '87)

I've been working through a textbook, often encountering difficulties with the exercises. On mathstackexchange, with most of them I haven't arrived yet at a satisfactory solution. As I understand, ...
80 views

### Shepherdson's conditions - a shortcut to the second incompleteness theorem?

I've been working through a textbook, often encountering difficulties with the exercises. On mathstackexchange, with most of them I haven't arrived yet at a satisfactory solution. As I understand, ...
288 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 ...
256 views

### Formal foundations done properly [closed]

I would want to do mathematics properly, so that the proofs of results can be trusted on instead of them being just suggestions on which results could perhaps apply. This means formulating the math in ...
147 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 ...
560 views

### A peculiarity of Henkin's 1950 proof of completeness for higher order logic

My question concerns Henkin's original (1950) completeness proof https://projecteuclid.org/euclid.jsl/1183730860 for classical higher order logic and type theory relative to so-called general models. ...
381 views

357 views

883 views

### Are there logical systems where formal proofs are not computer verifiable?

In a set-theoretic system using first-order logic, every proof could be written as a goal followed by a finite sequence of sentence where each one is justified by an axiom or previously established ...
420 views

### Counting without one-to-one correspondence? [closed]

Ash and Gross in their wonderful book Fearless Symmetry found it worth mentioning (and thus suggesting) another way of counting for which "we do not even need to know how to count" (in the sense of ...
The principle of unique choice (PUC), also called the principle of function comprehension, says that if $R$ is a relation between two sets $A,B$, and for every $x\in A$ there exists a unique $y\in B$ ...