All Questions
Tagged with foundations soft-question
27 questions
9
votes
2
answers
473
views
Completing half of Hilbert's program: Foundations that are conservative over Peano Arithmetic
The goal of the Hilbert program was to find a complete and consistent formalization of mathematics. Gödel's first incompleteness theorem establishes that completeness is impossible with first-order ...
- 6,353
25
votes
1
answer
2k
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 ...
- 551
13
votes
0
answers
362
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 ...
- 395
5
votes
2
answers
629
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.
...
- 115
9
votes
1
answer
848
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 ...
- 3,029
1
vote
0
answers
522
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 ...
- 11
157
votes
5
answers
28k
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 ...
- 1,667
16
votes
2
answers
852
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 ...
- 177
63
votes
4
answers
7k
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,318
11
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 ...
- 237
8
votes
3
answers
2k
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 ...
6
votes
1
answer
993
views
Which branches of mathematics can be done just in terms of morphisms and composition?
Consider the first-order language $L_{\omega\omega}$ of the signature $L:=\{\mathrm{dom}, \mathrm{cod}, \mathrm{comp}\}$, where $\mathrm{dom}$ and $\mathrm{cod}$ are unary function symbols and $\...
user103598
60
votes
7
answers
9k
views
In what respect are univalent foundations "better" than set theory?
It was an ambitious project of Vladimir Voevodsky's to provide new foundations for mathematics with univalent foundations (UF) to eventually replace set theory (ST).
Part of what makes ST so appealing ...
8
votes
1
answer
403
views
Can ETCC/ETCS talk about 'size issues'?
In material set theories (like ZFC), one can prove that there is no set of all sets. Can one prove a similar statement in ETCS? This exact statement "there is no set x such that y in x for every set y"...
- 81
8
votes
1
answer
1k
views
Does equality between sets contradict the philosophy behind structural set theory?
Zermelo-Fraenkel set theory (with choice) is commonly accepted as the standard foundation of mathematics. It is a material set theory. This means that for every two objects/sets $a,b$ one can ask ...
- 89
19
votes
2
answers
2k
views
Which kind of foundation are mathematicians using when proving metatheorems?
Zermelo-Fraenkel set theory (with choice) is commonly accepted as the standard foundation of mathematics. It is a material set theory. For every two objects/sets $a,b$ one can ask whether $a=b$ or not....
user103598
1
vote
0
answers
223
views
What should one know about abstract sets and structural foundations?
Recently I came by accident across the book sets for mathematics by Lawvere. It says:
First we deplete the object of nearly all content. We could think of an idealized
computer memory bank that ...
25
votes
5
answers
4k
views
What is some current research going on in foundations about?
What is some current research going on in the foundations of mathematics about?
Are the foundations of mathematics still a research area, or is everything solved? When I think about foundations I'm ...
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 (...
- 221
1
vote
1
answer
484
views
"Co-ordinate-free" mathematics for general structures? [closed]
Edit (15 November 2017): I've just stumbled across this question, which I think is asking essentially the same thing I tried to ask below, but probably worded it more clearly - and got far more ...
- 3,612
0
votes
1
answer
678
views
Why do we try to encode every mathematical object as a set? [closed]
Probably everyone of us has seen set-theoretic encodings of mathematical objects which we wouldn't naturally consider to be sets. May it be the "definition" of a function from $A$ to $B$ as a relation ...
- 27
50
votes
4
answers
6k
views
Do set-theorists use informal set theory as their meta-theory when talking about models of ZFC?
Here, Noah Schweber writes the following:
Most mathematics is not done in ZFC. Most mathematics, in fact, isn't done axiomatically at all: rather, we simply use propositions which seem "intuitively ...
- 509
16
votes
3
answers
1k
views
Proof correctness problem
I was watching this talk by Vladimir Voevodsky which was given at the Institute of Advanced Study in 2006.
In his talk the first slide he shows has the following written on it:
...
6
votes
2
answers
1k
views
Why can't mathematics be formalised in terms of classes rather than sets? [closed]
I've always been curious about the seeming compulsion to found mathematics upon sets, be it ZF(C) or some other system. Of course, there are other approaches these days like category theory and type ...
- 820
20
votes
5
answers
2k
views
Does formalizing math require search and creativity, or is it near-mechanical?
I remember reading somewhere that it takes about a week to convert a page of math into something a proof-assistant like Isabelle or HOL Light would accept.
Is this type of conversion something that ...
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 ...
- 393
5
votes
5
answers
3k
views
Easy and Hard problems in Mathematics [closed]
Modified question:
I would like to know some examples of problems in Mathematics, for pedagogical purposes, which do not involve difficult techiques to solve the problem but with a change of context ...