Set theory and type theory as the "foundation of mathematics"

Question

I've heard that set theory or type theory can be used as a foundation for mathematics. What does this mean, exactly? According to Gödel's Incompleteness Theorem, this does not mean you can derive all of mathematics from set theory or type theory. Does it mean that all other axioms of mathematics can be written using set theory or type theory? Is there a proof of this? In addition, which systems of set theory and type theory can be used to do this? Some of the systems that were originally conceived were shown to have inconsistencies. Which modern theories are there that don't have any (known) inconsistencies? How much are these theories used in practice?

Answer 1

Mathematics is about the study of objects and how they relate to one another through various relations that we come up with.

As such the question can be then

How do we construct these objects and relations?

At first it might seem like we must do every kind of object and relation on their own, as we have groups, functions, operations, folds, various numbers etc. However it can be shown that using sets we can construct all these things previous mentioned. So basically you can turn all concepts into sets and then start using set theory alone to describe it all.

However that becomes quickly enormously unweildly because the amount of parenthesis, sets in sets and much else grows astronomicly as you try this and keeping track of it in your mind is putting a lot of strain on your mind. I have myself written how we can define relations and functions from set theory and even there it starts getting a bit difficult to keep track of what kind of subsets and all we are talking about in the constructed sets from set theory and definition. So in that way it isn't "used". It is primarily used to demonstrate "we can do this" but once that is done few really bothers because, as said, it is too much work and it is mentally easier to work with clearly distinct concepts than the conversion to sets.

A note should be made there are areas of mathematics that have arisen without relying on sets, Category theory comes to mind. However even there you can technically make them into "sets", I put quotation marks around because such sets would be enormously large and is more called proper classes. They are technicly "too big" to be sets.

Which leads to the other questions. ZFC is the common set theory that is used most often, it has no known inconsistencies, that doesn't mean there aren't any. As you say Gödel's incompleteness theorem makes it impossible to be certain. Von Neumann–Bernays–Gödel set theory includes what is classes, proper classes are classes that are not sets. Classes however behave similar to sets without being sets. Many of the known old paradoxes of naive set theory, which was before ZFC, was due to an unstated (and even unknown) assumption that all classes are sets, which is false. When you realise this is not the case the paradoxes disappear in many regards.